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 and Models

First, let us recall the beginning part of Section 1.2:

The vision behind the notion of predicate languages is centered on the so-called "domain" - a (non-empty?) collection of "objects", their "properties" and "relations" between them, that we wish to "describe" (or "define"?) by using the language.

...

Thus, the first kind of language elements we will need are object variables (or simply, variables, an unlimited number of them):

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 object constants - symbols denoting some specific "objects" of our "domain".

...

In some languages we may need also the so-called function constants - 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 constants - symbols denoting specific properties (of) or relations between "objects" of our "domain".

...

Thus, the specification of a particular predicate language includes the following primitives:

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

2) An empty, finite, or countable set of object constants.

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

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

Different sets of primitives yield different predicate languages.

By using the language primitives, we can build terms, atomic formulas and (compound) formulas. The remaining part of the language definition is common for all predicate languages.

...

... 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 an object variable, then (AxB) and (ExB) also are formulas.

...

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

Each first order theory T includes:

a) a specific predicate 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 "syntax" - axioms and rules of inference. And this is the only way of doing mathematics for computers! But how about "semantics" - about our intended "vision behind our predicate language"? Is it only a vision, or it could be defined precisely? For a particular predicate language - is there only one such vision possible? Trying to answer these questions, we arrive at 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. In model theory, we investigate formal theories by using set theory as a meta-theory.

Paul Bernays, in 1958: "As Bernays remarks, syntax is a branch of number theory and semantics the one of set theory." See p. 470 of
Hao Wang. EIGHTY YEARS OF FOUNDATIONAL STUDIES. Dialectica, Vol. 12, Issue 3-4, pp. 466-497, December 1958 (available online at Blackwell Synergy).

In Sections 4.1-4.3 we will develop model theory for the classical logic, and in Sections 4.4-4.5 - model theory for the constructive logic.

In the classical model theory, we will replace our vague "visions behind predicate languages" by relatively well-defined mathematical structures - the so-called interpretations. As we will see, interpretations are allowed to be non-constructive.

Technically, an interpretation will be a relatively well-defined way of assigning "precise meanings" to all formulas of a predicate language. Any particular predicate language allows multiple ways of assigning "precise meanings" to its formulas - multiple interpretations.

For example, let us considered the language of first order arithmetic (language primitives: x, y, ..., 0, 1 +, *, =), and the following "Boolean vision" B behind it.

a) As the domain of B (the "target" set of objects), instead of the set of all natural numbers, let us consider the set of "Boolean values" D_B = {t, f}. Thus, under the variables x, y, ... can take only values t, f.

b) The interpretation mapping int_B assigns: to the object constant 1 - the object t, to the object constant 0 - the object t, thus: int_B(0)=f, int_B(1)=t.

c) To the function constant "+" we assign the well-known disjunction truth table: int_B(+)=v, to the function constant "*" - the well-known conjunction truth table: int_B(*)=&.

d) To the predicate constant "=" - the equality predicate for the set D_B, i.e. int_B(=) = {(t, t) , (f, f)}.

Is this vision "worse" than the usual one involving natural numbers? It seems, it is worse, because the following axiom of arithmetic:

x+1=y+1 -> x=y

is false under this vision. Indeed, set x=0 and y=1: 0+1=1+1 -> 0=1. Here, the premise is true: 0+1 = f v t = t = 1, 1+1 = t v t = t = 1, but the conclusion is not: 0=1 means f=t.

On the other hand, the following theorem of Boolean algebra:

x+x=x

is true under the above "Boolean vision" (t v t = t, f v f = f), but it is false under the usual vision involving natural numbers.

Thus, if two theories share the same language (as do Boolean algebra and first order arithmetic), then the "validity" of a vision depends on the formulas (axioms and theorems) that we expect to be true. If we consider only a language, then many different and even strange interpretations-visions will be possible. But if we consider a theory (i.e. a language plus specific axioms), then only a part of the interpretations-visions will be valid - only those ones, under which the specific axioms of our theory will be true. Such interpretations-visions are called models of the theory.

Another example: in our "language for people" we used names of people (John, Paris, ...) as object constants and the following predicate constants:
Male(x) - means "x is a male";
Female(x) - means "x is a female";
Mother(x, y) - means "x is mother of y";
Father(x, y) - means "x is father of y";
Married(x, y) - means "x and y are married";
x=y - means "x an y are the same person".

Now, let us fix the list of names: Britney, John, Paris, Peter, and let us consider the following interpretation J of the language:
a) The domain - and the range of variables - is D_J = {br, jo, pa, pe} (4 character strings).
b) int_J(Britney)=br, int_J(John)=jo, int_J(Paris)=pa, int_J(Peter)=pe.
c) int_J(Male) = {jo, pe}; int_J(Female) = {br, pa}.
d) int_J(Mother) = {(pa, br), (pa, jo)}; int_J(Father) = {(pe, jo), (pe, br)}.
e) int_J(Married) = {(pa, pe), (pe, pa)}.
f) d) int_J(=) = {(br, br), (jo, jo), (pa, pa), (pe, pe)}.

Under this interpretation, it is true that, "mothers are females", and that "all fathers are married people" (under this interpretation!), but it not true that "each person possess a mother".

Interpretation of a language - the specific part

Let L be a predicate language containing object constants c₁, ..., c_k, ... , function constants f₁, ..., f_m, ..., and predicate constants p₁, ..., p_n, .... An interpretation J of the language L consists of the following two entities:

a) A non-empty set D_J - the domain of interpretation (it will serve first of all as the range of object variables). Your favorite set theory comes in here.

b) A mapping int_J that assigns:

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

- to each function constant 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),

- to each predicate constant 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).

Thus, in a sense, the mapping int_J assigns "meaning" to the language primitives.

The most polular example - let us consider the so-called standard interpretation S of first order (Peano) arithmetic PA:

a) The domain is D_S = {0, 1, 2, ...} - the set of all natural numbers "as we know it" (more precisely - as you define it in your favorite set theory).

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

Yet another interpretation J1 of the same language:

a) The domain is D_J1 = {e, a, aa, aaa, ...} - the set of all strings built of the letter "a" (e is the empty string).

b) The mapping int_J1 assigns: to the object constant 0 - the empty string e, to the object constant 1 - the string "a", to the function constant "+" - the concatenation function of strings, to the function constant "*" - y times concatenation of x, to the predicate constant "=" - the string equality predicate.

Yet another interpretation J2 (there is no way to disqualify it as a formally correct interpretation of the language):

a) The domain is D_J2 = {o} - a single object o.

b) The mapping int_J2 assigns: to the object constant 0 - the object o, to the object constant 1 - the same object o, to the function constant "+" - the only possible function f(o)=o, to the function constant "*" - the only possible function f(o)=o, to the predicate constant "=" - the predicate {(o, o)}.

Some time later, we will use non-logical axioms to disqualify (at least some of) such "inadequate" interpretations.

Having an interpretation J of the language L, we can define the notion of true formulas (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 object constants, or object variables, or their combinations by means of function constants. 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 (1+1)+1 is the number 3, the interpretation of (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 constants may be non-computable functions. But, if they are all computable, then we can compute the "value" of any term t for any combination of values of variables appearing in t.

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, if and only if 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 constants may be non-computable predicates. But, if they were all computable, then we could compute the "truth value" of any atomic formula F for any combination of values of variables appearing in F.

Interpretations of languages - the standard common part

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 well-known classical truth tables from Section 4.2 below).

b) The formula AxB is true under J, if and only if B(c) is true under J for all members c of the domain D_J.

c) The formula ExB is true under J, if and only if there is a member c of the domain D_J such that B(c) is true under J.

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 under J" 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 100% 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? 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 concentrate on non-empty domains only.

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

Three Kinds of Formulas

If one explores some formula F of the language L in various interpretations, then three situations are possible:

a) F is true in all interpretations of the language L. Formulas of this kind are called logically valid formulas.

b) F is true in some interpretations of L, and false - in some other interpretations of L.

c) F is false in all interpretations of L (then, of course, ~F is true in all interpretations). Formulas of this kind are called unsatisfiable formulas.

Formulas that are "not unsatisfiable" (i.e. formulas of kinds (a) and (b)) are called, of course, satisfiable formulas.

they are true in the above-mentioned standard interpretation S of first order arithmetic.

Exercise 4.1.1. Verify that: a) F is satisfiable, if and only if ~F is not logically valid. b) F is logically valid, if and only if ~F is unsatisfiable.

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)),

Ax(G(x)&H(x)) -> (AxG(x)&AxH(x)),

Ex(G(x)vH(x)) -> (ExG(x)vExH(x)).

Such formulas are called logically valid. More precisely, in a predicate language L, a formula is called logically valid, if and only if 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 of its "meaning" - the interpretations of constants, functions and predicates used in it. But note that here, the (classical!) interpretations of propositional connectives and quantifiers remain fixed.

Important - non-constructivity! 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 we will see in Section 4.3, all the axioms of our classical logical axiom system [L₁-L₁₅, MP, Gen] are logically valid formulas. And that inference rules MP and Gen generate only logically valid formulas. Hence, all the formulas that can be proved in the classical logic [L₁-L₁₅, MP, Gen], are logically valid.

As an example, let us verify that the axiom L₁₂: AxF(x)->F(t) is logically valid. Let us assume the contrary, i.e. 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, if and only if 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), 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.2. Verify that the remaining 6 of the above 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.)

Is our classical logical axiom system [L₁-L₁₅, MP, Gen] powerful enough to prove ALL logically valid formulas? The answer is positive - see Goedel's Completeness Theorem in Section 4.3.

But, of course, there are formulas that are not logically valid. For example, negations of logically valid formulas are false in all interpretations, i.e. they are not logically valid. Such formulas are called unsatisfiable formulas. But there are formulas that are true in some interpretations, and false - in some other ones. An example of such formulas: the axiom of arithmetic x+1=y+1 -> x=y considered above.

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 constants). 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. the premise Ax(p(x) v q(x)) is true. But the formulas Ax p(x), Ax q(x) both are false. Hence, in this interpretation, the consequent Ax p(x) v Ax q(x) is false, and thus, 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.3. Verify that the following formulas are not logically valid (p, q, r are predicate constants):

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) v r(x)) -> (Ax p(x) v Ax 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)).

Exercise 4.1.4. Is the following formula logically valid, or not (p, q are predicate constants): (Ex p(x)->Ex q(x))->Ex(p(x)->q(x)). (Hint: follow the above example - use natural numbers or other objects trying to build an interpretation J such that the formula under question is false for some values of its free variables.)

Satisfiability

Recall that, in a predicate language L, a formula is called logically valid, if and only if it is true in all interpretations of the language L for all values of its free variables. Let us consider a "weaker" notion - the so-called "satisfiability": a formula will be called satisfiable, if it is not "completely wrong", i.e. if it can be "made true" by an appropriate choice of interpretation. More precisely:

In a predicate language L, a formula F is called satisfiable, if and only if there is an interpretation of the language L such that F is true for some values of its free variables (we will say also that F is satisfied under this interpretation). A set of formulas F₁, ..., F_n, ... is called satisfiable, if and only if there is an interpretation under which the formulas F₁, ..., F_n, ... are satisfied simultaneously.

Examples. a) Formula Ex p(x) is, of course, not logically valid, but it is satisfiable, because it is true in the following interpretation J: D_J={b}, p(b) is true.

b) Formulas x*0=0, x+y=y+x and x+(y+z)=(x+y)+z are not logically valid (see Exercise 4.1.7 below), but they are satisfiable, because

Exercise 4.1.5. 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 constant).

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 constants).

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

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

Logical Consequences

"F implies G", or "the formula G follows from the formula F" - what should this mean in general? If F is true, then G is true? Always, or under some specific conditions? Let us specify all these "conditions" as formulas A₁, ..., A_n. Then, G follows from A₁, ..., A_n unconditionally ("logically"), i.e. if A₁, ..., A_n are all true, then G must be true without any other conditions. Since the notion of "true" we have formalized as "true in interpretation", we can formalize the notion of "logical consequence" as follows:

G is a logical consequence of A₁, ..., A_n, if and only if G is true under any interpretation, under which A₁, ..., A_n are all true.

Or, as follows:

G is a logical consequence of A₁, ..., A_n, if and only if G is true in any model of A₁, ..., A_n.

Or, as follows:

G is a logical consequence of A₁, ..., A_n, if and only if the formula A₁& ..&A_n->G is logically valid.

(Verify that these three versions are equivalent).

Exercise 4.1.6. Verify that:

a) If the set of formulas A₁, ..., A_n is satisfiable, then the formulas B, ~B cannot both be logical consequences of A₁, ..., A_n.

b) The formula G is a logical consequence of formulas A₁, ..., A_n, if and only if the set A₁, ..., A_n, ~G is unsatisfiable.

Theories and Their Models

If T is a first order theory, and J is an interpretation of its language, and if J makes true the specific axioms of T, then (traditionally) J is called a model of T.

For non-mathematical people, the term "model of a theory" may seem somewhat strange: in "normal" branches of science, theories serve as a basis for building models of natural phenomena, technical devices etc. But only the term is strange ("upside down") here, the process is the same as in "normal" branches of science: first order theories "generate" their models, and these models can be used for modeling natural phenomena, technical devices etc.

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 - it is a proper subclass of all the possible interpretations. 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 and x will be equal! Logically valid formulas must be true under all interpretations!

Exercise 4.1.7. a) Verify that, if a theory has a model, then the set of its specific axioms is satisfiable.
b)Verify that x=x, x*0=0, x+y=y+x and x+(y+z)=(x+y)+z are satisfiable, but not logically valid formulas.

In a sense, logically valid formulas "do not contain information" - just because they are true in all interpretations, i.e. they are true independently of the "meaning" of language primitives. 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 get more about zero and addition after reading them? Another example: 2*2=5 -> 2*2=5, or 2*2=4 -> 2*2=4, these formulas also are logically valid, but do they help in computing the value of 2*2? Specific axioms of a theory T, on the contrary, do "contain information" - they separate a proper subclass of all interpretations - models of T.

Do the axioms of first order arithmetic separate the standard interpretation S, i.e. are the axioms of first order arithmetic true in this interpretation only? No, there are many non-standard interpretations making these axioms true! More: Non-standard arithmetic in Wikipedia.

Transitive predicates and recursion

Le tus return to the problem that we considered already in Section 1.2.

How about the predicate Ancestor(x, y) - "x is an ancestor of y"? Could it be expressed as a formula of our "language for people"? The first idea - let us "define" this predicate recursively:

AxAy(Father(x, y) v Mother(x, y) -> Ancestor(x, y));
AxAyAz(Ancestor(x, y) & Ancestor(y, z) -> Ancestor(x, z)).

The second rule declares the transitivity property of the predicate. The above two formulas are axioms, allowing to derive essential properties of the predicate Ancestor(x, y). But how about a single formula F(x, y) in the "language for people", expressing that "x is an ancestor of y"? Such a formula should be a tricky combination of formulas Father(x, y), Mother(x, y) and x=y. And such a formula is impossible! See Carlos Areces. Ph.D. Thesis, 2000, Theorem 1.2.

Exercise 4.1.8 (for smart students). Explain the precise meaning of the statement: in the "language for people", formula F(x, y) expresses that "x is an ancestor of y".

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).

As the first step, let us try answering the question: is the "intended meaning" of logical connectives (conjunction, disjunction, implication and negation) represented properly in our propositional axioms L₁-L₁₁? Let us investigate possible interpretations of 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, if and only if ~(B&~C) is true (or: B->C is false. if and only if B is true, and C is false).

If we agree that the above classical truth tables represent the "intended meaning" of logical connectives, we can move forward by proving

Lemma 4.2.1. Under the 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₉.

See also:
"Truth Tables" from The Wolfram Demonstrations Project
 http://demonstrations.wolfram.com/TruthTables/. Contributed by: Hector Zenil.

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 (i.e. b) of Theorem 4.2.4) was first proved by Emil L. Post in his 1920 Ph.D. thesis:

E. Post. Introduction to a general theory of elementary propositions. American Journal of Mathematics, 1921, vol. 43, pp.163-185.

About the history, see also:

Richard Zach. Completeness before Post: Bernays, Hilbert, and the development of propositional logic. The Bulletin of Symbolic Logic, 1999, vol. 5, N3, pp.331-366 (online copy available).

Following an elegant later idea by Laszlo Kalmar we need two simple 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 the 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 the 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,

their, in a sense, "final" version of the axioms of 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
See also:
Hilbert and Ackermann's 1928 Logic Book by Stanley N. Burris).

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 predicate language, a formula is logically valid, if and only if it can be proved by using the classical logic [L₁-L₁₁, L₁₂-L₁₅, MP, Gen].

In fact, a more general theorem can be proved:

Theorem 4.3.0 (Thanks to Sune Foldager for the idea.). If T is a first order theory with classical logic, then some formula F is always true in all models of T, if and only if T proves F.

Goedel's Completeness Theorem follwos from Theorem 4.3.0, if the set of specific axioms of T is empty.

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 the 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, if and only if 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), 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, if and only if 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 (soundness of the classical predicate logic). 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.

Exercise 4.3.1X. Verify that if, under an interpretation J, all specific axioms of a theory T are true, then all theorems of T also are true under J. (Hint: each theorem C is proved by using some finite set of specific axioms, let us denote by B the conjunction of these axioms, consider the formula B->C, and use Corollary 4.3.3.)

Of course, the above soundness theorem is the easy half of Goedel's 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 generalized, simplified and best presented as the so-called 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.

See also Henkin's later account of his discovery:

L. Henkin. The discovery of my completeness proofs. "The Bulletin of Symbolic Logic", 1996, vol.2, N2, pp.127-158 (avaliable online at http://citeseer.ist.psu.edu/henkin96discovery.html).

Henkin's proof was further 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).

In the 1920s, some people insisted 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 a meaningful theory - as a "theory of something". Model Existence Theorem says the contrary - (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". For example, 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, if necessary. Euclidean geometry describes its own kind of "mathematical reality".

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

Proof of Theorem 4.3.0.

If T proves F, then F is always true in all models of T (Exercise 4.3.1X).

Now , let us assume that some formula F is always true in all models of theory T, yet it cannot be proved in T. Let us consider the theory T' in the language of T which contains (besides the axioms of T) an additional 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 to F the quantifiers Ax₁...Ax_n). Since F cannot be derived from the axioms of T, 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 [T]: ~Ax₁...Ax_nF |- C, and [T]: ~Ax₁...Ax_nF |- ~C. Since ~Ax₁...Ax_nF is a closed formula, by Deduction Theorem 2, [T]: |- ~Ax₁...Ax_nF ->C, and [T]: |- ~Ax₁...Ax_nF ->~C. Now, by axiom L₉: (B->C)->(B->~C)->~B, we obtain that [T]: |- ~~Ax₁...Ax_nF. By the (classical) Double Negation Law, this implies [T]: |- Ax₁...Ax_nF, and by axiom L₁₂: AxB(x)->B(x) - [T]: |- F. But, by our assumption, F cannot be proved in T. 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, all axioms of T are always true, i.e. J is a model of T. And the formula ~Ax₁...Ax_nF (as an axiom of T') also is true under J. On the other hand, since F is always true in all models of T, it is always true also under the interpretation J. Hence, formulas Ax₁...Ax_nF and ~Ax₁...Ax_nF both are always true under J. This is impossible, hence, F must be provable in T. Q.E.D.

1. Such a simple proof seems almost impossible! We are proving that the logical axioms and rules of inference 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 that we will consider below, is positive, not negative!

2. The above simple proof seems to be extremely non-constructive! "If F is always true in all models of T, then it can be proved in T". How could we obtain this proof? Still, how do we know that F is true in all models of T? Only, if we had a constructive procedure verifying this, we could ask for an algorithm converting such procedures into proofs in T!

Corollary 4.3.4. In any predicate 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 predicate languages do not 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 in

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

improved Church's result:

Church-Kalmar Theorem. If a predicate language contains at least one at least binary predicate constant, then this language do not allow an algorithm determining, is a given formula logically valid or not.

Thus, none of the serious predicate languages allows such an algorithm (languages of PA and ZF included). 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 predicate formulas is semi-decidable.

Church-Kalmar Theorem and Knowledge Bases

TBD.

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 object constants of the language! So, let us add to the language of T an infinite set of new object constants 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 each function constant 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 each predicate constant p as the relation p' such that p'(t₁, ..., t_n) is true in M, if and only if T₂ proves p'(t₁, ..., t_n). To complete the proof, prove that an arbitrary formula G is always true in M, if and only if T₂ proves G. Hence, all theorems of the initial theory T are always true in M.

Adolf Lindenbaum (1904-1941, picture), see also Verfolgte Mathematiker. His wife Janina Hosiasson-Lindenbaum (1899-1941, picture), see also EiGENSiNN philosophiestudentische Zeitung, Juli 2006.

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 predicate 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 object constants of the language! So, in order to prepare enough "bricks", let us add to the language of T a countable set of new object constants 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, object constants 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 object constants do appear in the proof of [T₀]: |- C& ~C? Then, let us replace these constants by any variables of T that do not appear in this proof (this is possible, since each predicate language contains a countable set of object variables). 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 object 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 predicate language contains a countable set of variables). 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 object constants added in Step 1). And let us define interpretations of object constants, function constants and predicate constants as follows.

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

b) The interpretation of a function constant f is the "syntactic constructor function" f', i.e., if f is an n-ary function constant, 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 constant p is the relation p' such, if p is an n-ary predicate constant, and t₁, ..., t_n are constant terms, then p'(t₁, ..., t_n) is defined as true in M, if and only if 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, if and only if 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, if and only if 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 constant, 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, if and only if T₂ |- p(s'₁, ..., s'_n), i.e., if and only if 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, if and only if T₂ |- F, then we can conclude that F is false in M, if and only if 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, if and only if T₂ |- ~F, then we can conclude that F is true in M, if and only if 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, if and only if H(t₁, ..., t_m) is false in M. By the induction assumption, H(t₁, ..., t_m) is true in M, if and only if 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, if and only if T₂ |- ~H(t₁, ..., t_m), i.e., if and only if 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, if and only if H(t₁, ..., t_m) is true in M, and K(t₁, ..., t_m) is false in M. By the induction assumption, H(t₁, ..., t_m) is true in M, if and only if T₂ |- H(t₁, ..., t_m), and K(t₁, ..., t_m) is true in M, if and only if T₂ |- K(t₁, ..., t_m). By the above note, K(t₁, ..., t_m) is false in M, if and only if T₂ |- ~K(t₁, ..., t_m). Hence,

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

or,

G(t₁, ..., t_m) is true in M, if and only if 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, if and only if T₂ |- H(t₁, ..., t_m)->K(t₁, ..., t_m),

or, G(t₁, ..., t_m) is true in M, if and only if 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, if and only if H(t₁, ..., t_m) is true in M, and K(t₁, ..., t_m) is true in M. By the induction assumption, H(t₁, ..., t_m) is true in M, if and only if T₂ |- H(t₁, ..., t_m), and K(t₁, ..., t_m) is true in M, if and only if 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, if and only if T₂ |- H(t₁, ..., t_m)&K(t₁, ..., t_m),

or, G(t₁, ..., t_m) is true in M, if and only if 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, if and only if H(t₁, ..., t_m) is false in M, and K(t₁, ..., t_m) is false in M. By the induction assumption, and by the above note, H(t₁, ..., t_m) is false in M, if and only if T₂ |- ~H(t₁, ..., t_m), and K(t₁, ..., t_m) is false in M, if and only if 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, if and only if T₂ |- ~(H(t₁, ..., t_m)vK(t₁, ..., t_m)),

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

Case 5: G is ExH. Then, by definition, G(t₁, ..., t_m) is true in M, if and only if H(x, t₁, ..., t_m) is "true for some x", i.e., if and only if H(t, t₁, ..., t_m) is true in M for some constant term t in M. By the induction assumption, H(t, t₁, ..., t_m) is true in M, if and only if 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 an object constant.

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 an object constant. Thus, by MP, T₂ |- H(c_H, t₁, ..., t_m). Since c_H is a constant term, by the 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, if and only if H(x, t₁, ..., t_m) is "true for all x", i.e., if and only if H(t, t₁, ..., t_m) is true in M for all constant terms t in M. By the induction assumption, H(t, t₁, ..., t_m) is true in M, if and only if T₂ |- H(t, t₁, ..., t_m).

Let us prove that G(t₁, ..., t_m) is false in M, if and only if 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 the 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 an object constant. Hence, by MP, T₂ |- ~H(c_~H, t₁, ..., t_m), i.e. T₂ does not prove H(c_~H, t₁, ..., t_m). Then, by the 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, if and only if T₂ does not prove Ex~H(x, t₁, ..., t_m). Since T₂ is a complete theory, G(t₁, ..., t_m) is true in M, if and only if 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), if and only if T₂ |- AxH(x, t₁, ..., t_m), i.e. G(t₁, ..., t_m) is true in M, if and only if 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 constants are computable functions (verify!). But the interpretations of predicate constants? We interpreted each predicate constant p as the relation p' such that p'(t₁, ..., t_n) is true, if and only if 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, if and only if there is a computable function g(x,y) such that, for all x, f(x) = lim g(x,y) as y->infinity.)

Logical Consequence

As noted above, some formula G is a "logical consequence" of the formulas A₁, ..., A_n, iff the formula A₁, ..., A_n->G is logically valid, iff, G can be derived from A₁, ..., A_n by using the axioms and rules of inference of the classical logic. This completes the formalization of the somewhat mystical notion of "logical consequence".

Consistency and Satisfiability

A set of formulas F₁, ..., F_n is called inconsistent, if and only if 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 predicate language: a) is consistent in the classical logic, if and only if it is satisfiable, b) is inconsistent in the classical logic, if and only if it is unsatisfiable. (Hint: use the result of Exercise 4.1.1).

Skolem's Paradox

Initially, the Model Existence Theorem was 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 1949): 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.

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.

Loewenheim-Skolem theorem (and the Model Existence theorem) is steadily provoking the so-called Skolem's Paradox, first noted by Skolem in his address before the 5th Congress of Scandinavian Mathematicians (July 4-7, 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.

Skolem called the effect "relativity of set-theoretic notions". 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 put it as follows: any consistent axiomatic set theory has countable models, hence, no axiom system can represent our "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