Just as with propositional logic, one can define a proof system for first order logic. We first need two definitions.
Definition 1 If is a formula, a generalization of is any formula of the form
(We are not requiring in the definition above that the are different or that they are present in )
Definition 2 Let be a term, let be a variable, and let be a formula. We say that is substitutable for in iff no free occurrence of in is within the scope of a quantifier or with a variable occurring in
The point of this definition is the following: Given a formula a variable and a term , let denote the formula resulting of replacing each free occurrence of in by For example, if is and for some binary function symbol and variables then Similarly, because no occurrence of in is free, and
We would like to mean that has whatever property was claiming of However, some care is needed, as the last example shows: While asserts that there is some element other than , which is true in any model with at least two elements, no matter how is interpreted, we have that asserts that there is an element different from itself, which is always false.
The notion of “ being substitutable for ” captures the idea that, no matter what is, will actually express, as intended, the property of that expressed of .
2. A Hilbert-type proof system
Just as with propositional calculus, we can develop a notion of formal proof as a finite string of formulas with some properties.
First, we state the axioms of predicate logic. To be concrete, we formalize syntax, so the only primitive connectives are and the only quantifier is and all others are treated as abbreviations.
A logical axiom is any generalization of any formula of the following form:
- (Propositional axioms)
- (Quantifier axioms)
- provided that is not free in
- provided that is a term substitutable for in
- (Equality axioms)
As before, the only rule of inference is MP, Modus Ponens.
Proofs are defined as before: Given a set of formulas and a formula we write proves iff there is a proof of from i.e., a sequence
where each is either a logical axiom, or an element of or comes from previous by an application of MP. Again, if we simply write
It is easy to verify that whenever is a logical axiom and is a structure, and that if and then This is the soundness theorem.
More delicate is the verification of the completeness theorem. I will only sketch the idea of one of its proofs, due to Leon Henkin.
As with propositional calculus, it is enough to check that if is consistent, i.e., it does not prove a contradiction, then is satisfiable, i.e., it has a model. Just as in that proof, it is enough to prove this result for a set that is maximal, i.e., such that for any formula in the language of either or and one can also request that is actually closed under deduction, i.e., if then
Henkin’s first idea is to expand the language by adding new constants, and to expand the theory so it is Skolemized. The name comes from Thoralf Skolem, and refers to the notion of a Skolem Hull; this is a kind of substructure in which only definable elements are considered. What Henkin means here is the following: For each formula in the language, with only one free variable add a new constant symbol and add to the `axiom’
What this accomplishes is that now we have a canonical `witness’ to existential statements, namely, if and then in fact
One needs to verify that given any consistent in a language one can expand to a larger language and to in language so that is still consistent, it is maximal, and is Skolemized.
This is accomplished by iterating the obvious process: First expand so it is maximal consistent in language expand the language adding constants for all formulas in thus obtaining and expand as required to form This does not yet work, since there are new formulas, e.g. that do not yet admit Skolemization. So one repeats, first passing to a maximal consistent in language then obtaining a larger language and a larger theory in etc. The language and the theory are finally as required.
One of course needs to check that the passage from to does not add contradictions.
Once we have a theory maximal consistent and with Skolemization, let’s call it again, Henkin’s idea is to note that the theory essentially describes a model of itself.
Namely, one defines an equivalence relation on the constant symbols of the language by setting
(That this is indeed an equivalence relation follows easily from the equality axioms.)
Now we define a model by setting as its universe the set of equivalence classes We define the interpretations of constant, relation, and function symbols as dictated by For example, if is a symbol for a binary function, we define by setting
(One needs to check that this is well defined).
One sets for a constant symbol. Finally, one defines , for an -ary relation symbol, by
Once the model is defined, then one checks that as desired. This makes essential use of the fact that is Skolemized.
One nice property of this technique is that it implies that if is a theory in a countable language, and is consistent, then has a countable model. We will return to the issue of the sizes of models later in the course, once we have discussed infinite cardinalities.
An immediate consequence of the completeness theorem is compactness: If is unsatisfiable, then it must be inconsistent, and therefore a finite subtheory is inconsistent, hence unsatisfiable.
This indicates that some use of the axiom of choice is required in any proof of completeness, since we have seen that compactness implies the existence of nonprincipal ultrafilters, and it is known that this requires some amount of choice. (In the proof sketched above, we used choice each time we expanded a consistent theory to a maximal consistent one. If the original theory is countable, this only requires König’s lemma, but more choice is necessary if is uncountable.)
Typeset using LaTeX2WP. Here is a printable version of this post.