502 – Completeness

 
1. Preliminaries

Just as with propositional logic, one can define a proof system for first order logic. We first need two definitions.

Definition 1 If {\phi} is a formula, a generalization of {\phi} is any formula of the form

 

\displaystyle \forall x_1\forall x_2\dots\forall x_n\,\phi.

 

(We are not requiring in the definition above that the {x_i} are different or that they are present in {\phi.})

Definition 2 Let {t} be a term, let {x} be a variable, and let {\phi} be a formula. We say that {t} is substitutable for {x} in {\phi} iff no free occurrence of {x} in {\phi} is within the scope of a quantifier {\exists z} or {\forall z} with {z} a variable occurring in {t.}

The point of this definition is the following: Given a formula {\phi,} a variable {x,} and a term {t}, let {\phi[x/t]} denote the formula resulting of replacing each free occurrence of {x} in {\phi} by {t.} For example, if {\phi} is {\exists y\,(x\ne y),} and {t=f(z,w)} for some binary function symbol {f} and variables {z,w,} then {\phi[x/t]=\exists y\,(f(z,w)\ne y).} Similarly, {\phi[y/t]=\phi} because no occurrence of {y} in {\phi} is free, and {\phi[x/y]=\exists y\,(y\ne y).}

We would like {\phi[x/t]} to mean that {t} has whatever property {\phi} was claiming of {x.} However, some care is needed, as the last example shows: While {\phi} asserts that there is some element other than {x}, which is true in any model with at least two elements, no matter how {x} is interpreted, we have that {\phi[x/y]} asserts that there is an element different from itself, which is always false.

The notion of “ {t} being substitutable for {x}” captures the idea that, no matter what {\phi} is, {\phi[x/t]} will actually express, as intended, the property of {t} that {\phi} expressed of {x}.

 

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 {\lnot,\rightarrow} and the only quantifier is {\forall,} and all others are treated as abbreviations.

A logical axiom is any generalization of any formula of the following form:

  1. (Propositional axioms) 
    1. {\phi\rightarrow(\psi\rightarrow\phi).}
    2. {((\phi\rightarrow(\psi\rightarrow\chi))\rightarrow((\phi\rightarrow\psi)\rightarrow(\phi\rightarrow\chi)).}
    3. {(\lnot\phi\rightarrow\lnot\psi)\rightarrow((\lnot\phi\rightarrow\psi)\rightarrow\phi).}
  2. (Quantifier axioms)
    1. {\forall x\,(\phi\rightarrow\psi)\rightarrow(\forall x\,\phi\rightarrow\forall x\,\psi).}
    2. {\phi\rightarrow\forall x\,\phi,} provided that {x} is not free in {\phi.}
    3. {\forall x\,\phi\rightarrow\phi[x/t],} provided that {t} is a term substitutable for {x} in {\phi.}
  3. (Equality axioms)
    1. {x=x.}
    2. {x=y\rightarrow y=x.}
    3. {(x=y\land y=z)\rightarrow(x=z).}
    4. {(x_1=y_1\land \dots\land x_n=y_n)\rightarrow} {(f(x_1,\dots,x_n)=f(y_1,\dots,y_n)).}
    5. {(x_1=y_1\land\dots\land x_ny_n)\rightarrow} {(R(x_1,\dots,x_n)\leftrightarrow R(y_1,\dots,y_n)).}

As before, the only rule of inference is MP, Modus Ponens.

Proofs are defined as before: Given a set of formulas {S} and a formula {\phi,} we write {S\vdash\phi,} {S} proves {\phi,} iff there is a proof of {\phi} from {S,} i.e., a sequence

\displaystyle \phi_1,\dots,\phi_n

where each {\phi} is either a logical axiom, or an element of {S,} or comes from previous {\phi_j,\phi_k} by an application of MP. Again, if {S=\emptyset} we simply write {\vdash\phi.}

It is easy to verify that {{\mathcal M}\models \phi} whenever {\phi} is a logical axiom and {{\mathcal M}} is a structure, and that if {{\mathcal M}\models S} and {S\vdash\phi,} then {{\mathcal M}\models\phi.} This is the soundness theorem.

 

3. Completeness

 

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 {S} is consistent, i.e., it does not prove a contradiction, then {S} is satisfiable, i.e., it has a model. Just as in that proof, it is enough to prove this result for a set {S} that is maximal, i.e., such that for any formula {\phi} in the language of {S,} either {S\vdash \phi} or {S\vdash\lnot\phi,} and one can also request that {S} is actually closed under deduction, i.e., if {S\vdash\phi,} then {\phi\in S.}

Henkin’s first idea is to expand the language by adding new constants, and to expand the theory {S} 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 {\phi(x)} in the language, with only one free variable {x,} add a new constant symbol {c_\phi,} and add to {S} the `axiom’

\displaystyle  \exists x\,\phi\rightarrow\phi[x/c_\phi].

What this accomplishes is that now we have a canonical `witness’ to existential statements, namely, if {M\models S} and {M\models\exists x\,\phi,} then in fact {M\models\phi(c_\phi^M).}

One needs to verify that given any consistent {S} in a language {{\mathcal L},} one can expand {{\mathcal L}} to a larger language {{\mathcal L}'} and {S} to {S'} in language {{\mathcal L}'} so that {S'} is still consistent, it is maximal, and is Skolemized.

This is accomplished by iterating the obvious process: First expand {S} so it is maximal consistent in language {{\mathcal L},} expand the language adding constants {c_\phi} for all formulas {\phi} in {{\mathcal L},} thus obtaining {{\mathcal L}_1,} and expand {\hat S} as required to form {S_1.} This does not yet work, since there are new formulas, e.g. {\exists x\,(x\ne c_{y=y})} that do not yet admit Skolemization. So one repeats, first passing to a maximal consistent {\hat S_1} in language {{\mathcal L}_1,} then obtaining a larger language {{\mathcal L}_2} and a larger theory {S_2} in {{\mathcal L}_2,} etc. The language {{\mathcal L}'=\bigcup_n{\mathcal L}_n} and the theory {S'=\bigcup_n S_n} are finally as required.

One of course needs to check that the passage from {S_n} to {S_{n+1}} does not add contradictions.

Once we have a theory maximal consistent and with Skolemization, let’s call it {S} 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

\displaystyle  c\sim c' \Longleftrightarrow S\vdash c=c'.

(That this is indeed an equivalence relation follows easily from the equality axioms.)

Now we define a model {M} by setting as its universe the set of equivalence classes {[c].} We define the interpretations of constant, relation, and function symbols as dictated by {S.} For example, if {f} is a symbol for a binary function, we define {f^M:M\times M\rightarrow M} by setting

\displaystyle  f^M([a],[b])=[c_{x=f(a,b)}].

(One needs to check that this is well defined).

One sets {a^M=[a]} for {a} a constant symbol. Finally, one defines {R^M}, for {R} an {n}-ary relation symbol, by

\displaystyle  R^M([a_1],\dots,[a_n])\Longleftrightarrow S\vdash R(a_1,\dots,a_n).

Once the model {M} is defined, then one checks that {M\models S,} as desired. This makes essential use of the fact that {S} is Skolemized.

One nice property of this technique is that it implies that if {S} is a theory in a countable language, and {S} is consistent, then {S} 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 {S} is unsatisfiable, then it must be inconsistent, and therefore a finite subtheory {S_0} 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 {S} is uncountable.)

Typeset using LaTeX2WP. Here is a printable version of this post.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: