Semantics of Predicate Logic

Now that we have seen the proof rules for Predicate Logic, we turn to its semantics. The semantics of Predicate Logic is more complex than the semantics of Propositional Logic that we saw in Week 1.

This page contains two videos introducing the semantics of Predicate Logic, and then an interactive tool that you can use to explore some (finite) models of Predicate Logic formulas.

Slides for the videos below

Models

To interpret a Predicate Logic formula, we need to upgrade the idea of a valuation (the mapping from atomic propositions to true/false values) to a model. Models come in two parts:

1. a collection of all the things that are considered to be in the universe for this model; and

2. the meanings of all the predicate symbols in our vocabulary as relations on the universe.

A useful intuition to think about models is as databases: each predicate symbol is interpreted as a (possibly infinite) table of related elements of the universe.

Models are explained in this video:

Interpretation of Formulas

Once we have a definition of model, we can interpret Predicate Logic formulas. We do this in the same way as we did for Propositional Logic: by breaking the formula down into its constituent parts, working out their meaning and then combining the meanings together.

Armed with an interpretation of formulas, we can define entailment for Predicate Logic. As with Propositional Logic, entailment means that for all models, if all the assumptions are true then the conclusion is true. Now there are infinitely many models, and each model may itself be infinite; so checking them all is no longer feasible. This is why proof for Predicate Logic is more essential than for Propositional Logic.

The interpretation of Predicate Logic formulas in a model, and the definition of entailment in predicate logic, are discussed in this video:

Examples

The following examples all use a tool that can synthesise models of a fixed size for a set of axioms. Click Run on each one to see what gets synthesised.

No axioms

With no axioms and no predicate symbols, there are no constraints on the model. We can have models of any size and there are no predicate symbols to give meaning to.

Something exists

Even with no predicate symbols, we can still say that something exists

Exercise What happens if you say “nothing exists”?

Only Equality

Even with no predicate symbols in the vocabulary, we can still say some interesting things using just equality.

Everything is equal

If we say that everything is equal to everything, then there can only be at most one thing in the model:

Exercise What sizes of model support the all-equal axiom?

Everything is unequal

With this tool we can only check that individual sizes of model do not exist. To prove that there are no models (even infinite ones), we can do a proof that these axioms entail “false” (to do this proof you will need the refl command from the proof rules for equality).

How to say that two things exist?

Below are several attempts to say that two things exist. Experiment with synthesising models for these axioms to learn exactly what they are expressing.

Unary Predicates

With unary predicates, we can talk about “types” of things and the relationships between them. The following example uses “humans” and “mortals”, and the relationship that all humans are mortal:

As above, we can check that HM3 has no models for each size 0, 1, 2, 3, ..., but to prove that there are no models of these axioms (i.e., these axioms are inconsistent), we have to do a proof that assuming both of these axioms entails “false”:

Exercise How would you say that there exists a mortal that is not human? Is adding this axiom to HM2 consistent?

Relations

Relations are predicates that have two or more arguments. They are used to express relationships between things.

Less than

“Less than” is a relationship between two things that is characterised by being transitive and irreflexive. Transitive means that if x is less than y and y is less than z, then x is less than z. Irreflexive means that nothing is less than itself.

The infinite axiom here, when coupled with the irreflexive axiom, is an example of an axiom that forces all models to be infinite. Unlike the examples above where there were no finite or infinite models, these do have infinite models, so it is not possible to prove “false” from these axioms.

Exercise What happens if you comment out the irreflexive axiom? Are there finite models then?

Less than or equal

“Less than or equal” is axiomatised by reflexivity, transitivity and antisymmetry*. Transitivity is the same as for “less than”. Reflexivity says that everything is “less than or equal” to itself. Anti-symmetry says that if x is less than or equal to y and y is less than or equal to x, then they are equal.

Exercise Can you add an axiom that makes the le relation minimal (so it only relates things to themselves)?

Exercise This axiomatisation of “less than or equal” generates forests. How can you make it generate models where everything is in a line?

Checking models

As well as synthesising models, we can get the computer to check them.

Going further

We have only scratched the surface of the kinds of things that can be expressed using Predicate Logic, and what kinds of models can be captured using axiomatisations. Try using the model synthesiser tool below to try different vocabularies and axiomisations and generate models for them: