model theory, interpretation, completeness theorem, Post, truth table, truth, Skolem, table, paradox, model, satisfiable, completeness, Skolem paradox, formula, logically valid, true, false, satisfiability

Back to title page

4. Completeness Theorems (Model Theory)

4.1. Interpretations

Let us recall the beginning part of Section 1.2:

The vision behind the notion of first order languages is centered on the so-called "domain" - a collection of "objects" that you wish to "describe" by using the language. Thus, the first kind of language elements you will need are variables:

x, y, z, x₁, y₁, z₁, ...

The above-mentioned "domain" is the intended "range" of all these variables.

...

The next possibility we may wish to have in our language are the so-called constant letters - symbols denoting some specific "objects" of our "domain".

...

In some languages we may need also the so-called function letters - symbols denoting specific functions, i.e. mappings between "objects" of our "domain", or operations on these objects.

...

The last kind of primitives we need in our language are the so-called predicate letters - symbols denoting specific properties (of) or relations between "objects" of our "domain".

...

Thus, the specification of a first order language includes the following primitives:

1) A countable set of variable names (you could generate these names, for example, by using a single letter "x": x, xx, xxx, xxxx, ...).

2) An empty, finite, or countable set of constant letters.

3) An empty, finite, or countable set of function letters. To each function letter a fixed argument number must be assigned.

4) A finite, or countable set of predicate letters. To each predicate letter a fixed argument number must be assigned.

Different sets of primitives yield different first order languages.

By using the language primitives, we can build terms, atomic formulas and (compound) formulas.

...

... we can define the notion of formula of our language as follows:

a) Atomic formulas are formulas.

b) If B and C are formulas, then (B->C), (B&C), (BvC), and (~B) also are formulas.

c) If B is a formula, and x is a variable, then (AxB) and (ExB) also are formulas.

...

All really working formal mathematical theories are formulated as the so-called first order theories.

Each first order theory T includes:

a) a specific first order language L(T),

b) logical axioms and rules of inference for this language (the classical, constructive or minimal version may be adopted),

c) a set of specific non-logical axioms of T.

End of quotes from Section 1.2.

In principle, to do the so-called pure mathematics, i.e. simply to prove theorems, we need only axioms and rules of inference.

But how about "applying" of our formal mathematical theories? In natural sciences we are used to think of theories as "theories of something" - classical mechanics, relativistic mechanics, general relativity theory, quantum mechanics, thermodynamics, electrodynamics, cosmology etc.

We will not attempt investigating applications of mathematical theories to real world structures (with observation, measurement, and other delicate problems involved). Instead, let us investigate applications of first order theories to mathematical structures - the so-called model theory.

Model theory is a very specific approach to investigation of formal theories as mathematical objects. Model theory is using (up to) the full power of set theory. Model theory is investigation of formal theories by using set theory as a metatheory.

The main structures of model theory are non-constructive (see below) interpretations. Let L be a first order language containing constant letters c₁, ..., c_k, ... , function letters f₁, ..., f_m, ..., and predicate letters p₁, ..., p_n, .... An interpretation J of the language L consists of the following objects:

a) a non-empty set D_J - the domain of interpretation (it will serve as the range of variables),

b) a mapping int_J that assigns:

- with each constant letter c_i - a member int_J(c_i) of the domain D_J (thus, constants "denote" particular objects in D_J),

- with each function letter f_i - a function int_J(f_i) from D_J x ... x D_J into D_J (of course, int_J(f_i) has the same number of arguments as f_i),

- with each predicate letter p_i - a predicate int_J(p_i) on D_J, i.e. a subset of D_J x ... x D_J (of course, int_J(p_i) has the same number of arguments as p_i).

As an example, let us consider the so-called standard interpretation S of the first order (Peano) arithmetic PA:

a) The domain is D_S = {0, 1, 2, ...}.

b) The mapping int_S assigns: with the constant 0 - the number 0, with the constant 1 - the number 1, with the function letter "+" - the function x+y (addition of natural numbers), with the function letter "*" - the function x*y (multiplication of natural numbers), with the predicate letter "=" - the predicate x=y (equality of natural numbers).

Having an interpretation J of the language L, we can define the notion of true formula (more precisely - the notion of formulas that are true under the interpretation J).

As the first step, terms of the language L are interpreted as members of D_J or functions over D_J. indeed, terms are defined as constant letters, or variable letters, or their combinations by means of function letters. The term c_i is interpreted as the member int_J(c_i) of D_J. The variable x_i is interpreted as the function X_i(x_i) = x_i. And, if t = f_i(t₁, ..., t_q), then int_J(t) is defined as the function obtained by substituting of functions int_J(t₁), ..., int_J(t_q) into the function int_J(f_i).

For example (first order arithmetic), the standard interpretation of the term (x+y+1)*(x+y+1) is the function (x+y+1)².

Important - non-constructivity! Note that, for an infinite domain D_J, the interpretations of function letters may be non-computable functions.

As the next step, the notion of true atomic formulas is defined. Of course, if a formula contains variables (as, for example, the formula x+y=1), then its "truth-value" must be defined for each combination of values of these variables. Thus, to obtain the truth-value of the formula p_i(t₁, ..., t_q) for some fixed values of the variables contained in t₁, .., t_q, we must first "compute" the values of these terms, and then substitute these values into the predicate int_J(p_i).

For example (first order arithmetic), under the standard interpretation S, the formula x+y=1 will be true, iff either x takes the value 0, and y takes the value 1, or x takes the value 1, and y takes the value 0. Otherwise, it is false.

Important - non-constructivity! Note that, for an infinite domain D_J, the interpretations of predicate letters may be non-computable predicates.

And finally, we "define" the notion of true compound formulas of the language L under the interpretation J (of course, for a fixed combination of values of their free variables):

a) Truth-values of the formulas ~B, B&C, BvC and B->C must be computed from the truth-values of B and C (by using the classical truth tables from Section 4.2 below).

b) The formula AxB is true, iff B(c) is true for all members c of the domain D_J.

c) The formula ExB is true, iff there is a member c of the domain D_J such that B(c) is true.

For example (first order arithmetic), the formula Ey((x=y+y) v (x=(y+y+1)) says that "each number is even or odd". Under the standard interpretation S, this formula is true for all values of its free variable x. Similarly, AxAy(x+y=y+x) is a closed formula that is true under S.

Important - non-constructivity! It may seem that, under an interpretation, any closed formula is "either true or flase". However, note that, for an infinite domain D_J, the notion of true formulas is extremely non-constructive: to establish, for example, the truth-value of the formula AxB, or the formula AxAy(x+y=y+x), we must verify the truth of B(c) for infinitely many values of c (or a+b=b+a for infinitely many values of a and b). Of, course, this verification cannot be performed on a computer. It can only (sometimes) be proved... in some other theory. The "degree of constructivity" of the formulas like as AxEyC(x,y), AxEyAzD(x,y,z) etc. is even less than that...

Empty Domains?

Do you think, we should consider also empty domains of interpretation D_J? According to the axiom L₁₃: (B->B)->Ex(B->B), hence, Ex(B->B). In an empty domain, this formula would be false. Thus, to cover the empty domain, we would be forced to re-consider the axioms and/or re-consider the traditional meaning of Ex - see (c) above.

Let us say that a formula of the language L is always true under the interpretation J, iff this formula is true for all combinations of values of its free variables.

Logically Valid Formulas

Some formulas are always true under all interpretations, for example:

(B->C) & (C->D) -> (B->D),

F(x) -> ExF(x),

AxF(x) -> F(x),

Ax(F(x)->G(x)) -> (AxF(x)->AxG(x)),

Ax(F(x)->G(x)) -> (ExF(x)->ExG(x)).

Such formulas are called logically valid. More precisely, in a first order language L, a formula is called logically valid, iff it is true in all interpretations of the language L for all values of its free variables.

Thus, a logically valid formula is true independently its "meaning" - the interpretations of constants, functions and predicates used in it. But note that the (classical!) interpretations of propositional connectives and quantifiers remain fixed.

The notion of logically valid formulas is doubly non-constructive in the sense that the universal quantifier "for all interpretations" is added to the (already) non-constructive definition of a (simply) true formula.

As an example, let us verify that the axiom L₁₂: AxF(x)->F(t) is logically valid. Let us assume that, under some interpretation J, for some values of its free variables, L₁₂ is false. According to the classical truth tables, this could be only, iff AxF(x) were true, and F(t) were false (under the interpretation J, for the same above-mentioned values of free variables). Let us "compute" the value of the term t for these values of free variables (since the substitution F(x/t) is admissible, t may contain only these variables - recall the Exercise 1.2.5), and denote it by c. Thus, F(c) is false. But AxF(x) is true, hence, F(a) is true for all a in the domain D_J, i.e. F(c) also is true. Contradiction. Hence, L₁₂ is true under all interpretations for all combinations of its free variables (if any).

Exercise 4.1.1. Verify that the above 5 formulas are logically valid. (Hint: follow the above example - assume that there is an interpretation J such that the formula under question is false for some values of its free variables, and derive a contradiction.)

To conclude that some formula is not logically valid, we must build an interpretation J such that the formula under question is false for some values of its free variables.

As an example, let us verify that the formula Ax(p(x) v q(x)) -> Ax p(x) v Ax q(x) is not logically valid (p, q are predicate letters). Why it is not? Because the truth-values of p(x) and q(x) may behave in such a way that p(x) v q(x) is always true, but neither Ax p(x), nor Ax q(x) is true. Indeed, let us take the domain D = {0, 1}, and set

p(0) = true, q(0) = false, p(1)=false, q(1)=true.

In this interpretation, p(0) v q(0) = true, p(1) v q(1) = true, i.e. Ax(p(x) v q(x)) is true. But Ax p(x), Ax q(x) both are false. Hence, in this interpretation, Ax p(x) v Ax q(x) is false, and Ax(p(x) v q(x)) -> Ax p(x) v Ax q(x) is false. We have built an interpretation, making the formula under question false. Q.E.D.

Exercise 4.1.2. Verify that the following formulas are not logically valid (p, q, r are predicate letters):

a) p(x, y) & p(y, z) -> p(x, z),

b) q(x)->Ax q(x),

c) (Ax q(x)->Ax r(x))->Ax(q(x)->r(x)),

c₁) Ex(p(x)->B)->(Ex p(x)->B), where B does not contain x,

d) AxEy p(x, y)->EyAx p(x, y),

e) Ex q(x) & Ex r(x) -> Ex(q(x)&r(x)),

f) Ax ~p(x, x) & AxAyAz(p(x, y) & p(y, z) -> p(x, z)) -> AxAy(x=y v p(x, y) v p(y, x)).

(Hint: follow the above example - use natural numbers or other objects to build an interpretation J such that the formula under question is false for some values of its free variables.)

Upside Down?

If T is a first order theory, and J is an interpretation of its language, then (traditionally) J is called a model of T, iff J makes true all axioms of T (and hence, all theorems of T - verify that! - or see Lemma 4.2.2 below). To normal people, such a notion of model may seem somewhat strange: in "normal" branches of science theories serve as a basis for building models of natural phenomena or technical devices. In the mathematical logic, we have turned this approach upside down - theories, not phenomena or devices, are "modelled"!

Two Notes

1. Specific axioms of a first order theory T are not logically valid formulas - they are not true in all interpretations, they are true only in the models of T. Models of T are a proper subclass of all the possible intepretations. For example, the "obvious" arithmetical axioms like as x+0=x (or theorems like as x+y=y+x) are not logically valid. If we would interpret 0 as the number "two", then x+0 will be not x! Logically valid formulas must be true under all interpretations!

Exercise 4.1.2X. Verify that x*0=0, x+y=y+x and x+(y+z)=(x+y)+z are not a logically valid formulas.

2. In a sense, logically valid formulas "do not contain information". Indeed, let us consider the formulas x+0=x -> x+0=x, and x+0=0 -> x+0=0. Both are logically valid, but do we know more about zero and addition after reading them? Another example: 2*2=5 -> 2*2=5.

Satisfiability

Recall that, in a first order language L, a formula is called logically valid, iff it is true in all interpretations of the language L for all values of its free variables.

In a first order language L, a formula F is called satisfiable, iff there is an interpretation of the language L such that F is true for some values of its free variables. A set of formulas F₁, ..., F_n is called satisfiable, iff the conjunction F₁& ...&F_n is satisfiable, i.e. if the formulas F₁, ..., F_n can be satisfied simultaneously.

Exercise 4.1.3. Verify that: a) F is satisfiable, iff ~F is not logically valid, and b) F is logically valid, iff ~F is unsatisfiable.

Exercise 4.1.4. a) Verify that the formula Axy(p(x)->p(y)) is always true in all one-element interpretations (i.e. when the interpretation domain consists of a single element), but is false in at least one two-element interpretation (p is a predicate letter).

b)Verify that the formula AxAyAz[(p(x)<->p(y))v(q(y)<->q(z))v(r(z)<->r(x))] is always true in all one- and two-element interpretations, but is false in at least one three-element interpretation (p, q, r are predicate letters).

c) Prove that the formula ExAy F(x,y) is logically valid, iff so is the formula Ex F(x, g(x)), where g is a function letter that does not appear in F.

d) Prove that the formula AxAyEz F(x,y,z) is satisfiable, iff so is the formula AxAy F(x, y, h(x,y)), where h is a function letter that does not appear in F.

4.2. Classical Propositional Logic - Truth Tables

Emil Leon Post (1897-1954). "... Post's Ph.D. thesis, in which he proved the completeness and consistency of the propositional calculus described in the Principia Mathematica by introducing the truth table method. He then generalised his truth table method, which was based on the two values "true" and "false", to a method which had an arbitrary finite number of truth-values... In the 1920s Post proved results similar to those which G�del, Church and Turing discovered later, but he did not publish them. He reason he did not publish was because he felt that a 'complete analysis' was necessary to gain acceptance." (According to MacTutor History of Mathematics archive).

First, let us investigate possible interpretations of the propositional connectives - conjunction, disjunction, implication and negation. Do you think, there is only one way to do this?

The simplest possible approach to interpretation of propositional connectives assumes that if we know "truth-values" of operands, then we must be able to compute the "truth-value" of the expression. Thus we arrive to the so-called truth tables (in fact, classical truth tables)..

If B is false, and C is false, then B&C is false.
If B is false, and C is true, then B&C is false.
If B is true, and C is false, then B&C is false.
If B is true, and B is true, then B&C is true.

If B is false, and C is false, then BvC is false.
If B is false, and C is true, then BvC is true.
If B is true, and C is false, then BvC is true.
If B is true, and C is true, then BvC is true.

If B is false, then ~B is true.
If B is true, then ~B is false.

No problems so far.

If B is false, and C is false, then B->C is what? False? But, why?
If B is false, and C is true, then B->C is what? False? But, why?
If B is true, and C is false, then B->C is false.
If B is true, and C is true, then B->C is what? Perhaps, not false? Hence, true?

How to answer the 3 what's? If B is false, then B->C possesses no real meaning. If we already know that B is true, and C is true, then B->C is no more interesting. But, if a definite "truth-

value" for B->C is mandatory in all cases, then we can greatly simplify our logical apparatus by assuming that B->C is always true, except, if B is true, and C is false. Thus:

If B is false, and C is false, then B->C is true.
If B is false, and C is true, then B->C is true.
If B is true, and C is false, then B->C is false.
If B is true, and C is true, then B->C is true.

This definition is equivalent to saying that B->C is true, iff ~(B&~C) is true (or: B->C is false. iff B is true, and C is false).

Lemma 4.2.1. Under the above classical truth tables, all the classical propositional axioms L₁-L₁₁ take only true values.

Proof. First, let us verify L₁₁ and L₁₀:

Exercise 4.2.1. Verify L₁-L₉.

Lemma 4.2.2. Under the classical truth tables, if the formulas B and B->C take only true values, then so does C. I.e. from "always true" formulas, Modus Ponens allows deriving only of "always true" formulas.

Proof. Let us assume that, in some situation, C takes a false value. In the same situation, B and B->C take true values. If B is true, and C is false, then B->C is false. Contradiction. Hence, C takes only true values. Q.E.D.

Note. In the proof of Lemma 4.2.2, only the third row of implication truth table was significant: if B is true, and C is false, then B->C is false!

Theorem 4.2.3 ("soundness" of the classical propositional logic). If [L₁-L₁₁, MP]: |- F, then, under the classical truth tables, F takes only true values.

Proof. By induction, from Lemmas 4.2.1 and 4.2.2.

How about the converse statement of Theorem 4.2.3: if, under the classical truth tables, formula F takes only true values, then [L₁-L₁₁, MP]: |- F? I.e., are our axioms powerful enough to prove any formula that is taking only true values? The answer is "yes":

Theorem 4.2.4 (completeness of the classical propositional logic). Assume, the formula F has been built of formulas B₁, B₂, ..., B_n by using propositional connectives only. If, under the classical truth tables, for any (possible and impossible) truth-values of B₁, B₂, ..., B_n, formula F takes only true values, then:

a) in the constructive logic, [L₁-L₁₀, MP]: B₁v~B₁, B₂v~B₂, ..., B_nv~B_n |- F,

b) in the classical logic, [L₁-L₁₁, MP]: |- F.

Thus, the classical propositional axioms [L₁-L₁₁, MP] are, in a sense, "complete" - within the range of their "responsibility" they allow proving of any formula that takes only true values.

Of course, (b) follows from (a) immediately - all the premises B₁v~B₁, B₂v~B₂, ..., B_nv~B_n are instances of the axiom L₁₁.

Note. Assume, the formula F is built of formulas B₁, B₂, ..., B_n by using propositional connectives only. If, under the classical truth tables, for any (possible and impossible) truth-values of B₁, B₂, ..., B_n, formula F takes only true values, then F is called a tautology. Theorem 4.2.4 says that any tautology can be proved in the classical propositional logic.

Completeness of the classical propositional logic - Theorem 4.2.4(b) was first proved by Emil L.Post in his 1920 Ph.D. thesis:

E.Post. Introduction to a general theory of elementary propositions. Amer. journ. math., 1921, vol. 21, pp.163-195

Following an elegant later idea by Laszlo Kalmar we need two lemmas before trying to prove this theorem.

L.Kalmar. Ueber Axiomatisiebarkeit des Aussagenkalkuels. Acta scientiarium mathematicarum (Szeged). 1934-35. vol. 7, pp. 222-243.

Lemma 4.2.5. In the constructive logic, one can "compute" the classical truth-values of ~B, B->C, B&C, BvC in the following sense:

Note. Thus, to "compute" the classical truth-values, L₁₁ is not necessary!

Proof.

~B |- ~B

Immediately, in any logic.

B |- ~~B

By Theorem 2.4.4. [L₁, L₂, L₉, MP]: |- A->~~A.

~B, C |- B->C
~B, ~C |- B->C

By axiom L₁₀: ~B->(B->C) we obtain ~B |- B->C. This covers both cases.

B, ~C |- ~(B->C)

This is exactly Theorem 2.4.1(c) [L₁, L₂, L₉, MP].

B, C |- B->C

By axiom L₁: C->(B->C) we obtain C |- B->C.

~B, ~C |- ~(B&C)
~B, C |- ~(B&C)

By axiom L₃: B&C->B and the Contraposition Law (Theorem 2.4.2) [L₁, L₂, L₉, MP]: |- (A->B)->(~B->~A) we obtain |- ~B->~(B&C), or ~B |- ~(B&C). This covers both cases.

B, ~C |- ~(B&C)

By axiom L₄: B&C->C and the Contraposition Law (Theorem 2.4.2) [L₁, L₂, L₉, MP]: |- (A->B)->(~B->~A) we obtain |- ~C->~(B&C), or ~C |- ~(B&C).

B, C |- B&C

By axiom L₅: B->(C->B&C) we obtain B, C |- B&C.

~B, ~C |- ~(BvC)

By Theorem 2.4.10(b).

~B, C |- BvC

By axiom L₇: C->BvC we obtain C |- BvC.

B, ~C |- BvC
B, C |- BvC

By axiom L₆: B->BvC we obtain B |- BvC. This covers both cases.

Q.E.D.

As the next step, we will generalize Lemma 4.2.5 by showing how to "compute" truth-values of arbitrary formula F, which is built of formulas B₁, B₂, ..., B_n by using more than one propositional connective. For example, let us take the formula BvC->B&C:

We will show that, in the constructive logic [L₁-L₁₀, MP]:

~B, ~C |- BvC->B&C,
~B, C |- ~(BvC->B&C),
B, ~C |- ~(BvC->B&C),
~B, ~C |- BvC->B&C.

Lemma 4.2.6. Assume, the formula F has been built of formulas B₁, B₂, ..., B_n by using propositional connectives only. Assume that, if the formulas B₁, B₂, ..., B_n take the truth-values v₁, v₂, ..., v_n respectively, then, for these values, formula F takes the truth-value w. Then, in the constructive logic, we can "compute" the truth-value of F in the following sense:

[L₁-L₁₀, MP]: v₁B₁, v₂B₂, ..., v_nB_n |- wF,

where: wF denotes F, if w is true, and ~F, if w is false, and v_iB_i denotes B_i, if v_i is true, and ~B_i, if v_i is false.

Proof. By induction.

Induction base. F is one of the formulas B_i. Then w=v_i, and, of course, in any logic, v_iB_i |- wF.

Induction step.

Note that Lemma 4.2.5 represents the assertion of Lemma 4.2.6 for formulas built of B₁, B₂, ..., B_n by using a single propositional connective.

1. F is ~G. By induction assumption, [L₁-L₁₀, MP]: v₁B₁, v₂B₂, ..., v_nB_n |- w'G, where w' represents the truth-value of G. By Lemma 4.2.5, [L₁-L₁₀, MP]: w'G |- wF, hence, [L₁-L₁₀, MP]: v₁B₁, v₂B₂, ..., v_nB_n |- wF.

2. F is G o H, where o is implication, conjunction, or disjunction. By induction assumption, [L₁-L₁₀, MP]: v₁B₁, v₂B₂, ..., v_nB_n |- w'G, where w' represents the truth-value of G, and [L₁-L₁₀, MP]: v₁B₁, v₂B₂, ..., v_nB_n |- w''H, where w'' represents the truth-value of H. By Lemma 4.2.5, [L₁-L₁₀, MP]: w'G, w''H |- wF, hence, [L₁-L₁₀, MP]: v₁B₁, v₂B₂, ..., v_nB_n |- wF.

Q.E.D.

Proof of Theorem 4.2.4(a). By Lemma 4.2.6:

[L₁-L₁₀, MP]: B₁, v₂B₂, ..., v_nB_n |- F,
[L₁-L₁₀, MP]: ~B₁, v₂B₂, ..., v_nB_n |- F,

because F takes only true values. By [L₁, L₂, MP] Deduction Theorem 1,

[L₁-L₁₀, MP]: v₂B₂, ..., v_nB_n |- B₁->F,
[L₁-L₁₀, MP]: v₂B₂, ..., v_nB_n |- ~B₁->F,

Let us merge these two proofs and append an instance of the axiom L₈:

|- (B₁->F)->((~B₁->F)->(B₁v~B₁->F)).

Hence, by MP:

[L₁-L₁₀, MP]: v₂B₂, ..., v_nB_n |- B₁v~B₁->F,

and

[L₁-L₁₀, MP]: B₁v~B₁, v₂B₂, ..., v_nB_n |- F.

By repeating this operation we obtain Theorem 4.2.4(a):

[L₁-L₁₀, MP]: B₁v~B₁, B₂v~B₂, ..., B_nv~B_n |- F.

Q.E.D.

From now on, we could forget our ability of proving formulas in the classical propositional logic, learned in Section 2. In order to verify, is a formula provable in [L₁-L₁₁, MP], or not, we can simply check, under the classical truth tables, takes this formula only true values, or not. Is this checking really simpler than proving formulas in [L₁-L₁₁, MP]? Of course, if your formula contains 2 or 3 atoms (like as (A->B)->~AvB, or the axiom L₂), then its "truth table" consists of 4 or 8 rows - for most people this is a feasible task. But the "truth table" for a formula containing 32 atoms will contain more than a billion of rows... Let us try inventing a more efficient algorithm? It seems, we will never succeed - see Section 6.1.

4.3. Classical Predicate Logic - Goedel's Completeness Theorem

Kurt G�del (1906-1978) "He is best known for his proof of G�del's Incompleteness Theorems. In 1931 he published these results in �ber formal unentscheidbare S�tze der Principia Mathematica und verwandter Systeme . ...G�del's results were a landmark in 20th-century mathematics, showing that mathematics is not a finished object, as had been believed. It also implies that a computer can never be programmed to answer all mathematical questions." (According to MacTutor History of Mathematics archive).

As David Hilbert and Wilhelm Ackermann published in

D.Hilbert, W.Ackermann. Grundzuege der theoretischen Logik. Berlin (Springer), 1928,

in a sense, the "final" version of the axioms of the classical logic, they observed: "Whether the system of axioms is complete at least in the sense that all the logical formulas which are correct for each domain of individuals can actually be derived from them, is still an unsolved question." (quoted after

S.C.Kleene. The Work of Kurt Goedel. "The Journal of Symbolic Logic", December 1976, Vol.41, N4, pp.761-778).

Indeed, as we will verify below, a) all axioms of the classical logic (L₁-L₁₁, L₁₂-L₁₅) are logically valid, b) the inference rules MP, Gen allow to prove (from logically valid formulas) only logically valid formulas. Hence, in this way only logically valid formulas can be proved. Still, is our list of logical axioms complete in the sense that all logically valid formulas can be proved? - the question asked by Hilbert and Ackermann in 1928. The answer is "yes" - as Kurt Goedel established in 1929, in his doctoral dissertation "Ueber die Vollstaendigkeit des Logikkalkuels"(visit Goedel's Archive in the Princeton University Library). The corresponding paper appeared in 1930:

K.Goedel. Die Vollstaendigkeit der Axiome des logischen Funktionenkalkuels. "Monatshefte fuer Mathematik und Physik", 1930, Vol.37, pp.349-360.

Goedel's Completeness Theorem. In any first order language, a formula is logically valid, iff it can be proved by using the classical logic [L₁-L₁₁, L₁₂-L₁₅, MP, Gen].

First, let us prove the easy part (sometimes called the soundness theorem) - that all the formulas that can be proved by using the classical logic [L₁-L₁₁, L₁₂-L₁₅, MP, Gen] are logically valid.

Lemma 4.3.1. All axioms of the classical logic (L₁-L₁₁, L₁₂-L₁₅) are logically valid.

Proof.

1) Under the classical truth tables, the propositional axioms L₁-L₁₁ take only true values (Lemma 4.2.1). Hence, these axioms are true under all interpretations.

2a) L₁₂: AxF(x)->F(t), where F is any formula, and t is a term such that the substitution F(x/t) is admissible.

Let us assume that, under some interpretation J, for some values of its free variables, L₁₂ is false. According to the classical truth tables, this could be only, iff AxF(x) were true, and F(t) were false (under the interpretation J, for the same above-mentioned values of free variables). Let us "compute" the value of the term t for these values of free variables (since the substitution F(x/t) is admissible, t may contain only these variables - recall the Exercise 1.2.5), and denote it by c. Thus, F(c) is false. But AxF(x) is true, hence, F(a) is true for all a in the domain D_J, i.e. F(c) also is true. Contradiction. Hence, L₁₂ is true under all interpretations for all combinations of its free variables.

2b) L₁₃: F(t)->ExF(x), where F is any formula, and t is a term such that the substitution F(x/t) is admissible.

Similarly, see Exercise 4.3.1.

2c) L₁₄: Ax(G->F(x))->(G->AxF(x)), where F is any formula, and G is a formula that does not contain x as a free variable.

Let us assume that, under some interpretation J, for some values of its free variables, L₁₄ is false. According to the classical truth tables, this could be only, iff Ax(G->F(x)) were true, and G->AxF(x) were false (under the interpretation J, for the same above-mentioned values of free variables)

If Ax(G->F(x)) is true, then G->F(c) is true for all c in D_J. Since G does not contain x, this means that if G is true, then F(c) is true for all c in D_J.

From the orher side, if G->AxF(x) is false, then G is true, and AxF(x) is false. And finally, if AxF(x) is false, then F(c) is false for some c in the domain D_J. But, as we established above, if G is true, then F(c) is true for all c in D_J. Contradiction. Hence, under all interpretations, L₁₄ is true for all combinations of its free variables.

2d) L₁₅: Ax(F(x)->G)->(ExF(x)->G), where F is any formula, and G is a formula that does not contain x as a free variable.

Similarly, see Exercise 4.3.1.

Q.E.D.

Exercise 4.3.1. Verify that the axioms L₁₃ and L₁₅ are logically valid.

Lemma 4.3.2. From logically valid formulas, inference rules MP and Gen allow deriving only of logically valid formulas..

Proof.

1. Modus Ponens. Assume, B and B->C are logically valid formulas. By MP, we derive C. Assume, C is not logically valid, i.e., under some interpretation J, for some values of its free variables, C is false. Under this interpretation J, for these values of free variables of C, the formulas B and B->C are true. Then, according to the classical truth tables, C also must be true. Contradiction. Hence, C is logically valid.

2. Generalization. Assume, F(x) is logically valid, but AxF(x) is not, i.e., under some interpretation J, for some values of its free variables, AxF(x) is false. Hence, under this interpretation J, for these values of free variables of AxF(x), there is c in D_J such that F(c) is false. But F(x) is logically valid, i.e. F(c) is true. Contradiction. Hence, AxF(x) is logically valid.

Q.E.D.

Corollary 4.3.3. All the formulas that can be proved by using the classical logic [L₁-L₁₁, L₁₂-L₁₅, MP, Gen], are logically valid.

Proof. Immediately, by Lemmas 4.3.1 and 4.3.2.

Of course, this (the so-called soundness theorem) is the easy half of the completeness theorem. To complete the proof, we must prove the converse: if some formula is logically valid, then it can be proved by using the classical logic [L₁-L₁₁, L₁₂-L₁₅, MP, Gen].

Goedel's initial very complicated proof from 1929 was greatly simplified in 1947, when Leon Henkin observed in his Ph.D. thesis that the hard part of the proof can be presented as the Model Existence Theorem. The result was published in 1949:

L.Henkin. The completeness of the first-order functional calculus. "J. Symbolic Logic", 1949, vol.14, pp.159-166.

Henkin's proof was simplified by Gisbert Hasenjaeger in 1953:

G.Hasenjaeger. Eine Bemerkung zu Henkin's Beweis fuer die Vollstaendigkeit des Praedikatenkalkuels der ersten Stufe. "J. Symbolic Logic", 1953, vol.18, pp.42-48.

Henkin's Model Existence Theorem. If a first order classical formal theory is consistent (in the sense that, by using the classical logic, it does not prove contradictions), then there is a finite or countable model of this theory (i.e. an interpretation with a finite or countable domain, under which all axioms and theorems of the theory are always true).

This theorem solved a serious mental problem of anti-formalists. They thought that mere consistency of a theory (in the syntactic sense of the word - as the lack of contradictions) is not sufficient to regard it as meaningful - as a "theory of something". Model Existence Theorem says that (syntactic!) consistency of a theory is sufficient: if a theory does not contain contradictions, then it is a "theory of something" - it describes at least some kind of "mathematical reality". You may think that Euclidean geometry is "meaningless" - because it does not describe 100% correctly the spacial properties of the Universe. But it's your problem, not Euclid's - use another theory.

Let us assume the Model Existence Theorem (we will prove it later in this section).

Proof of the Completeness Theorem

Let us assume that some formula F in some first order language L is logically valid, yet it cannot be proved by using axioms and rules of the classical logic. Let us consider the theory T in the language L which contains (besides the logical axioms) only one non-logical axiom - the negation of F, i.e. the formula ~Ax₁...Ax_nF, where x₁, .., x_n are exactly all the free variables of F (if F contains free variables x₁, .., x_n, then, to negate its assertion, we must add the quantifiers Ax₁...Ax_n). Since F cannot be derived from the logical axioms, T is a consistent theory.

Indeed, if T would be inconsistent, i.e. we could prove in T some formula C and its negation ~C, then we had proofs of [L₁-L₁₁, L₁₂-L₁₅, MP, Gen] ~Ax₁...Ax_nF |- C, and ~Ax₁...Ax_nF |- ~C. Since ~Ax₁...Ax_nF is a closed formula, by Deduction Theorem 2, [L₁-L₁₁, L₁₂-L₁₅, MP, Gen] |- ~Ax₁...Ax_nF ->C, and |- ~Ax₁...Ax_nF ->~C. Now, by axiom L₉: (B->C)->(B->~C)->~B, we obtain that [L₁-L₁₁, L₁₂-L₁₅, MP, Gen] |- ~~Ax₁...Ax_nF. By the (classical) Double Negation Law, this implies [L₁-L₁₁, L₁₂-L₁₅, MP, Gen] |- Ax₁...Ax_nF, and by axiom L₁₂: AxB(x)->B(x) - [L₁-L₁₁, L₁₂-L₁₅, MP, Gen] |- F. But, by our assumption, F cannot be proved in [L₁-L₁₁, L₁₂-L₁₅, MP, Gen]. Hence, T is a consistent theory.

Now, by the Model Existence Theorem, there is a model of T, i.e. an interpretation J that makes all its axioms always true. Under this interpretation, the formula ~Ax₁...Ax_nF (as an axiom of T) is always true. On the other hand, since F is logically valid, it is always true under all interpretations, i.e. it is always true also under the interpretation J. Hence, formulas F and ~Ax₁...Ax_nF both are always true under J. This is impossible, hence, F must be provable from logical axioms. Q.E.D.

1. Such a simple proof seems almost impossible! We are proving that the logical axioms and rules of infernce are strong enough, but where come these axioms in? They come in - in the proof of the Model Existence Theorem. This theorem says that if some formal theory T does not have models, then the logical axioms and rules of inference are strong enough to derive a contradiction from the axioms of T. But the proof of the Model Existence Theorem we will consider below, is positive, not negative!

Exercise 4.3.2. a) Explain, how logical axioms are used in this (positive!) proof.

b) (Thanks to Sune Foldager for the idea.) Prove the following version of Goedel's Completeness Theorem: if T is a first order formal theory, and M is an interpretation where all the AXIOMS of T are true, and F is a formula that is true in M, then T proves F (i.e. F is true in M, iff F is a theorem of T).

2. The above simple proof seems extremely non-constructive! "If F is logically valid, then it can be proved [L₁-L₁₁, L₁₂-L₁₅, MP, Gen]". How could we obtain this proof? Still, how do we know that F is logically valid? Only, if we had a constructive procedure verifying that F is logically valid, we could ask for an algorithm converting such procedures into proofs in [L₁-L₁₁, L₁₂-L₁₅, MP, Gen]!

Lemma 4.3.4. In any first order language the set of all logically valid formulas is effectively denumerable. I.e. given a language L, we can write a computer program that (working ad infinitum) prints out all logically valid formulas of L.

Proof. Immediately from Exercise 1.1.4.

This makes Goedel's completeness theorem very significant: it shows that the "doubly non-constructive" notion of logically valid formula is at least 50% constructive!

Still, unfortunately, this notion is not 100% constructive. In 1936, Alonzo Church proved that at least some first order languages do allow an algorithm determining, is a given formula logically valid or not (i.e. an algorithm solving the famous Entscheidungsproblem - decision problem):

A.Church. A note on the Entscheidungsproblem. "Journal of Symb. Logic", 1936, vol.1, pp.40-41

After this, Laszlo Kalmar proved that, if a first order language contains at least one binary predicate letter, then it does not allow an algorithm determining, is a given formula logically valid or not. Thus, none of the serious first order languages allows such an algorithm (languages of PA and ZF included):

L.Kalmar. Die Zurueckfuehrung des Entscheidungsproblems auf den Fall von Formeln mit einer einzigen, binaeren Funktionsvariablen. "Compositio Math.", 1936, Vol.4, pp.137-144

For details, see Section 6.x, or Mendelson [1997]. Sometimes, this fact (the 50% constructiveness of the notion of the logical validity) is expressed a follows: the logical validity of first order formulas is semi-decidable.

Exercise 4.3.3. (For smart students). Prove Henkin's Model Existence Theorem by using the following smart ideas due to L.Henkin and G.Hasenjaeger. Let T be a consistent theory. We must build a model of T. What kind of "bricks" should we use for this "building"? Idea #1: let us use language constant letters! So, let us add to the language of T an infinite set of new constant letters d₁, d₂, d₃, ... (and adopt the corresponding additional instances of logical axioms). Prove that this extended theory T₀ is consistent. The model we are building must contain all "objects" whose existence can be proved in T₀. Idea #2: for each formula F of T₀ having exactly one free variable (for example, x) let us add to the theory T₀ the axiom ExF(x)->F(d_i), where the constant d_i is unique for each F. If T₀ proves ExF(x), then this constant d_i will represent in our model the "object" x having the property F. Prove that this extended theory T₁ is consistent. Idea #3: prove the (non-constructive) Lindenbaum's lemma: the axiom set of any consistent theory can be extended in such a way, that the extended theory is consistent and complete (the axiom set of the extended theory may be not effectively solvable). After this, extend T₁ to a consistent complete theory T₂. Idea #4: let us take as the domain of the interpretation M the set of all those terms of T₀ that do not contain variables. And let us interpret a function letter f as the "syntactic constructor function" f', i.e. let us define the value f'(t₁, ..., t_n) simply as the character string "f(t₁, ..., t_n)". Finally, let us interpret a predicate letter p as the relation p' such that p'(t₁, ..., t_n) is true in M, iff T₂ proves p'(t₁, ..., t_n). To complete the proof, prove that an arbitrary formula G is always true in M, iff T₂ proves G. Hence, all theorems of the initial theory T are always true in M.

Adolf Lindenbaum, 1904-1941? - logico, collaboratore e amico di Alfred Tarski (according to Matematici famosi). "No one knows what happened to Lindenbaum after his arrest by the Gestapo." (Marcel Guillaume, Mathematical Reviews, 2001c:03006).

Lindenbaum's Lemma. Any consistent first order theory can be extended to a consistent complete theory. More precisely, if T is a consistent first order theory, then, in the language of T, there is a set A of closed formulas such that T+A is a consistent complete theory. (In general, T+A is not a formal theory in the sense of Section 1.1, see below.)

Note. By T+A we denote the first order theory in the language of T, obtained from T by adding the formulas of the set A as non-logical axioms.

Exercise 4.3.4. Verify that, in any first order language L, only countably many formulas can be generated. I.e. produce an algorithm for printing out a sequence F₀, F₁, F₂, ... containing all the formulas of L.

Proof of the Lindenbaum's Lemma (Attention: non-constructive reasoning!)

Let us use the algorithm of the Exercise 4.3.4 printing out the sequence F₀, F₁, F₂, ... of all formulas in the language of T, and let us run through this sequence, processing only those formulas F_i that are closed.

At the very beginning, the set of new axioms A₀ is empty.

At the step i, we already have some set A_i-1 of new axioms. If the formula F_i is not closed, let us ignore it, and set A_i=A_i-1. Now, let us suppose that F_i is a closed formula. If T+A_i-1 proves F_i, or T+A_i-1 proves ~F_i, then we can ignore this formula, and set A_i=A_i-1. If T+A does not prove neither F_i, nor ~F_i, then let us simply add F_i (or ~F_i, if you like it better) to our set of new axioms, i.e. set A_i=A_i-1U{F_i}.

Etc., ad infinitum. As the result of this process we obtain a set of closed formulas A = A₀UA₁UA₂U... UA_iU....

Let us prove that T+A is a consistent complete theory.

Consistency. If T+A would be inconsistent, we would have a proof of [T+A] |- C&~C for some formula C. If, in this proof, no axioms from the set A would be used, we would have a proof of [T] |- C&~C, i.e. T would be inconsistent.

Otherwise, the proof of [T+A] |- C&~C could contain a finite number of axioms B₁, ..., B_k from the set A. Let us arrange these axioms in the sequence, as we added them to the set A. Thus we have a proof of [T]: B₁, ..., B_k |- C&~C. Let us recall Theorem 2.4.1(a):

If A₁, A₂, ..., A_n, B |- C&~C, then A₁, A₂, ..., A_n |- ~B.

Hence, we have a proof of [T]: B₁, ..., B_k-1 |- ~B_k. But this is impossible - we added B_k to the set A just because T+A_i-1 could not prove neither B_k, nor ~B_k. Q.E.D.

Completeness. We must verify that, for any closed formula F in the language of T, either T+A |- F, or T+A |- ~F. Let us assume, this is not the case for some closed formula F. Of course, F appears in the above sequence F₀, F₁, F₂, ... as some F_i. If neither T+A |- F, nor T+A |- ~F, then neither T+A_i-1 |- F_i, nor T+A_i-1 |- ~F_i. In such a situation we would add F to the set A, hence, we would have T+A |- F. Q.E.D.

This completes the proof of Lindenbaum's Lemma.

Attention: non-constructive reasoning! T+A is a somewhat strange theory, because, in general, we do not have an effective decision procedure for its axiom set. Indeed, to decide, is some closed formula F an axiom of T+A, or not, we must identify F in the sequence F₀, F₁, F₂, ... as some F_i, and after this, we must verify, whether T+A_i-1 proves F_i, or T+A_i-1 proves ~F_i, or none of these. Thus, in general, T+A is not a formal theory in the sense of Section 1.1.

Proof of the Model Existence Theorem (Attention: non-constructive reasoning!)

Inspired by the beautiful exposition in Mendelson [1997].

Step 1. We must build a model of T. What kind of "bricks" should we use for this "building"? Idea #1: let us use language constant letters! So, in order to prepare enough "bricks", let us add to the language of T a countable set of new constant letters d₁, d₂, d₃, ... (and extend the definitions of terms, atomic formulas and formulas accordingly, and add new instances of logical axioms accordingly). Let us prove that, if T is consistent, then this extended theory T₀ also is consistent.

If T₀ would be inconsistent, then, for some formula C, we could obtain a proof of [T₀]: |- C& ~C. If, in this proof, constant letters from the set {d₁, d₂, d₃, ...} would not appear at all, then, in fact, we had a proof of [T]: |- C&~C, i.e. we could conclude that T is inconsistent. But, if the new constant letters do appear in the proof of [T₀]: |- C& ~C? Then, let us replace these constant letters by any variables of T that do not appear in this proof (this is possible, since each first order language contains a countable set of variable letters). After these substitutions, the proof becomes a valid proofs of T, because:

a) The logical axioms remain valid.

b) The non-logical axioms of T do not contain the constants d₁, d₂, d₃, ..., i.e. they do not change.

c) Applications of inference rules MP and Gen remain valid.

Hence, [T]: |- C'&~C', where the formula C' has been obtained from C by the above substitutions. I.e., if T₀ would be inconsistent, then T also would be inconsistent.

Step 2. The model we are building must contain all "objects" whose existence can be proved in T₀. Idea #2: for each formula F of T₀ having exactly one free variable (for example, x) let us add to the theory T₀ the axiom ExF(x)->F(d_i), where the constant d_i is unique for each F. If T₀ proves ExF(x), then this d_i will represent in our model the "object" x having the property F. Let us prove that, if T is consistent, then this extended theory T₁ also is consistent. Note that in T₁ the same language is used as in T₀.

To implement the Idea #2 correctly, first let us use the algorithm of the Exercise 4.3.4 printing out the sequence F₀, F₁, F₂, ... of all formulas in the language of T₀, and let us run through this sequence, processing only those formulas F_i that have exactly one free variable. Let us assign to each such formula F_i a unique constant d_c(i) in such a way that d_c(i) does not appear neither in the non-logical axioms of T, nor in F_i, nor in the axioms EyF_j(y)->F_j(d_c(j)) for all formulas F_j preceding F_i in the sequence F₀, F₁, F₂, .... And, if x is the (only) free variable of F_i, let us adopt ExF_i(x)->F_j(d_c(i)) as an axiom of T₁.

Now, let us assume that the extended theory T₁ is inconsistent, i.e. that, for some formula C of T₀, we have a proof of [T₁]: |- C&~C. In these proofs, only a finite number n of axioms ExF(x)->F(d_c(F)) could be used. If n=0, then we have [T₀]: |- C&~C, i.e. then T₀ is inconsistent.

If n>0, then let us mark the axiom ExF(x)->F(d_c(F)) with F having the largest index in the sequence F₀, F₁, F₂, .... And, in the proof of [T₁]: |- C&~C, let us replace the constant c(F) by some variable y that does not appear in this proof (this is possible, since each first order language contains a countable set of variable letters). After this substitution, the proof remain a valid proof of T₁, because:

a) The logical axioms remain valid.

b) The non-logical axioms of T do not contain the constant c(F), i.e. they do not change.

c) The axiom ExF(x)->F(d_c(F)) becomes ExF(x)->F(y). Since F does not contain the constant c(F), the premise ExF(x) does not change.

d) The remaining n-1 axioms EyF_j(y)->F_j(d_c(j)) of T₁ do not contain the constant c(F), i.e. they do not change.

e) Applications of inference rules MP and Gen remain valid.

Thus we have now another proof of a contradiction - [T₁]: |- C'&~C', where the formula C' has been obtained from C by substituting y for c(F). Let us recall Theorem 2.4.1(a):

If A₁, A₂, ..., A_n, B |- C&~C, then A₁, A₂, ..., A_n |- ~B.

Let us take the formula ExF(x)->F(y) for B, and C'- for C. Thus, there is a proof of ~(ExF(x)->F(y)), where only logical axioms, non-logical axioms of T, and the remaining n-1 axioms EyF_j(y)->F_j(d_c(j)) of T₁ are used. Let us recall the Exercise 2.6.3(b) [L₁-L₁₁, MP]: |- ~(A->B) <-> A&~B. Thus, ~(ExF(x)->F(y)) is equivalent to ExF(x)&~F(y), and, in fact, we have a proof of ExF(x), and a proof of ~F(y). By applying Gen to the second formula, we obtain a proof of Ay~F(y), which is equivalent to ~EyF(y) (indeed, let us recall Section 3.2, Table 3.2, Group IV, constructively, |- Ax~B<->~ExB). By Replacement Theorem 3, ~EyF(y) is equivalent to ~ExF(x). Thus, we have a proof of a contradiction ExF(x)&~ExF(x), where only logical axioms, non-logical axioms of T, and the remaining n-1 axioms EyF_j(y)->F_j(d_c(j)) of T₁ are used.

Let us repeat the above chain of reasoning another n-1 times to eliminate all occurrences of the axioms ExF(x)->F(d_c(F)) from our proof of a contradiction. In this way we obtain a proof of a contradiction in T₀, which is impossible (see Step 1). Hence, T₁ is a consistent theory.

Step 3. Idea #3: let us use the (non-constructive!) Lindenbaum's lemma, and extend T₁ to a consistent complete theory T₂. Note that in T₂ the same language is used as in T₀.

Step 4. Let us define an interpretation M of the language of T₀, in which all theorems of T₂ will be always true. Since all theorems of the initial theory T are theorems of T₂, this will complete our proof.

Idea #4: let us take as the domain D_M of the interpretation M the (countable! - verify!) set of all constant terms of T₀, i.e. terms that do not contain variables (this set of terms is not empty, it contains at least the countable set of constant letters added in Step 1). And let us define interpretations of constant letters, function letters and predicate letters as follows.

a) The interpretation of each constant letter c is the letter c itself.

b) The interpretation of a function letter f is the "syntactic constructor function" f', i.e., if f is an n-ary function letter, and t₁, ..., t_n are constant terms, then the value f'(t₁, ..., t_n) is defined simply as the character string "f(t₁, ..., t_n)" (quotation marks ignored).

c) The interpretation of a predicate letter p is the relation p' such, if p is an n-ary predicate letter, and t₁, ..., t_n are constant terms, then p'(t₁, ..., t_n) is defined as true in M, iff T₂ proves p(t₁, ..., t_n) (note that T₂ is a consistent complete theory, i.e. it proves either p(t₁, ..., t_n), or ~p(t₁, ..., t_n), but not both!).

Step 5. To complete the proof, we must prove that, in the language of T₀, an arbitrary formula G is always true in M, iff T₂ proves G (let us denote this, as usual, by T₂ |- G. This will be proved, if we will prove that, if x₁, ..., x_m is the set of at least all free variables contained in the formula G, and t₁, ..., t_m are constant terms, then G(t₁, ..., t_m) is true in M, iff T₂ |- G(t₁, ..., t_m). The proof will be by induction.

Induction base: G is an atomic formula p(s₁, ..., s_n), where p is a predicate letter, and the terms s₁, ..., s_n contain some of the variables x₁, ..., x_m. In s₁, ..., s_n, let us substitute for x₁, ..., x_m the terms t₁, ..., t_m respectively. In this way we obtain constant terms s'₁, ..., s'_n. Thus G(t₁, ..., t_m) is simply p(s'₁, ..., s'_n). By definition (see Step 4), p(s'₁, ..., s'_n) is true, iff T₂ |- p(s'₁, ..., s'_n), i.e., iff T₂ |- G(t₁, ..., t_m). Q.E.D.

Induction step.

Note. Since, T₂ is a complete consistent theory, for any closed formula F, T₂ proves either F, or ~F (but not both). Hence, if we know that F is true in M, iff T₂ |- F, then we can conclude that F is false in M, iff T₂ |- ~F. Indeed, if F is false, then F is not true, i.e. T₂ does not prove F, i.e. T₂ |- ~F. And, if T₂ |- ~F, then T₂ does not prove F, i.e. F is not true, i.e. F is false. And conversely: if we know that F is false in M, iff T₂ |- ~F, then we can conclude that F is true in M, iff T₂ |- F. Indeed, if F is true, then ~F is not true, i.e. T₂ does not prove ~F, i.e. T₂ |- F. And, if T₂ |- F, then T₂ does not prove ~F, i.e. F is not false, i.e. F is true.

Case 1: G is ~H. Then, according to the classical truth tables, G(t₁, ..., t_m) is true in M, iff H(t₁, ..., t_m) is false in M. By induction assumption, H(t₁, ..., t_m) is true in M, iff T₂ |- H(t₁, ..., t_m). Then, by the above note, since H(t₁, ..., t_m) is a closed formula, H(t₁, ..., t_m) is false in M, iff T₂ |- ~H(t₁, ..., t_m), i.e., iff T₂ |- G(t₁, ..., t_m). Q.E.D.

Case 2: G is H->K. Then, according to the classical truth tables, G(t₁, ..., t_m) is false in M, iff H(t₁, ..., t_m) is true in M, and K(t₁, ..., t_m) is false in M. By induction assumption, H(t₁, ..., t_m) is true in M, iff T₂ |- H(t₁, ..., t_m), and K(t₁, ..., t_m) is true in M, iff T₂ |- K(t₁, ..., t_m). By the above note, K(t₁, ..., t_m) is false in M, iff T₂ |- ~K(t₁, ..., t_m). Hence,

G(t₁, ..., t_m) is false in M, iff T₂ |- H(t₁, ..., t_m), and T₂ |- ~K(t₁, ..., t_m),

or,

G(t₁, ..., t_m) is true in M, iff not (T₂ |- H(t₁, ..., t_m), and T₂ |- ~K(t₁, ..., t_m)).

Let us recall Theorem 2.2.1: a) [L₅, MP] A, B |- A&B, b) [L₃, L₄, MP]: A&B |- A, A&B |- B, and Exercise 2.6.3(a), [L₁-L₁₁, MP]: |- (A->B) <-> ~(A&~B). In T₂, all the axioms of the classical logic are adopted, hence (verify!),

G(t₁, ..., t_m) is true in M, iff T₂ |- H(t₁, ..., t_m)->K(t₁, ..., t_m),

or, G(t₁, ..., t_m) is true in M, iff T₂ |- G(t₁, ..., t_m). Q.E.D.

Case 3: G is H&K. Then, according to the classical truth tables, G(t₁, ..., t_m) is true in M, iff H(t₁, ..., t_m) is true in M, and K(t₁, ..., t_m) is true in M. By induction assumption, H(t₁, ..., t_m) is true in M, iff T₂ |- H(t₁, ..., t_m), and K(t₁, ..., t_m) is true in M, iff T₂ |- K(t₁, ..., t_m). Let us recall Theorem 2.2.1: a) [L₅, MP] A, B |- A&B, b) [L₃, L₄, MP]: A&B |- A, A&B |- B. In T₂, all the axioms of the classical logic are adopted, hence (verify!),

G(t₁, ..., t_m) is true in M, iff T₂ |- H(t₁, ..., t_m)&K(t₁, ..., t_m),

or, G(t₁, ..., t_m) is true in M, iff T₂ |- G(t₁, ..., t_m). Q.E.D.

Case 4: G is HvK. Then, according to the classical truth tables, G(t₁, ..., t_m) is false in M, iff H(t₁, ..., t_m) is false in M, and K(t₁, ..., t_m) is false in M. By induction assumption, and by the above note, H(t₁, ..., t_m) is false in M, iff T₂ |- ~H(t₁, ..., t_m), and K(t₁, ..., t_m) is false in M, iff T₂ |- ~K(t₁, ..., t_m). Let us recall Theorem 2.2.1: a) [L₅, MP] A, B |- A&B, b) [L₃, L₄, MP]: A&B |- A, A&B |- B, and Theorem 2.4.10(b): [L₁-L₁₀, MP] |- ~(AvB) <-> ~A&~B (the so-called Second de Morgan Law). In T₂, all the axioms of the classical logic are adopted, hence (verify!),

G(t₁, ..., t_m) is false in M, iff T₂ |- ~(H(t₁, ..., t_m)vK(t₁, ..., t_m)),

or, G(t₁, ..., t_m) is false in M, iff T₂ |- ~G(t₁, ..., t_m). Thus, by the above note, G(t₁, ..., t_m) is true in M, iff T₂ |- G(t₁, ..., t_m). Q.E.D.

Case 5: G is ExH. Then, by definition, G(t₁, ..., t_m) is true in M, iff H(x, t₁, ..., t_m) is "true for some x", i.e., iff H(t, t₁, ..., t_m) is true in M for some constant term t in M. By induction assumption, H(t, t₁, ..., t_m) is true in M, iff T₂ |- H(t, t₁, ..., t_m). Let us recall our above Step 2. Since H(x, t₁, ..., t_m) is a formula containing exactly one free variable, in T₂ we have an axiom ExH(x, t₁, ..., t_m)->H(c_H, t₁, ..., t_m), where c_H is a constant letter.

First, let us assume that G(t₁, ..., t_m) is true in M. Then H(t, t₁, ..., t_m) is true in M for some constant term t in M, hence, T₂ |- H(t, t₁, ..., t_m) for this particular t. Let us recall the axiom L₁₃: F(t)->ExF(x). Since t is a constant term, this axiom is valid for t. We need the following instance of L₁₃: H(t, t₁, ..., t_m)->ExH(x, t₁, ..., t_m). In T₂, all the axioms of the classical logic are adopted, hence, T₂ |- H(t, t₁, ..., t_m)->ExH(x, t₁, ..., t_m), and, by MP, T₂ |- ExH(x, t₁, ..., t_m), i.e. T₂ |- G(t₁, ..., t_m). Q.E.D.

Now, let us assume that T₂ |- G(t₁, ..., t_m), i.e. T₂ |- ExH(x, t₁, ..., t_m). By the above-mentioned axiom, T₂ |- ExH(x, t₁, ..., t_m)->H(c_H, t₁, ..., t_m), where c_H is a constant letter. Thus, by MP, T₂ |- H(c_H, t₁, ..., t_m). Since c_H is a constant term, by induction assumption, if T₂ |- H(c_H, t₁, ..., t_m), then H(c_H, t₁, ..., t_m) is true in M. Hence, H(c_H, t₁, ..., t_m) is true in M, i.e. H(x, t₁, ..., t_m) is true "for some x", i.e. ExH(x, t₁, ..., t_m) is true in M, i.e. G(t₁, ..., t_m) is true in M. Q.E.D.

Case 6: G is AxH. By definition, G(t₁, ..., t_m) is true in M, iff H(x, t₁, ..., t_m) is "true for all x", i.e., iff H(t, t₁, ..., t_m) is true in M for all constant terms t in M. By induction assumption, H(t, t₁, ..., t_m) is true in M, iff T₂ |- H(t, t₁, ..., t_m).

Let us prove that G(t₁, ..., t_m) is false in M, iff T₂ |- Ex~H(x, t₁, ..., t_m).

First, let us assume that G(t₁, ..., t_m) is false in M. Then H(t, t₁, ..., t_m) is false in M for some constant term t in M. By induction assumption, and by the above note, T₂ |- ~H(t, t₁, ..., t_m). As in the Case 5, let us recall the axiom L₁₃: ~H(t, t₁, ..., t_m)->Ex~H(x, t₁, ..., t_m). In T₂, all the axioms of the classical logic are adopted, hence, by MP, T₂ |- Ex~H(x, t₁, ..., t_m).

Now, let us assume that T₂ |- Ex~H(x, t₁, ..., t_m). As in the Case 5, let us recall the axiom Ex~H(x, t₁, ..., t_m)->~H(c_~H, t₁, ..., t_m), where c_~H is a constant letter. Hence, by MP, T₂ |- ~H(c_~H, t₁, ..., t_m), i.e. T₂ does not prove H(c_~H, t₁, ..., t_m). Then, by induction assumption, H(c_~H, t₁, ..., t_m) is false in M, i.e. AxH(x, t₁, ..., t_m) is false in M, i.e G(t₁, ..., t_m) is false in M.

Thus, we know that G(t₁, ..., t_m) is true in M, iff T₂ does not prove Ex~H(x, t₁, ..., t_m). Since T₂ is a complete theory, G(t₁, ..., t_m) is true in M, iff T₂ |- ~Ex~H(x, t₁, ..., t_m). Now, let us recall from Section 3.2, Table 3.2, Group I, [L₁-L₁₁, L₁₂-L₁₅, MP, Gen]: |- ~Ex~B<->AxB. In T₂, all the axioms of the classical logic are adopted, hence, T₂ |- ~Ex~H(x, t₁, ..., t_m), iff T₂ |- AxH(x, t₁, ..., t_m), i.e. G(t₁, ..., t_m) is true in M, iff T₂ |- G(t₁, ..., t_m). Q.E.D.

This completes the proof of the Model Existence Theorem. Q.E.D.

Attention: non-constructive reasoning! The above construction of the model M seems to be "almost constructive". The domain D_M consists of all constant terms from the language of T₀. The axiom set of T₁ is effectively solvable (verify!). The interpretations of function letters are computable functions (verify!). But the interpretations of predicate letters? We interpreted the predicate letter p as the relation p' such that p'(t₁, ..., t_n) is true, iff T₂ proves p(t₁, ..., t_n). This would be, in general, effectively unsolvable (see Section ZZ), even if the axiom set of T₂ would be solvable! But, in general, the axiom set of theory T₂ (obtained by means of Lindenbaum's Lemma) is not effectively solvable! Thus, our construction of the model M is essentially non-constructive.

Exercise 4.3.5. (For smart students) Determine the "degree of non-constructiveness" of the Model Existence Theorem. (Hint: prove that it is DELTA₂, i.e. that all the necessary functions are "computable in the limit". A function f(x) is called computable in the limit, iff there is a computable function g(x,y) such that, for all x, f(x) = lim g(x,y) as y->infinity.)

Consistency and Satisfiability

A set of formulas F₁, ..., F_n is called inconsistent, iff a contradiction (i.e. a formula B&~B) can be derived from it. For example, the set {B, B->C, C->~B}is inconsistent (verify).

The Model Existence Theorem allows to connect the notions of consistency and satisfiability.

Exercise 4.3.6. Verify, that a set of formulas in a first order language: a) is consistent in the classical logic, iff it is satisfiable, b) is inconsistent in the classical logic, iff it is unsatisfiable. (Hint: use the result of Exercise 4.1.3).

Skolem's Paradox

Initially, the Model Existence Theorem has been proved in a weaker form in 1915 (by Leopold Loewenheim) and 1919 (by Thoralf Skolem): if a first order theory has a model, then it has a finite or countable model (the famous Loewenheim-Skolem theorem). Proof (after 1929): if T has a model, then T is consistent, i.e. T has a finite or countable model.

L.Loewenheim. Ueber Moeglichkeiten im Relativkalkuel. "Mathematische Annalen", 1915, Vol.76, pp.447-470 (see also http://thoralf2.uwaterloo.ca/htdocs/scav/lowen/lowen.html)

Th. Skolem. Logisch-kombinatorische Untersuchungen �ber die Erf�llbarkeit und Beweisbarkeit mathematischen S�tze nebst einem Theoreme �ber dichte Mengen. Videnskabsakademiet i Kristiania, Skrifter I, No. 4, 1920, pp. 1-36 (see also http://thoralf2.uwaterloo.ca/htdocs/scav/skolem/skolem.html)

Loewenheim-Skolem theorem (and the Model Existence theorem) is steadily provoking the so-called Skolem's Paradox, first noted by Skolem in 1922:

Th. Skolem. Einige Bemerkungen zur axiomatischen Begruendung der Mengenlehre. Matematikerkongressen i Helsingfors den 4-7 Juli 1922, Den femte skandinaviska matematikerkongressen, Redog�relse, Akademiska Bokhandeln, Helsinki, 1923, pp. 217-232.

Indeed, in all formal set theories (for example, in ZF) we can prove the existence of uncountable sets. Still, according to the Model Existence theorem, if our formal set theory consistent, then there is a countable model where all its axioms and theorems are true. I.e. a theory proves the existence of uncountable sets, yet it has a countable model! Is this possible? Does it mean that all formal set theories are inconsistent? Platonists could say even more: any consistent axiomatic set theory has countable models, hence, no axiom system can represent the "intended" set theory (i.e. "the" Platonist "world of sets") adequately.

For a formalist, Skolem's Paradox is not a paradox at all. I would rather call it Skolem's effect - like as the photo-effect, it is simply a striking phenomenon. Indeed, let J be a countable model of our formal set theory. In this theory, we can prove that the set r of all real numbers is uncountable, i.e.

~Ef (f is 1-1 function from r into w), -----------(1)

where w is the set of all natural numbers. What is the meaning of this theorem in the countable model J? Interpretations of r and w are subsets of the domain D_J, i.e. they both are countable sets, i.e.

Ef (f is 1-1 function from r_J into w_J). ----------(2)

Interpretation of (1) in J is

~Ef((f in D_J) & (f is 1-1 function from r_J into w_J)).

Hence, the mapping f of (2) does exist, yet it exists outside the model J! Do you think that f of (2) "must" be located in the model? Why? If you are living (as an "internal observer") within the model J, the set r_J seems uncountable to you (because you cannot find a 1-1 function from r_J into w_J in your world J). Still, for me (an "external observer") your uncountable r_J is countable - in my world I have a 1-1 function from r_J into w_J!

Hence, indeed, Skolem's Paradox represents simply a striking phenomenon. It is worth of knowing, yet there is no danger in it.

Back to title page

model theory, interpretation, completeness theorem, Post, truth table, truth, Skolem, table, paradox, model, satisfiable, completeness, Skolem paradox, formula, logically valid, true, false, satisfiability