Copyright \begin{matrix}c \\ ◯ \end{matrix}1998–2013 by Stephen G. Simpson

Mathematical Logic

Stephen G. Simpson

October 17, 2013 Department of Mathematics The Pennsylvania State University University Park, State College PA 16802

       http://www.math.psu.edu/simpson/

This is a set of lecture notes for introductory courses in mathematical logic offered at the Pennsylvania State University.

Contents

Contents 1

1 Propositional Calculus 3 1.1 Formulas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2 Assignments and Satisfiability . . . . . . . . . . . . . . . . . . . . 6 1.3 Logical Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . 10 1.4 The Tableau Method . . . . . . . . . . . . . . . . . . . . . . . . . 12 1.5 The Completeness Theorem . . . . . . . . . . . . . . . . . . . . . 18 1.6 Trees and König’s Lemma . . . . . . . . . . . . . . . . . . . . . . 20 1.7 The Compactness Theorem . . . . . . . . . . . . . . . . . . . . . 21 1.8 Combinatorial Applications . . . . . . . . . . . . . . . . . . . . . 22

2 Predicate Calculus 24 2.1 Formulas and Sentences . . . . . . . . . . . . . . . . . . . . . . . 24 2.2 Structures and Satisfiability . . . . . . . . . . . . . . . . . . . . . 26 2.3 The Tableau Method . . . . . . . . . . . . . . . . . . . . . . . . . 31 2.4 Logical Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . 37 2.5 The Completeness Theorem . . . . . . . . . . . . . . . . . . . . . 40 2.6 The Compactness Theorem . . . . . . . . . . . . . . . . . . . . . 46 2.7 Satisfiability in a Domain . . . . . . . . . . . . . . . . . . . . . . 47

3 Proof Systems for Predicate Calculus 50 3.1 Introduction to Proof Systems . . . . . . . . . . . . . . . . . . . . 50 3.2 The Companion Theorem . . . . . . . . . . . . . . . . . . . . . . 51 3.3 Hilbert-Style Proof Systems . . . . . . . . . . . . . . . . . . . . . 56 3.4 Gentzen-Style Proof Systems . . . . . . . . . . . . . . . . . . . . 61 3.5 The Interpolation Theorem . . . . . . . . . . . . . . . . . . . . . 67

4 Extensions of Predicate Calculus 72 4.1 Predicate Calculus with Identity . . . . . . . . . . . . . . . . . . 72 4.2 The Spectrum Problem . . . . . . . . . . . . . . . . . . . . . . . 76 4.3 Predicate Calculus With Operations . . . . . . . . . . . . . . . . 79 4.4 Predicate Calculus with Identity and Operations . . . . . . . . . 83 4.5 Many-Sorted Predicate Calculus . . . . . . . . . . . . . . . . . . 85 5 Theories, Models, Definability 88

5.1 Theories and Models . . . . . . . . . . . . . . . . . . . . . . . . . 88 5.2 Mathematical Theories . . . . . . . . . . . . . . . . . . . . . . . . 90 5.3 Definability over a Model . . . . . . . . . . . . . . . . . . . . . . 98 5.4 Definitional Extensions of Theories . . . . . . . . . . . . . . . . . 101 5.5 Foundational Theories . . . . . . . . . . . . . . . . . . . . . . . . 104 5.6 Axiomatic Set Theory . . . . . . . . . . . . . . . . . . . . . . . . 107 5.7 Interpretability . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112 5.8 Beth’s Definability Theorem . . . . . . . . . . . . . . . . . . . . . 113

6 Arithmetization of Predicate Calculus 115 6.1 Primitive Recursive Arithmetic . . . . . . . . . . . . . . . . . . . 115 6.2 Interpretability of PRA in Z_{1} . . . . . . . . . . . . . . . . . . . . 115 6.3 Gödel Numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115 6.4 Undefinability of Truth . . . . . . . . . . . . . . . . . . . . . . . . 118 6.5 The Provability Predicate . . . . . . . . . . . . . . . . . . . . . . 119 6.6 The Incompleteness Theorems . . . . . . . . . . . . . . . . . . . . 120 6.7 Proof of Lemma 6.5.3 . . . . . . . . . . . . . . . . . . . . . . . . 122

Bibliography 123

Index 124

Chapter 1

Propositional Calculus

1.1 Formulas

Definition 1.1.1. The propositional connectives are negation (¬), conjunction ( ∧), disjunction ( ∨), implication ( ⇒), biimplication ( ⇔). They are read as “not”, “and”, “or”, “if-then”, “if and only if” respectively. The connectives ∧, ∨, ⇒, ⇔ are designated as binary, while ¬ is designated as unary.

Definition 1.1.2. A propositional language L is a set of propositional atoms p, q, r, . . .. An atomic L-formula is an atom of L.

Definition 1.1.3. The set of L-formulas is generated inductively according to the following rules:

1. If p is an atomic L-formula, then p is an L-formula.

2. If A is an L-formula, then (¬ A) is an L-formula.

3. If A and B are L-formulas, then (A ∧ B), (A ∨ B), (A ⇒ B), and (A ⇔ B) are L-formulas.

Note that rule 3 can be written as follows:

3′. If A and B are L-formulas and b is a binary connective, then (A b B) is an L-formula.

Example 1.1.4. Assume that L contains propositional atoms p, q, r, s. Then

(((p ⇒ q) ∧ (q ∨ r)) ⇒ (p ∨ r)) ⇒ ¬ (q ∨ s)

is an L-formula.

Definition 1.1.5. If A is a formula, the degree of A is the number of occurrences of propositional connectives in A. This is the same as the number of times rules 2 and 3 had to be applied in order to generate A.

Example 1.1.6. The degree of the formula of Example 1.1.4 is 8.

Remark 1.1.7 (omitting parentheses). As in the above example, we omit parentheses when this can be done without ambiguity. In particular, outermost parentheses can always be omitted, so instead of ((¬ A) ⇒ B) we may write (¬ A) ⇒ B. But we may not write ¬ A ⇒ B, because this would not distinguish the intended formula from ¬ (A ⇒ B).

Definition 1.1.8. Let L be a propositional language. A formation sequence is finite sequence A_{1}, A_{2}, …, A_{n} such that each term of the sequence is obtained from previous terms by application of one of the rules in Definition 1.1.3. A formation sequence for A is a formation sequence whose last term is A. Note that A is an L-formula if and only if there exists a formation sequence for A.

Example 1.1.9. A formation sequence for the L-formula of Example 1.1.4 is

\begin{matrix}p, q, p ⇒ q, r, q ∨ r, (p ⇒ q) ∧ (q ∨ r), p ∨ r, ((p ⇒ q) ∧ (q ∨ r)) ⇒ (p ∨ r), \\ s, q ∨ s, ¬ (q ∨ s), (((p ⇒ q) ∧ (q ∨ r)) ⇒ (p ∨ r)) ⇒ ¬ (q ∨ s) . \end{matrix}

Remark 1.1.10. In contexts where the language L does not need to be specified, an L-formula may be called a formula.

Definition 1.1.11. A formation tree is a finite rooted dyadic tree where each node carries a formula and each non-atomic formula branches to its immediate subformulas (see the example below). If A is a formula, the formation tree for A is the unique formation tree which carries A at its root.

Example 1.1.12. The formation tree for the formula of Example 1.1.4 is

(((p ⇒ q) ∧ (q ∨ r)) ⇒ (p ∨ r)) ⇒ ¬ (q ∨ s)
/ \

\begin{matrix}((p ⇒ q) ∧ (q ∨ r)) ⇒ (p ∨ r) \\ /  \ \\ \begin{matrix}(p ⇒ q) ∧ (q ∨ r) \\ /  \ \\ p ⇒ q  q ∨ r \\ / \  / \ \\ p  q q  r \end{matrix} & \begin{matrix}p ∨ r \\ / \ \\ p  r \end{matrix} \end{matrix}  \begin{matrix}¬ (q ∨ s) \\ | \\ q ∨ s \\ / \ \\ q  s \end{matrix}

or, in an abbreviated style,

⇒

/  \

\begin{matrix}⇒ \\ / \ \\ ∧ & ∨ \\ / \ / \ \\ ⇒ ∨ p r \\ / \ / \ \\ p q q r \end{matrix} \begin{matrix}¬ \\ | \\ ∨ \\ / \ \\ q s \end{matrix}

Remark 1.1.13. Note that, if we identify formulas with formation trees in the abbreviated style, then there is no need for parentheses.

Remark 1.1.14. Another way to avoid parentheses is to use Polish notation. In this case the set of L-formulas is generated as follows:

1. If p is an atomic L-formula, then p is an L-formula.

2. If A is an L-formula, then ¬ A is an L-formula.

3. If A and B are L-formulas and b is a binary connective, then b A B is an L-formula.

For example, (¬ p) ⇒ q becomes ⇒ ¬ p q, and ¬ (p ⇒ q) becomes ¬ ⇒ p q. The formula of Example 1.1.4 becomes

⇒ ⇒ ∧ ⇒ p q ∨ q r ∨ p r ¬ ∨ q s

and a formation sequence for this is

\begin{matrix}p, q, ⇒ p q, r, ∨ q r, ∧ ⇒ p q ∨ q r, ∨ p r, ⇒ ∧ ⇒ p q ∨ q r ∨ p r, \\ s, ∨ q s, ¬ ∨ q s, ⇒ ⇒ ∧ ⇒ p q ∨ q r ∨ p r ¬ ∨ q s . \end{matrix}

Obviously Polish notation is difficult to read, but it has the advantages of being linear and of not using parentheses.

Remark 1.1.15. In our study of formulas, we shall be indifferent to the question of which system of notation is actually used. The only point of interest for us is that each non-atomic formula is uniquely of the form ¬ A or A b B, where A and B are formulas and b is a binary connective.

Exercises 1.1.16. Let C be the formula (p ∧ ¬ q) ⇒ ¬ (p ∨ r).

1. Restore all the omitted parentheses to C. (See Remark 1.1.7.)

2. Exhibit a formation sequence for C.

3. List the immediate subformulas of C, their immediate subformulas, etc., i.e., all subformulas of C.

4. Calculate the degrees of C and its subformulas.

5. Display the formation tree of C.

6. Write C according to various notation systems:

(a) The rules 1–3 of Definition 1.1.3:

1. Each atom is a formula.

2. If A is a formula then (¬ A) is a formula.

3. If A and B are formulas and b is a binary connective, then (AbB) is a formula.

(b) The following alternative set of rules: 1. Each atom is a formula.

2. If A is a formula then ¬ (A) is a formula.

3. If A and B are formulas and b is a binary connective, then

(A)b(B) is a formula.

(c) Polish notation.

(d) Reverse Polish notation.

1.2 Assignments and Satisfiability

Definition 1.2.1. There are two truth values, T and F, denoting truth and falsity.

Definition 1.2.2. Let L be a propositional language. An L-assignment is a mapping

M : {p | p is an atomic L-formula} → {T, F} .

Note that if L has exactly n atoms then there are exactly 2^{n} different Lassignments.

Lemma 1.2.3. Given an L-assignment M, there is a unique L-valuation

v_{M} : {A | A is an L-formula} → {T, F}

given by the following clauses:

1. v_{M}(¬ A) = \{ \begin{matrix}T & if v_{M}(A) = F , \\ F & if v_{M}(A) = T . \end{matrix}

2. v_{M}(A ∧ B) = \{ \begin{matrix}T & if v_{M}(A) = v_{M}(B) = T , \\ F & if at least one of v_{M}(A), v_{M}(B) = F . \end{matrix}

3. v_{M}(A ∨ B) = \{ \begin{matrix}T & if at least one of v_{M}(A), v_{M}(B) = T , \\ F & if v_{M}(A) = v_{M}(B) = F . \end{matrix}

4. v_{M}(A ⇒ B) = v_{M}(¬ (A ∧ ¬ B)) .

5. v_{M}(A ⇔ B) = \{ \begin{matrix}T & if v_{M}(A) = v_{M}(B) , \\ F & if v_{M}(A) ≠ v_{M}(B) . \end{matrix}

Proof. The truth value v_{M}(A) is defined by recursion on L-formulas, i.e., by induction on the degree of A where A is an arbitrary L-formula. □

Remark 1.2.4. Note that each clause of Lemma 1.2.3 corresponds to the familiar truth table for the corresponding propositional connective. Thus clause 3 corresponds to the truth table

A B A ∨ B
T T  T
T F  T
F T  T
F F  F

for ∨, and clause 4 corresponds to the truth table

A B A ⇒ B
T T  T
T F  F
F T  T
F F  T

for ⇒.

Remark 1.2.5. Lemma 1.2.3 may be visualized in terms of formation trees. To define v_{M}(A) for a formula A, one begins with an assignment of truth values to the atoms, i.e., the end nodes of the formation tree for A, and then proceeds upward to the root, assigning truth values to the nodes, each step being given by the appropriate clause.

Example 1.2.6. Consider the formula (p ⇒ q) ⇒ (q ⇒ r) under an assignment M with M(p) = T, M(q) = F, M(r) = T. In terms of the formation tree, this looks like

(p ⇒ q) ⇒ (q ⇒ r)

/ \

p ⇒ q q ⇒ r / \ / \ p q q r T F F T

and by applying clause 4 three times we get

(p ⇒ q) ⇒ (q ⇒ r)

T

/ \

p ⇒ q q ⇒ r F T / \ / \ p q q r T F F T

and from this we see that v_{M}((p ⇒ q) ⇒ (q ⇒ r)) = T.

Remark 1.2.7. The above formation tree with truth values can be compressed and written linearly as

\begin{matrix}(p ⇒ q) ⇒ (q ⇒ r) \\ T F F T F T T . \end{matrix}

This illustrates a convenient method for calculating v_{M}(A), where M is an arbitrary L-assignment. Remark 1.2.8. Lemma 1.2.3 implies that there is an obvious one-to-one correspondence between L-assignments and L-valuations. If the language L is understood from context, we may speak simply of assignments and valuations.

We now present some key definitions. Fix a propositional language L. Definition 1.2.9. Let M be an assignment. A formula A is said to be true under M if v_{M}(A) = T, and false under M if v_{M}(A) = F. Definition 1.2.10. A set of formulas S is said to be satisfiable if there exists an assignment M which satisfies S, i.e., v_{M}(A) = T for all A ∈ S. Definition 1.2.11. Let S be a set of formulas. A formula B is said to be a logical consequence of S if it is true under all assignments which satisfy S. Definition 1.2.12. A formula B is said to be logically valid (or a tautology) if B is true under all assignments. Equivalently, B is a logical consequence of the empty set. Remark 1.2.13. B is a logical consequence of A_{1}, …, A_{n} if and only if

(A_{1} ∧ ⋯ ∧ A_{n}) ⇒ B

is logically valid. B is logically valid if and only if ¬ B is not satisfiable. Exercises 1.2.14.

1. Use truth tables to show that ((A ⇒ B) ⇒ A) ⇒ A is logically valid.

2. Use truth tables to show that (A ∧ B) ⇒ C is logically equivalent to

A ⇒ (B ⇒ C). Exercises 1.2.15. Prove the following. (See Remarks 1.2.13 and 1.3.2.)

1. B is logically valid if and only if ¬ B is not satisfiable.

2. B is satisfiable if and only if ¬ B is not logically valid.

3. B is a logical consequence of A_{1}, …, A_{n} if and only if (A_{1} ∧ ⋯ ∧ A_{n}) ⇒ B is logically valid.

4. A is logically equivalent to B if and only if A ⇔ B is logically valid. Exercise 1.2.16. Brown, Jones, and Smith are suspected of a crime. They testify as follows:

Brown: Jones is guilty and Smith is innocent. Jones: If Brown is guilty then so is Smith.

Smith: I’m innocent, but at least one of the others is guilty.

Let b, j, and s be the statements “Brown is innocent,” “Jones is innocent,” “Smith is innocent”.

1. Express the testimony of each suspect as a propositional formula. Write a truth table for the three testimonies.

2. Use the above truth table to answer the following questions:

(a) Are the three testimonies consistent?

(b) The testimony of one of the suspects follows from that of another. Which from which?

(c) Assuming everybody is innocent, who committed perjury?

(d) Assuming all testimony is true, who is innocent and who is guilty?

(e) Assuming that the innocent told the truth and the guilty told lies, who is innocent and who is guilty?

Solution.

1. The testimonies are:

\begin{matrix}B : & (¬ j) ∧ s \\ J : & (¬ b) ⇒ (¬ s) \\ S : & s ∧ ((¬ b) ∨ (¬ j)) \end{matrix}

The truth table is:

b j s  B J S
1 T T T F T F
2 T T F F T F
3 T F T T T T
4 T F F F T F
5 F T T F F T
6 F T F F T F
7 F F T T F T
8 F F F F T F

2. (a) Yes, by line 3 of the table.

(b) The table shows that S is a logical consequence of B. In other words, Smith’s testimony follows from Brown’s.

(c) If everybody is innocent, we are in line 1 of the table. Hence B and S are false, i.e., Brown and Smith lied.

(d) If all the testimony is true, we are in line 3 of the table. Thus Brown and Smith are innocent, while Jones is guilty.

(e) Our assumption is v_{M}(b) = v_{M}(B), v_{M}(j) = v_{M}(J), v_{M}(s) = v_{M}(S). Hence we are in line 6 of the table. Thus Jones is innocent, and Brown and Smith are guilty.

1.3 Logical Equivalence

Definition 1.3.1. Two formulas A and B are said to be logically equivalent, written A ≡ B, if each is a logical consequence of the other. Remark 1.3.2. A ≡ B holds if and only if A ⇔ B is logically valid. Exercise 1.3.3. Assume A_{1} ≡ A_{2}. Show that

1. ¬ A_{1} ≡ ¬ A_{2};

2. A_{1} ∧ B ≡ A_{2} ∧ B;

3. B ∧ A_{1} ≡ B ∧ A_{2};

4. A_{1} ∨ B ≡ A_{2} ∨ B;

5. B ∨ A_{1} ≡ B ∨ A_{2};

6. A_{1} ⇒ B ≡ A_{2} ⇒ B;

7. B ⇒ A_{1} ≡ B ⇒ A_{2};

8. A_{1} ⇔ B ≡ A_{2} ⇔ B;

9. B ⇔ A_{1} ≡ B ⇔ A_{2}. Exercise 1.3.4. Assume A_{1} ≡ A_{2}. Show that for any formula C containing A_{1} as a part, if we replace one or more occurrences of the part A_{1} by A_{2}, then the resulting formula is logically equivalent to C. (Hint: Use the results of the previous exercise, plus induction on the degree of C.) Remark 1.3.5. Some useful logical equivalences are:

1. commutative laws: (a) A ∧ B ≡ B ∧ A

(b) A ∨ B ≡ B ∨ A

(c) A ⇔ B ≡ B ⇔ A

Note however that A ⇒ B ≢ B ⇒ A.

2. associative laws: (a) A ∧ (B ∧ C) ≡ (A ∧ B) ∧ C

(b) A ∨ (B ∨ C) ≡ (A ∨ B) ∨ C

(c) A ⇔ (B ⇔ C) ≡ (A ⇔ B) ⇔ C Note however that A ⇒ (B ⇒ C) ≢ (A ⇒ B) ⇒ C.

3. distributive laws:

(a) A ∧ (B ∨ C) ≡ (A ∧ B) ∨ (A ∧ C)

(b) A ∨ (B ∧ C) ≡ (A ∨ B) ∧ (A ∨ C)

(c) A ⇒ (B ∧ C) ≡ (A ⇒ B) ∧ (A ⇒ C)

(d) A ⇒ (B ∨ C) ≡ (A ⇒ B) ∨ (A ⇒ C)

(e) (A ∧ B) ⇒ C ≡ (A ⇒ C) ∨ (B ⇒ C)

(f) (A ∨ B) ⇒ C ≡ (A ⇒ C) ∧ (B ⇒ C)

Note however that (A ∧ B) ⇒ C ≢ (A ⇒ C) ∧ (B ⇒ C), and (A ∨ B) ⇒ C ≢ (A ⇒ C) ∨ (B ⇒ C).

4. negation laws:

(a) ¬ (A ∧ B) ≡ (¬ A) ∨ (¬ B)

(b) ¬ (A ∨ B) ≡ (¬ A) ∧ (¬ B)

(c) ¬ ¬ A ≡ A

(d) ¬ (A ⇒ B) ≡ A ∧ ¬ B

(e) ¬ (A ⇔ B) ≡ (¬ A) ⇔ B

(f) ¬ (A ⇔ B) ≡ A ⇔ (¬ B)

5. implication laws:

(a) A ⇒ B ≡ ¬ (A ∧ ¬ B)

(b) A ⇒ B ≡ (¬ A) ∨ B

(c) A ⇒ B ≡ (¬ B) ⇒ (¬ A)

(d) A ⇔ B ≡ (A ⇒ B) ∧ (B ⇒ A)

(e) A ⇔ B ≡ (¬ A) ⇔ (¬ B)

Definition 1.3.6. A formula is said to be in disjunctive normal form if it is of the form A_{1} ∨ ⋯ ∨ A_{m}, where each clause A_{i}, i = 1, …, m, is of the form B_{1} ∧ ⋯ ∧ B_{n}, and each B_{j}, j = 1, …, n is either an atom or the negation of an atom.

Example 1.3.7. Writing \overline{p} as an abbreviation for ¬ p, the formula

(p_{1} ∧ \overline{p_{2}} ∧ p_{3}) ∨ (\overline{p_{1}} ∧ p_{2} ∧ p_{3}) ∨ (p_{1} ∧ \overline{p_{2}} ∧ \overline{p_{3}})

is in disjunctive normal form.

Exercise 1.3.8. Show that every propositional formula C is logically equivalent to a formula in disjunctive normal form.

Remark 1.3.9. There are two ways to do Exercise 1.3.8.

1. One way is to apply the equivalences of Remark 1.3.5 to subformulas of C via Exercise 1.3.4, much as one applies the commutative and distributive laws in algebra to reduce every algebraic expression to a polynomial.

2. The other way is to use a truth table for C. The disjunctive normal form of C has a clause for each assignment making C true. The clause specifies the assignment.

Example 1.3.10. Consider the formula (p ⇒ q) ⇒ r. We wish to put this in disjunctive normal form.

Method 1. Applying the equivalences of Remark 1.3.5, we obtain

(p ⇒ q) ⇒ r ≡ r ∨ ¬ (p ⇒ q)
≡ r ∨ ¬ ¬ (p ∧ ¬ q)
≡ r ∨ (p ∧ ¬ q)

and this is in disjunctive normal form.

Method 2. Consider the truth table

p q r p ⇒ q (p ⇒ q) ⇒ r
1  T T T T  T
2  T T F T  F
3  T F T F  T
4  T F F F  T
5  F T T T  T
6  F T F T  F
7  F F T T  T
8  F F F T  F

Each line of this table corresponds to a different assignment. From lines 1, 3, 4, 5, 7 we read off the following formula equivalent to (p ⇒ q) ⇒ r in disjunctive normal form:

(p ∧ q ∧ r) ∨ (p ∧ \overline{q} ∧ r) ∨ (p ∧ \overline{q} ∧ \overline{r}) ∨ (\overline{p} ∧ q ∧ r) ∨ (\overline{p} ∧ \overline{q} ∧ r) .

1.4 The Tableau Method

Remark 1.4.1. A more descriptive name for tableaux is satisfiability trees. We follow the approach of Smullyan [4].

Definition 1.4.2. A signed formula is an expression of the form TA or FA, where A is a formula. An unsigned formula is simply a formula.

Definition 1.4.3. A signed tableau is a rooted dyadic tree where each node carries a signed formula. An unsigned tableau is a rooted dyadic tree where each node carries an unsigned formula. The signed tableau rules are presented in Table 1.1. The unsigned tableau rules are presented in Table 1.2. If τ is a (signed or unsigned) tableau, an immediate extension of τ is a larger tableau τ′ obtained by applying a tableau rule to a finite path of τ.

⋮ ; T A ∧ B ; ⋮ ; | ; T A ; T B  ⋮ ; F A ∧ B ; ⋮ ; / \ ; F A F B

⋮ ; T A ∨ B ; ⋮ ; / \ ; T A T B  ⋮ ; F A ∨ B ; ⋮ ; | ; F A ; F B

⋮ ; T A ⇒ B ; ⋮ ; / \ ; F A T B  ⋮ ; F A ⇒ B ; ⋮ ; | ; T A ; F B

⋮ ; T A ⇔ B ; ⋮ ; / \ ; T A F A ; T B F B  ⋮ ; F A ⇔ B ; ⋮ ; / \ ; T A F A ; F B T B

⋮ ; T ¬ A ; ⋮ ; | ; F A  ⋮ ; F ¬ A ; ⋮ ; | ; T A

Table 1.1: Signed tableau rules for propositional connectives.

⋮ ; A ∧ B ; ⋮ ; | ; A ; B  ⋮ ; ¬ (A ∧ B) ; ⋮ ; / \ ; ¬ A ¬ B

⋮ ; A ∨ B ; ⋮ ; / \ ; A B  ⋮ ; ¬ (A ∨ B) ; ⋮ ; | ; ¬ A ; ¬ B

⋮ ; A ⇒ B ; ⋮ ; / \ ; ¬ A B  ⋮ ; ¬ (A ⇒ B) ; ⋮ ; | ; A ; ¬ B

⋮ ; A ⇔ B ; ⋮ ; / \ ; A ¬ A ; B ¬ B  ⋮ ; ¬ (A ⇔ B) ; ⋮ ; / \ ; A ¬ A ; ¬ B B

⋮ ¬ ¬ A

⋮ | A

Table 1.2: Unsigned tableau rules for propositional connectives.

Definition 1.4.4. Let X_{1}, …, X_{k} be a finite set of signed or unsigned formulas. A tableau starting with X_{1}, …, X_{k} is a tableau obtained from

X_{1} ; ⋮ ; X_{k}

by repeatedly applying tableau rules.

Definition 1.4.5. A path of a tableau is said to be closed if it contains a conjugate pair of signed or unsigned formulas, i.e., a pair such as TA, FA in the signed case, or A, ¬ A in the unsigned case. A path of a tableau is said to be open if it is not closed. A tableau is said to be closed if each of its paths is closed.

The tableau method:

1. To test a formula A for validity, form a signed tableau starting with FA, or equivalently an unsigned tableau starting with ¬ A. If the tableau closes off, then A is logically valid.

2. To test whether B is a logical consequence of A_{1}, …, A_{k}, form a signed tableau starting with TA_{1}, …, TA_{k}, FB, or equivalently an unsigned tableau starting with A_{1}, …, A_{k}, ¬ B. If the tableau closes off, then B is indeed a logical consequence of A_{1}, …, A_{k}.

3. To test A_{1}, …, A_{k} for satisfiability, form a signed tableau starting with TA_{1}, …, TA_{k}, or equivalently an unsigned tableau starting with A_{1}, …, A_{k}. If the tableau closes off, then A_{1}, …, A_{k} is not satisfiable. If the tableau does not close off, then A_{1}, …, A_{k} is satisfiable, and from any open path we can read off an assignment satisfying A_{1}, …, A_{k}.

The correctness of these tests will be proved in Section 1.5. See Corollaries 1.5.9, 1.5.10, 1.5.11 below.

Example 1.4.6. Using the signed tableau method to test (p ∧ q) ⇒ (q ∧ p) for logical validity, we have

F (p ∧ q) ⇒ (q ∧ p)
T p ∧ q
F q ∧ p
T p
T q
/ \
F q F p

Since (every path of) the tableau is closed, (p ∧ q) ⇒ (q ∧ p) is logically valid.

Exercises 1.4.7.

1. Use a signed tableau to show that (A ⇒ B) ⇒ (A ⇒ C) is a logical consequence of A ⇒ (B ⇒ C). Solution.

T A ⇒ (B ⇒ C)
F (A ⇒ B) ⇒ (A ⇒ C)
T A ⇒ B
F A ⇒ C
T A
F C
/ \
F A T B ⇒ C
/ \
F B T C
/ \
F A T B

2. Use a signed tableau to show that A ⇒ B is logically equivalent to (¬ B) ⇒ (¬ A). Solution.

F (A ⇒ B) ⇔ ((¬ B) ⇒ (¬ A))
/
T A ⇒ B
F (¬ B) ⇒ (¬ A)
T ¬ B
F ¬ A
F B
T A
/ \
F A T B

\
F A ⇒ B
T (¬ B) ⇒ (¬ A)
T A
F B
/ \
F ¬ B T ¬ A
T B F A

3. Use an unsigned tableau to show that A ⇒ (B ⇒ C) is logically equivalent to (A ∧ B) ⇒ C. Solution.

¬ ((A ⇒ (B ⇒ C)) ⇔ ((A ∧ B) ⇒ C))

/ \

\begin{matrix}A ⇒ (B ⇒ C) \\ ¬ ((A ∧ B) ⇒ C) \\ A ∧ B \\ ¬ C \\ A \\ B \\ / \ \\ ¬ A B ⇒ C \\ / \ \\ ¬ B  C \end{matrix}  \begin{matrix}¬ (A ⇒ (B ⇒ C)) \\ (A ∧ B) ⇒ C \\ A \\ ¬ (B ⇒ C) \\ B \\ ¬ C \\ / \ \\ ¬ (A ∧ B) C \\ / \ \\ ¬ A ¬ B \end{matrix}

4. Use an unsigned tableau to test (p ∨ q) ⇒ (p ∧ q) for logical validity. If this formula is not logically valid, use the tableau to find all assignments which falsify it.

Solution.

¬ ((p ∨ q) ⇒ (p ∧ q))
p ∨ q
¬ (p ∧ q)
/ \
p q
/ \ / \
¬ p ¬ q ¬ p ¬ q
1  2  3  4

The open paths 2 and 3 provide the assignments M_{2} and M_{3} which falsify our formula. M_{2}(p) = T, M_{2}(q) = F, M_{3}(p) = F, M_{3}(q) = T.

5. Redo the previous problem using a signed tableau.

Solution.

F (p ∨ q) ⇒ (p ∧ q)
T p ∨ q
F p ∧ q
/ \
T p T q
/ \ / \
F p F q F p F q
1  2  3  4

The open paths 2 and 3 provide the assignments M_{2} and M_{3} which falsify our formula. M_{2}(p) = T, M_{2}(q) = F, M_{3}(p) = F, M_{3}(q) = T.

Exercise 1.4.8.

1. Formulate the following argument as a propositional formula.

If it has snowed, it will be poor driving. If it is poor driving, I will be late unless I start early. Indeed, it has snowed. Therefore, I must start early to avoid being late.

Solution. Use the following atoms.

s: it has snowed p: it is poor driving l: I will be late e: I start early The argument can be translated as follows: s ⇒ p, p ⇒ (l ∨ e), s, therefore (¬ l) ⇒ e. Written as a single propositional formula, this becomes:

((s ⇒ p) ∧ (p ⇒ (l ∨ e)) ∧ s) ⇒ ((¬ l) ⇒ e).

2. Use the tableau method to demonstrate that this formula is logically valid.

Solution.

F ((s ⇒ p) ∧ (p ⇒ (l ∨ e)) ∧ s) ⇒ ((¬ l) ⇒ e)
T (s ⇒ p) ∧ (p ⇒ (l ∨ e)) ∧ s
F (¬ l) ⇒ e
T s ⇒ p
T (p ⇒ (l ∨ e)) ∧ s
T p ⇒ (l ∨ e)
T s
T ¬ l
F e
F l
/ \
F s T p
/ \
F p T l ∨ e
/ \
T l T e

1.5 The Completeness Theorem

Let X_{1}, …, X_{k} be a finite set of signed formulas, or a finite set of unsigned formulas.

Lemma 1.5.1 (the Soundness Theorem). If τ is a finite closed tableau starting with X_{1}, …, X_{k}, then X_{1}, …, X_{k} is not satisfiable.

Proof. Straightforward. □

Definition 1.5.2. A path of a tableau is said to be replete if, whenever it contains the top formula of a tableau rule, it also contains at least one of the branches. A replete tableau is a tableau in which every path is replete.

Lemma 1.5.3. Any finite tableau can be extended to a finite replete tableau.

Proof. Apply tableau rules until they cannot be applied any more. □

Definition 1.5.4. A tableau is said to be open if it is not closed, i.e., it has at least one open path.

Lemma 1.5.5. Let τ be a replete tableau starting with X_{1}, …, X_{k}. If τ is open, then X_{1}, …, X_{k} is satisfiable.

In order to prove Lemma 1.5.5, we introduce the following definition.

Definition 1.5.6. Let S be a set of signed or unsigned formulas. We say that S is a Hintikka set if

1. S “obeys the tableau rules”, in the sense that if it contains the top formula of a rule then it contains at least one of the branches;

2. S contains no pair of conjugate atomic formulas, i.e., Tp, Fp in the signed case, or p, ¬ p in the unsigned case.

Lemma 1.5.7 (Hintikka’s Lemma). If S is a Hintikka set, then S is satisfiable.

Proof. Define an assignment M by

M(p) = \{ \begin{matrix}T & if Tp belongs to S \\ F & otherwise \end{matrix}

in the signed case, or

M(p) = \{ \begin{matrix}T & if p belongs to S \\ F & otherwise \end{matrix}

in the unsigned case. It is not difficult to see that v_{M}(X) = T for all X ∈ S. □

To prove Lemma 1.5.5, it suffices to note that a replete open path is a Hintikka set. Thus, if a replete tableau starting with X_{1}, …, X_{k} is open, Hintikka’s Lemma implies that X_{1}, …, X_{k} is satisfiable.

Combining Lemmas 1.5.1 and 1.5.3 and 1.5.5, we obtain:

Theorem 1.5.8 (the Completeness Theorem). X_{1}, …, X_{k} is satisfiable if and only if there is no finite closed tableau starting with X_{1}, …, X_{k}.

Corollary 1.5.9. A_{1}, …, A_{k} is not satisfiable if and only if there exists a finite closed signed tableau starting with TA_{1}, …, TA_{k}, or equivalently a finite closed unsigned tableau starting with A_{1}, …, A_{k}.

Corollary 1.5.10. A is logically valid if and only if there exists a finite closed signed tableau starting with FA, or equivalently a finite closed unsigned tableau starting with ¬ A.

Corollary 1.5.11. B is a logical consequence of A_{1}, …, A_{k} if and only if there exists a finite closed signed tableau starting with TA_{1}, …, TA_{k}, FB, or equivalently a finite closed unsigned tableau starting with A_{1}, …, A_{k}, ¬ B.

Exercise 1.5.12. Consider the following argument.

The attack will succeed only if the enemy is taken by surprise or the position is weakly defended. The enemy will not be taken by surprise unless he is overconfident. The enemy will not be overconfident if the position is weakly defended. Therefore, the attack will not succeed.

1. Translate the argument into propositional calculus.

2. Use an unsigned tableau to determine whether the argument is logically valid.

1.6 Trees and König’s Lemma

Up to this point, our discussion of trees has been informal. We now pause to make our tree terminology precise.

Definition 1.6.1. A tree consists of

1. a set T

2. a function ℓ : T → ℕ^{+},

3. a binary relation P on T.

The elements of T are called the nodes of the tree. For x ∈ T, ℓ(x) is the level of x. The relation xP y is read as x immediately precedes y, or y immediately succeeds x. We require that there is exactly one node x ∈ T such that ℓ(x) = 1, called the root of the tree. We require that each node other than the root has exactly one immediate predecessor. We require that ℓ(y) = ℓ(x) + 1 for all x, y ∈ T such that xP y.

Definition 1.6.2. A subtree of T is a nonempty set T′ ⊆ T such that for all y ∈ T′ and xP y, x ∈ T′. Note that T′ is itself a tree, under the restriction of ℓ and P to T′. Moreover, the root of T′ is the same as the root of T.

Definition 1.6.3. An end node of T is a node with no (immediate) successors. A path in T is a set S ⊆ T such that (1) the root of T belongs to S, (2) for each x ∈ S, either x is an end node of T or there is exactly one y ∈ S such that xP y.

Definition 1.6.4. Let P^{∗} be the transitive closure of P, i.e., the smallest reflexive and transitive relation on T containing P. For x, y ∈ T, we have xP^{∗}y if and only if x precedes y, i.e., y succeeds x, i.e., there exists a finite sequence x = x_{0}P x_{1}P x_{2} ⋯ x_{n−1}P x_{n} = y. Note that the relation P^{∗} is reflexive (xP^{∗}x for all x ∈ T), antisymmetric (xP^{∗}y and yP^{∗}x imply x = y), and transitive (xP^{∗}y and yP^{∗}z imply xP^{∗}z). Thus P^{∗} is a partial ordering of T.

Definition 1.6.5. T is finitely branching if each node of T has only finitely many immediate successors in T. T is dyadic if each node of T has at most two immediate successors in T. Note that a dyadic tree is finitely branching.

Theorem 1.6.6 (König’s Lemma). Let T be an infinite, finitely branching tree. Then T has an infinite path.

Proof. Let T̂ be the set of all x ∈ T such that x has infinitely many successors in T. Note that T̂ is a subtree of T. Since T is finitely branching, it follows by the pigeonhole principle that each x ∈ T̂ has at least one immediate successor y ∈ T̂. Now define an infinite path S = {x_{1}, x_{2}, …, x_{n}, …} in T̂ inductively by putting x_{1} = the root of T, and x_{n+1} = one of the immediate successors of x_{n} in T̂. Clearly S is an infinite path of T. □

1.7 The Compactness Theorem

Theorem 1.7.1 (the Compactness Theorem, countable case). Let S be a countable set of propositional formulas. If each finite subset of S is satisfiable, then S is satisfiable.

Proof. In brief outline: Form an infinite tableau. Apply König’s Lemma to get an infinite path. Apply Hintikka’s Lemma.

Details: Let S = {A_{1}, A_{2}, …, A_{i}, …}. Start with A_{1} and generate a finite replete tableau, τ_{1}. Since A_{1} is satisfiable, τ_{1} has at least one open path. Append A_{2} to each of the open paths of τ_{1}, and generate a finite replete tableau, τ_{2}. Since {A_{1}, A_{2}} is satisfiable, τ_{2} has at least one open path. Append A_{3} to each of the open paths of τ_{2}, and generate a finite replete tableau, τ_{3}. . . . . Put τ = ⋃_{i=1}^{∞} τ_{i}. Thus τ is a replete tableau. Note also that τ is an infinite, finitely branching tree. By König’s Lemma (Theorem 1.6.6), let S′ be an infinite path in τ. Then S′ is a Hintikka set containing S. By Hintikka’s Lemma, S′ is satisfiable. Hence S is satisfiable. □

Theorem 1.7.2 (the Compactness Theorem, uncountable case). Let S be an uncountable set of propositional formulas. If each finite subset of S is satisfiable, then S is satisfiable.

Proof. We present three proofs. The first uses Zorn’s Lemma. The second uses transfinite induction. The third uses Tychonoff’s Theorem.

Let L be the (necessarily uncountable) propositional language consisting of all atoms occurring in formulas of S. If S is a set of L-formulas, we say that S is finitely satisfiable if each finite subset of S is satisfiable. We are trying to prove that, if S is finitely satisfiable, then S is satisfiable.

First proof. Consider the partial ordering 𝔉 of all finitely satisfiable sets of L-formulas which include S, ordered by inclusion. It is easy to see that any chain in 𝔉 has a least upper bound in 𝔉. Hence, by Zorn’s Lemma, 𝔉 has a maximal element, S^{∗}. Thus S^{∗} is a set of L-formulas, S^{∗} ⊇ S, S^{∗} is finitely satisfiable, and for each L-formula A ∉ S^{∗}, S^{∗} ∪ {A} is not finitely satisfiable. From this it is straightforward to verify that S^{∗} is a Hintikka set. Hence, by Hintikka’s Lemma, S^{∗} is satisfiable. Hence S is satisfiable.

Second proof. Let A_{ξ}, ξ < α, be a transfinite enumeration of all L-formulas. By transfinite recursion, put S_{0} = S, S_{ξ+1} = S_{ξ} ∪ {A_{ξ}} if S_{ξ} ∪ {A_{ξ}} is finitely satisfiable, S_{ξ+1} = S_{ξ} otherwise, and S_{η} = ⋃_{ξ<η} S_{ξ} for limit ordinals η ≤ α. Using transfinite induction, it is easy to verify that S_{ξ} is finitely satisfiable for each ξ ≤ α. In particular, S_{α} is finitely satisfiable. It is straightforward to verify that S_{α} is a Hintikka set. Hence, by Hintikka’s Lemma, S_{α} is satisfiable. Hence S is satisfiable.

Third proof. Let 𝔐 = {T, F}^{L} be the space of all L-assignments M : L → {T, F}. Make 𝔐 a topological space with the product topology where {T, F} has the discrete topology. Since {T, F} is compact, it follows by Tychonoff’s Theorem that 𝔐 is compact. For each L-formula A, put 𝔐_{A} = {M ∈ 𝔐 | v_{M}(A) = T}. It is easy to check that each 𝔐_{A} is a topologically closed set in 𝔐. If S is finitely satisfiable, then the family of sets 𝔐_{A}, A ∈ S has the finite intersection property, i.e., ⋂_{A∈S_{0}} 𝔐_{A} ≠ ∅ for each finite S_{0} ⊆ S. By compactness of 𝔐 it follows that ⋂_{A∈S} 𝔐_{A} ≠ ∅. Thus S is satisfiable. □

1.8 Combinatorial Applications

In this section we present some combinatorial applications of the Compactness Theorem for propositional calculus.

Definition 1.8.1.

1. A graph consists of a set of vertices together with a specification of certain pairs of vertices as being adjacent. We require that a vertex may not be adjacent to itself, and that u is adjacent to v if and only if v is adjacent to u.

2. Let G be a graph and let k be a positive integer. A k-coloring of G is a function f : {vertices of G} → {c_{1}, …, c_{k}} such that f(u) ≠ f(v) for all adjacent pairs of vertices u, v.

3. G is said to be k-colorable if there exists a k-coloring of G. This notion is much studied in graph theory.

Exercise 1.8.2. Let G be a graph and let k be a positive integer. For each vertex v and each i = 1, …, k, let p_{vi} be a propositional atom expressing that vertex v receives color c_{i}. Define C_{k}(G) to be the following set of propositional formulas: p_{v1} ∨ ⋯ ∨ p_{vk} for each vertex v; ¬ (p_{vi} ∧ p_{vj}) for each vertex v and 1 ≤ i < j ≤ k; ¬ (p_{ui} ∧ p_{vi}) for each adjacent pair of vertices u, v and 1 ≤ i ≤ k.

1. Show that there is a one-to-one correspondence between k-colorings of G and assignments satisfying C_{k}(G).

2. Show that G is k-colorable if and only if C_{k}(G) is satisfiable.

3. Show that G is k-colorable if and only if each finite subgraph of G is k-colorable.

Definition 1.8.3. A partial ordering consists of a set P together with a binary relation ≤_{P} such that

1. a ≤_{P} a for all a ∈ P (reflexivity);

2. a ≤_{P} b, b ≤_{P} c imply a ≤_{P} c (transitivity);

3. a ≤_{P} b, b ≤_{P} a imply a = b (antisymmetry).

Example 1.8.4. Let P = ℕ^{+} = {1, 2, 3, …, n, …} = the set of positive integers.

1. Let ≤_{P} be the usual order relation on P, i.e., m ≤_{P} n if and only if m ≤ n.

2. Let ≤_{P} be the divisibility ordering of P, i.e., m ≤_{P} n if and only if m is a divisor of n.

Definition 1.8.5. Let P, ≤_{P} be a partial ordering.

1. Two elements a, b ∈ P are comparable if either a ≤_{P} b or b ≤_{P} a. Otherwise they are incomparable.

2. A chain is a set X ⊆ P such that any two elements of X are comparable.

3. An antichain is a set X ⊆ P such that any two distinct elements of X are incomparable.

Exercise 1.8.6. Let P, ≤_{P} be a partial ordering, and let k be a positive integer.

1. Use the Compactness Theorem to show that P is the union of k chains if and only if each finite subset of P is the union of k chains.

2. Dilworth’s Theorem says that P is the union of k chains if and only if every antichain is of size ≤ k. Show that Dilworth’s Theorem for arbitrary partial orderings follows from Dilworth’s Theorem for finite partial orderings.

Predicate Calculus

2.1 Formulas and Sentences

Definition 2.1.1 (languages). A language L is a set of predicates, each predicate P of L being designated as n-ary for some nonnegative^{1} integer n.

Definition 2.1.2 (variables and quantifiers). We assume the existence of a fixed, countably infinite set of symbols x, y, z, … known as variables. We introduce two new symbols: the universal quantifier (∀) and the existential quantifier (∃). They are read as “for all” and “there exists”, respectively.

Definition 2.1.3 (formulas). Let L be a language, and let U be a set. It is understood that U is disjoint from the set of variables. The set of L-U-formulas is generated as follows.

1. An atomic L-U-formula is an expression of the form P e_{1} ⋯ e_{n} where P is an n-ary predicate of L and each of e_{1}, …, e_{n} is either a variable or an element of U.

2. Each atomic L-U-formula is an L-U-formula.

3. If A is an L-U-formula, then ¬ A is an L-U-formula.

4. If A and B are L-U-formulas, then A ∧ B, A ∨ B, A ⇒ B, A ⇔ B are L-U-formulas.

5. If x is a variable and A is an L-U-formula, then ∀x A and ∃x A are L-U-formulas.

Definition 2.1.4 (degree). The degree of a formula is the number of occurrences of propositional connectives ¬ , ∧ , ∨ , ⇒ , ⇔ and quantifiers ∀, ∃ in it.

1It will be seen that 0-ary predicates behave as propositional atoms. Thus the predicate calculus is an extension of the propositional calculus.

Definition 2.1.5. An L-formula is an L-∅-formula, i.e., an L-U-formula where U = ∅, the empty set. Remark 2.1.6. If U is a subset of U′, then every L-U-formula is automatically an L-U′-formula. In particular, every L-formula is automatically an L-U-formula, for any set U. Definition 2.1.7. In situations where the language L is understood from context, an L-U-formula may be called a U-formula, and an L-formula a formula. Definition 2.1.8 (substitution). If A is an L-U-formula and x is a variable and a ∈ U, we define an L-U-formula A[x/a] as follows.

1. If A is atomic, then A[x/a] = the result of replacing each occurrence of x in A by a.

2. (¬ A)[x/a] = ¬ A[x/a].

3. (A ∧ B)[x/a] = A[x/a] ∧ B[x/a].

4. (A ∨ B)[x/a] = A[x/a] ∨ B[x/a].

5. (A ⇒ B)[x/a] = A[x/a] ⇒ B[x/a].

6. (A ⇔ B)[x/a] = A[x/a] ⇔ B[x/a].

7. (∀x A)[x/a] = ∀x A.

8. (∃x A)[x/a] = ∃x A.

9. If y is a variable other than x, then (∀y A)[x/a] = ∀y A[x/a].

10. If y is a variable other than x, then (∃y A)[x/a] = ∃y A[x/a]. Definition 2.1.9 (free variables). An occurrence of a variable x in an L-U-formula A is said to be bound in A if it is within the scope of a quantifier ∀x or ∃x in A. An occurrence of a variable x in an L-U-formula A is said to be free in A if it is not bound in A. A variable x is said to occur freely in A if there is at least one occurrence of x in A which is free in A. Exercise 2.1.10.

1. Show that A[x/a] is the result of substituting a for all free occurrences of x in A.

2. Show that x occurs freely in A if and only if A[x/a] ≠ A. Definition 2.1.11 (sentences). An L-U-sentence is an L-U-formula in which no variables occur freely. An L-sentence is an L-∅-sentence, i.e., an L-U-sentence where U = ∅, the empty set.

Remark 2.1.12. If U is a subset of U′, then every L-U-sentence is automatically an L-U′-sentence. In particular, every L-sentence is automatically an L-U-sentence, for any set U.

Definition 2.1.13. In situations where the language L is understood from context, an L-U-sentence may be called a U-sentence, and an L-sentence a sentence.

2.2 Structures and Satisfiability

Definition 2.2.1. Let U be a nonempty set, and let n be a nonnegative^{2} integer. U^{n} is the set of all n-tuples of elements of U, i.e.,

U^{n} = {⟨a_{1}, …, a_{n}⟩ | a_{1}, …, a_{n} ∈ U} .

An n-ary relation on U is a subset of U^{n}.

Definition 2.2.2. Let L be a language. An L-structure M consists of a nonempty set U_{M}, called the domain or universe of M, together with an n-ary relation P_{M} on U_{M} for each n-ary predicate P of L. An L-structure may be called a structure, in situations where the language L is understood from context.

Definition 2.2.3. Two L-structures M and M′ are said to be isomorphic if there exists an isomorphism of M onto M′, i.e., a one-to-one correspondence ϕ : U_{M} ≅ U_{M′} such that for all n-ary predicates P of L and all n-tuples ⟨a_{1}, …, a_{n}⟩ ∈ (U_{M})^{n}, ⟨a_{1}, …, a_{n}⟩ ∈ P_{M} if and only if ⟨ϕ(a_{1}), …, ϕ(a_{n})⟩ ∈ P_{M′}.

As usual in abstract mathematics, we are mainly interested in properties of structures that are invariant under isomorphism.

Lemma 2.2.4. Given an L-structure M, there is a unique valuation or assignment of truth values

v_{M} : {A | A is an L-U_{M}-sentence} → {T, F}

defined as follows:

1. v_{M}(P a_{1} ⋯ a_{n}) = \{ \begin{matrix}T & if ⟨a_{1}, …, a_{n}⟩ ∈ P_{M} , \\ F & if ⟨a_{1}, …, a_{n}⟩ ∉ P_{M} . \end{matrix}

2. v_{M}(¬ A) = \{ \begin{matrix}T & if v_{M}(A) = F , \\ F & if v_{M}(A) = T . \end{matrix}

3. v_{M}(A ∧ B) = \{ \begin{matrix}T & if v_{M}(A) = v_{M}(B) = T , \\ F & if at least one of v_{M}(A), v_{M}(B) = F . \end{matrix}

2In the special case n = 0 we obtain the notion of a 0-ary relation, i.e., a subset of {⟨⟩}.

There are only two 0-ary relations, {⟨⟩} and {}, corresponding to T and F respectively. Thus a 0-ary predicate behaves as a propositional atom.

4. v_{M}(A ∨ B) = \{ \begin{matrix}T & if at least one of v_{M}(A), v_{M}(B) = T , \\ F & if v_{M}(A) = v_{M}(B) = F . \end{matrix}

5. v_{M}(A ⇒ B) = v_{M}(¬ (A ∧ ¬ B)) .

6. v_{M}(A ⇔ B) = \{ \begin{matrix}T & if v_{M}(A) = v_{M}(B) , \\ F & if v_{M}(A) ≠ v_{M}(B) . \end{matrix}

7. v_{M}(∀x A) = \{ \begin{matrix}T & if v_{M}(A[x/a]) = T for all a ∈ U_{M} , \\ F & if v_{M}(A[x/a]) = F for at least one a ∈ U_{M} . \end{matrix}

8. v_{M}(∃x A) = \{ \begin{matrix}T & if v_{M}(A[x/a]) = T for at least one a ∈ U_{M} , \\ F & if v_{M}(A[x/a]) = F for all a ∈ U_{M} . \end{matrix}

Proof. The truth value v_{M}(A) is defined by recursion on L-U_{M}-sentences, i.e., by induction on the degree of A where A is an arbitrary L-U_{M}-sentence. □

Definition 2.2.5 (truth and satisfaction). Let M be an L-structure.

1. Let A be an L-U_{M}-sentence. We say that A is true in M if v_{M}(A) = T. We say that A is false in M if v_{M}(A) = F.

2. Let S be a set of L-U_{M}-sentences. We say that M satisfies S, abbreviated M ⊧ S, if all of the sentences of S are true in M.

Theorem 2.2.6.

1. If M and M′ are isomorphic L-structures and ϕ : M ≅ M′ is an isomorphism of M onto M′, then for all L-U_{M}-sentences A we have v_{M}(A) = v_{M′}(A′) where A′ = A[a_{1}/ϕ(a_{1}), …, a_{k}/ϕ(a_{k})].^{3} Here a_{1}, …, a_{k} are the elements of U_{M} which occur in A.

2. If M and M′ are isomorphic L-structures, then they are elementarily equivalent, i.e., they satisfy the same L-sentences. We shall see later that the converse does not hold in general.

Proof. We omit the proof of part 1. A more general result will be proved later as Theorem 2.7.3. Part 2 follows immediately from part 1. □

Definition 2.2.7 (satisfiability). Let S be a set of L-sentences. S is said to be satisfiable^{4} if there exists an L-structure M which satisfies S.

3We have extended the substitution notation 2.1.8 in an obvious way.

4Similarly, the notions of logical validity and logical consequence are defined for Lsentences, in the obvious way, using L-structures. An L-sentence is said to be logically valid if it is satisfied by all L-structures. An L-sentence is said to be a logical consequence of S if it is satisfied by all L-structures satisfying S.

Remark 2.2.8. Satisfiability is one of the most important concepts of mathematical logic. A key result known as the Compactness Theorem^{5} states that a set S of L-sentences is satisfiable if and only every finite subset of S is satisfiable.

The following related notion is of technical importance.

Definition 2.2.9 (satisfiability in a domain). Let U be a nonempty set. A set S of L-U-sentences is said to be satisfiable in the domain U if there exists an L-structure M such that M ⊧ S and U_{M} = U.

Remark 2.2.10. Let S be a set of L-sentences. Then S is satisfiable (according to Definition 2.2.7) if and only if S is satisfiable in some domain U.

Theorem 2.2.11. Let S be a set of L-sentences. If S is satisfiable in a domain U, then S is satisfiable in any domain of the same cardinality as U.

Proof. Suppose S is satisfiable in a domain U. Let M be an L-structure M satisfying S with U_{M} = U. Let U′ be any set of the same cardinality as U. Then there exists a one-to-one correspondence ϕ : U → U′. Let M′ be the L-structure with U_{M′} = U′, P_{M′} = {⟨ϕ(a_{1}), …, ϕ(a_{n})⟩ | ⟨a_{1}, …, a_{n}⟩ ∈ P_{M}} for all n-ary predicates P of L. Then M is isomorphic to M′. Hence, by Theorem 2.2.6, M′ ⊧ S. Thus S is satisfiable in the domain U′. □

Example 2.2.12. We exhibit a sentence A_{∞} which is satisfiable in an infinite domain but not in any finite domain. Our sentence A_{∞} is (1) ∧ (2) ∧ (3) with

\begin{matrix}(1) & ∀x ∀y ∀z ((Rxy ∧ Ryz) ⇒ Rxz) \\ (2) & ∀x ∀y (Rxy ⇒ ¬ Ryx) \\ (3) & ∀x ∃y Rxy \end{matrix}

See also Example 2.5.9.

Exercise 2.2.13. Let L be the language consisting of one binary predicate, R. Consider the following sentences:

(a) ∀x Rxx
(b) ∀x ¬ Rxx
(c) ∀x ∀y (Rxy ⇒ Ryx)
(d) ∀x ∀y (Rxy ⇒ ¬ Ryx)
(e) ∀x ∀y ∀z ((Rxy ∧ Ryz) ⇒ Rxz)
(f) ∀x ∃y Rxy

Which of subsets of this set of sentences are satisfiable? Verify your claims by exhibiting appropriate structures. Use the simplest possible structures.

5See Theorems 2.6.1 and 2.6.2 below.

Solution.

(a,c,e,f) is satisfiable: U = {1}, R = {⟨1, 1⟩}. (b,c,d,e) is satisfiable: U = {1}, R = { }. (b,c,f) is satisfiable: U = {1, 2}, R = {⟨1, 2⟩, ⟨2, 1⟩}. (b,d,e,f) is satisfiable: U = {1, 2, 3, …}, R = <.

These are the only maximal satisfiable sets, because: (a,b) is not satisfiable. (a,d) is not satisfiable. (b,c,e,f) is not satisfiable. (c,d,f) is not satisfiable.

Note: (d,e,f) is not satisfiable in any finite domain. Exercise 2.2.14.

1. Assume the following predicates:

Hx: x is a human Cx: x is a car T x: x is a truck Dxy: x drives y

Write formulas representing the obvious assumptions: no human is a car, no car is a truck, humans exist, cars exist, only humans drive, only cars and trucks are driven, etc.

2. Write formulas representing the following statements: (a) Everybody drives a car or a truck.

(b) Some people drive both.

(c) Some people don’t drive either.

(d) Nobody drives both.

3. Assume in addition the following predicate:

Ixy: x is identical to y Write formulas representing the following statements:

(a) Every car has at most one driver.

(b) Every truck has exactly two drivers.

(c) Everybody drives exactly one vehicle (car or truck). Solution.

1. No human is a car. ¬ ∃x (Hx ∧ Cx).

No car is a truck. ¬ ∃x (Cx ∧ T x). Humans exist. ∃x Hx. Cars exist. ∃x Cx. Only humans drive. ∀x ((∃y Dxy) ⇒ Hx). Only cars and trucks are driven. ∀x ((∃y Dyx) ⇒ (Cx ∨ T x)). Some humans drive. ∃x (Hx ∧ ∃y Dxy). Some humans do not drive. ∃x (Hx ∧ ¬ ∃y Dxy). Some cars are driven. ∃x (Cx ∧ ∃y Dyx). Some cars are not driven (e.g., old wrecks). ∃x (Cx ∧ ¬ ∃y Dyx). Etc, etc.

2. (a) ∀x (Hx ⇒ ∃y (Dxy ∧ (Cy ∨ T y))). (b) ∃x (Hx ∧ ∃y ∃z (Dxy ∧ Cy ∧ Dxz ∧ T z)).

(c) ∃x (Hx ∧ ¬ ∃y (Dxy ∧ (Cy ∨ T y))).

(d) ¬ ∃x (Hx ∧ ∃y ∃z (Dxy ∧ Dxz ∧ Cy ∧ T z)).

3. (a) ∀x (Cx ⇒ ∀y ∀z ((Dyx ∧ Dzx) ⇒ Iyz)). (b) ∀x (T x ⇒ ∃y ∃z ((¬ Iyz) ∧ Dyx ∧ Dzx ∧ ∀w (Dwx ⇒ (Iwy ∨ Iwz)))).

(c) ∀x (Hx ⇒ ∃y (Dxy ∧ (Cy ∨ T y) ∧ ∀z ((Dxz ∧ (Cz ∨ T z)) ⇒ Iyz))).

Exercise 2.2.15. Assume the following predicates:

Ixy: x = y P xyz: x · y = z

Write formulas representing the axioms for a group: axioms for equality, existence and uniqueness of products, associative law, existence of an identity element, existence of inverses. Solution.

1. equality axioms:

(a) ∀x Ixx (reflexivity)

(b) ∀x ∀y (Ixy ⇔ Iyx) (symmetry)

(c) ∀x ∀y ∀z ((Ixy ∧ Iyz) ⇒ Ixz) (transitivity)

(d) ∀x ∀x′ ∀y ∀y′ ∀z ∀z′ ((Ixx′ ∧ Iyy′ ∧ Izz′) ⇒ (P xyz ⇔ P x′y′z′)) (congruence with respect to P).

2. existence and uniqueness of products:

(a) ∀x ∀y ∃z P xyz (existence)

(b) ∀x ∀y ∀z ∀w ((P xyz ∧ P xyw) ⇒ Izw) (uniqueness).

3. associative law:

∀x ∀y ∀z ∃u ∃v ∃w (P xyu ∧ P yzv ∧ P uzw ∧ P xvw).

4. existence of identity element:

∃u ∀x (P uxx ∧ P xux).

5. existence of inverses:

∃u ∀x ∃y (P uxx ∧ P xux ∧ P xyu ∧ P yxu).

Exercise 2.2.16. Let G be a group. The order of an element a ∈ G is the smallest positive integer n such that a^{n} = e. Here e denotes the identity element of G, and

a^{n} = \underbrace{a · · · · · a}_{n times} .

Using only the predicates P xyz (“x · y = z”) and Ixy (“x = y”), write a predicate calculus sentence S such that, for any group G, G satisfies S if and only if G has no elements of order 2 or 3.

Solution. ¬ ∃x ∃y (P xxx ∧ (¬ P yyy) ∧ (P yyx ∨ ∃z (P yyz ∧ P zyx))).

2.3 The Tableau Method

Definition 2.3.1. Fix a countably infinite set V = {a_{1}, a_{2}, …, a_{n}, …} = {a, b, c, …}. The elements of V will be called parameters. If L is a language, L-V -sentences will be called sentences with parameters.

Definition 2.3.2. A (signed or unsigned) tableau is a rooted dyadic tree where each node carries a (signed or unsigned) L-V -sentence. The tableau rules for the predicate calculus are the same as those for the propositional calculus, with the following additional rules.

Signed:

⋮ ; T ∀x A ; ⋮ ; | ; T A[x/a]  ⋮ ; F ∃x A ; ⋮ ; | ; F A[x/a]

where a is an arbitrary parameter

⋮ ; T ∃x A ; ⋮ ; | ; T A[x/a]  ⋮ ; F ∀x A ; ⋮ ; | ; F A[x/a]

where a is a new parameter

Unsigned:

⋮ ; ∀x A ; ⋮ ; | ; A[x/a]  ⋮ ; ¬ ∃x A ; ⋮ ; | ; ¬ A[x/a]

where a is an arbitrary parameter

⋮ ; ∃x A ; ⋮ ; | ; A[x/a]  ⋮ ; ¬ ∀x A ; ⋮ ; | ; ¬ A[x/a]

where a is a new parameter

Remark 2.3.3. In the above tableau rules, “a is new” means that a does not occur in the path that is being extended. Or, we can insist that a not occur in the tableau that is being extended.

Remark 2.3.4. We are going to prove that the tableau method for predicate calculus is sound (Theorem 2.3.13) and complete (Theorem 2.5.5). In particular, a sentence A of the predicate calculus is logically valid if and only if there exists a finite closed signed tableau starting with F A, or equivalently a finite closed unsigned tableau starting with ¬ A.

Example 2.3.5. The signed tableau

F (∃x ∀y Rxy) ⇒ (∀y ∃x Rxy)
T ∃x ∀y Rxy
F ∀y ∃x Rxy
T ∀y Ray
F ∃x Rxb
T Rab
F Rab

is closed. Therefore, by the Soundness Theorem, (∃x ∀y Rxy) ⇒ (∀y ∃x Rxy) is logically valid.

Example 2.3.6. The unsigned tableau

¬ ((∃x (P x ∨ Qx)) ⇔ ((∃x P x) ∨ (∃x Qx)))
/ \

\begin{matrix}∃x (P x ∨ Qx) \\ ¬ ((∃x P x) ∨ (∃x Qx)) \\ ¬ ∃x P x \\ ¬ ∃x Qx \\ P a ∨ Qa \\ / \ \\ P a  Qa \\ ¬ P a  ¬ Qa \end{matrix}  \begin{matrix}¬ ∃x (P x ∨ Qx) \\ (∃x P x) ∨ (∃x Qx) \\ /  \ \\ \begin{matrix}∃x P x \\ P b \\ ¬ (P b ∨ Qb) \\ ¬ P b \\ ¬ Qb \end{matrix} & \begin{matrix}∃x Qx \\ Qc \\ ¬ (P c ∨ Qc) \\ ¬ P c \\ ¬ Qc \end{matrix} \end{matrix}

is closed. Therefore, by the Soundness Theorem,

(∃x (P x ∨ Qx)) ⇔ ((∃x P x) ∨ (∃x Qx))

is logically valid.

Exercises 2.3.7. Use signed tableaux to show that the following are logically valid.

1. (∀x (A ⇒ B)) ⇒ ((∀x A) ⇒ (∀x B))

Solution.

F (∀x (A ⇒ B)) ⇒ ((∀x A) ⇒ (∀x B))

T ∀x(A ⇒ B)

F (∀x A) ⇒ (∀x B)

T ∀x A F ∀x B F B[x/a] T A[x/a]

T (A ⇒ B)[x/a]

/ \

F A[x/a] T B[x/a]

2. (∃x (A ∨ B)) ⇔ ((∃x A) ∨ (∃x B))

Solution.

F (∃x (A ∨ B)) ⇔ ((∃x A) ∨ (∃x B))
/ \
T ∃x (A ∨ B)
F (∃x A) ∨ (∃x B)
T (A ∨ B)[x/a]
F ∃x A
F ∃x B
F A[x/a]
F B[x/a]
/ \
T A[x/a] T B[x/a]

F ∃x (A ∨ B)
T (∃x A) ∨ (∃x B)
/ \
T ∃x A T ∃x B
T A[x/a] T B[x/a]
F (A ∨ B)[x/a] F (A ∨ B)[x/a]
F A[x/a] F A[x/a]
F B[x/a] F B[x/a]

3. (∃x A) ⇔ (¬ ∀x ¬ A)

Solution.

F (∃x A) ⇔ (¬ ∀x ¬ A)
/ \
T ∃x A F ∃x A
F ¬ ∀x ¬ A T ¬ ∀x ¬ A
T A[x/a] F ∀x ¬ A
T ∀x ¬ A F (¬ A)[x/a]
T (¬ A)[x/a] T A[x/a]
F A[x/a] F A[x/a]

4. (∀x (A ∨ C)) ⇔ ((∀x A) ∨ C), provided x is not free in C

Solution.

F (∀x (A ∨ C)) ⇔ ((∀x A) ∨ C)
/ \
T ∀x (A ∨ C)
F (∀x A) ∨ C
F ∀x A
F C
F A[x/a]
T (A ∨ C)[x/a]
/ \
T A[x/a] T C

F ∀x (A ∨ C)
T (∀x A) ∨ C
F (A ∨ C)[x/a]
F A[x/a]
F C
/ \
T ∀x A T C
T A[x/a]

Exercise 2.3.8. Using the predicates Bx (“x is a barber in Podunk”), Cx (“x is a citizen of Podunk”), and Sxy (“x shaves y”), translate the following argument into a sentence of the predicate calculus.

There is a barber in Podunk who shaves exactly those citizens of Podunk who do not shave themselves. Therefore, there is a barber in Podunk who is not a citizen of Podunk.

Use an unsigned tableau to test this argument for logical validity.

Solution. (∃x (Bx ∧ ∀y (Cy ⇒ (Sxy ⇔ ¬ Syy)))) ⇒ ∃x (Bx ∧ ¬ Cx). A tableau starting with the negation of this sentence (left to the reader) closes off to show that the sentence is logically valid.

Exercise 2.3.9. Translate the following argument into the predicate calculus, and use appropriate methods to establish its validity or invalidity.

Anyone who can solve all logic problems is a good student. No student can solve every logic problem. Therefore, there are logic problems that no student can solve.

Exercise 2.3.10. Use an unsigned tableau to show that ∃x (P x ⇔ ∀y P y) is logically valid.

The rest of this section is devoted to proving the Soundness Theorem 2.3.13.

Definition 2.3.11.

1. An L-V -structure consists of an L-structure M together with a mapping ϕ : V → U_{M}. If A is an L-V -sentence, we write

A^{ϕ} = A[a_{1}/ϕ(a_{1}), …, a_{k}/ϕ(a_{k})]

where a_{1}, …, a_{k} are the parameters occurring in A. Note that A^{ϕ} is an L-U_{M}-sentence. Note also that, if A is an L-sentence, then A^{ϕ} = A.

2. Let S be a finite or countable set of (signed or unsigned) L-V -sentences. An L-V -structure M, ϕ is said to satisfy S if v_{M}(A^{ϕ}) = T for all A ∈ S. S is said to be satisfiable^{6} if there exists an L-V -structure satisfying S. Note that this definition is compatible with Definition 2.2.7.

3. Let τ be an L-tableau. We say that τ is satisfiable if at least one path of τ is satisfiable.

Lemma 2.3.12. Let τ and τ′ be tableaux such that τ′ is an immediate extension of τ, i.e., τ′ is obtained from τ by applying a tableau rule to a path of τ. If τ is satisfiable, then τ′ is satisfiable.

Proof. The proof consists of one case for each tableau rule. We consider some representative cases.

6Similarly, the notions of logical validity and logical consequence are extended to L-V - sentences, in the obvious way, using L-V -structures. An L-V -sentence is said to be logically valid if it satisfied by all L-V -structures. An L-V -sentence is said to be a logical consequence of S if it is satisfied by all L-V -structures satisfying S.

Case 1. Suppose that τ′ is obtained from τ by applying the rule

⋮
A ∨ B
⋮
/ \
A B

to the path θ in τ. Since τ is satisfiable, it has at least one satisfiable path, S. If S ≠ θ, then S is a path of τ′, so τ′ is satisfiable. If S = θ, then θ is satisfiable, so let M and ϕ : V → U_{M} satisfy θ. In particular v_{M}((A ∨ B)^{ϕ}) = T, so we have at least one of v_{M}(A^{ϕ}) = T and v_{M}(B^{ϕ}) = T. Thus M and ϕ satisfy at least one of θ, A and θ, B. Since these are paths of τ′, it follows that τ′ is satisfiable.

Case 2. Suppose that τ′ is obtained from τ by applying the rule

⋮
∀x A
⋮
|
A[x/a]

to the path θ in τ, where a is a parameter. Since τ is satisfiable, it has at least one satisfiable path, S. If S ≠ θ, then S is a path of τ′, so τ′ is satisfiable. If S = θ, then θ is satisfiable, so let M and ϕ : V → U_{M} satisfy θ. In particular v_{M}(∀x (A^{ϕ})) = v_{M}((∀x A)^{ϕ}) = T, so v_{M}(A^{ϕ}[x/c]) = T for all c ∈ U_{M}. In particular

v_{M}(A[x/a]^{ϕ}) = v_{M}(A^{ϕ}[x/ϕ(a)]) = T.

Thus M and ϕ satisfy θ, A[x/a]. Since this is a path of τ′, it follows that τ′ is satisfiable.

Case 3. Suppose that τ′ is obtained from τ by applying the rule

⋮
∃x A
⋮
|
A[x/a]

to the path θ in τ, where a is a new parameter. Since τ is satisfiable, it has at least one satisfiable path, S. If S ≠ θ, then S is a path of τ′, so τ′ is satisfiable. If S = θ, then θ is satisfiable, so let M and ϕ : V → U_{M} satisfy θ. In particular v_{M}(∃x (A^{ϕ})) = v_{M}((∃x A)^{ϕ}) = T, so v_{M}(A^{ϕ}[x/c]) = T for at least one c ∈ U_{M}. Fix such a c and define ϕ′ : V → U_{M} by putting ϕ′(a) = c, and ϕ′(b) = ϕ(b) for all b ≠ a, b ∈ V. Since a is new, we have B^{ϕ′} = B^{ϕ} for all B ∈ θ, and A^{ϕ′} = A^{ϕ}, hence A[x/a]^{ϕ′} = A^{ϕ′}[x/ϕ′(a)] = A^{ϕ}[x/c]. Thus v_{M}(B^{ϕ′}) = v_{M}(B^{ϕ}) = T for all B ∈ θ, and v_{M}(A[x/a]^{ϕ′}) = v_{M}(A^{ϕ}[x/c]) = T. Thus M and ϕ′ satisfy θ, A[x/a]. Since this is a path of τ′, it follows that τ′ is satisfiable. □

Theorem 2.3.13 (the Soundness Theorem). Let X_{1}, …, X_{k} be a finite set of (signed or unsigned) sentences with parameters. If there exists a finite closed tableau starting with X_{1}, …, X_{k}, then X_{1}, …, X_{k} is not satisfiable.

Proof. Let τ be a closed tableau starting with X_{1}, …, X_{k}. Thus there is a finite sequence of tableaux τ_{0}, τ_{1}, …, τ_{n} = τ such that

τ_{0} = X_{1} ; ⋮ ; X_{k}

and each τ_{i+1} is an immediate extension of τ_{i}. Suppose X_{1}, …, X_{k} is satisfiable. Then τ_{0} is satisfiable, and by induction on i using Lemma 2.3.12, it follows that all of the τ_{i} are satisfiable. In particular τ_{n} = τ is satisfiable, but this is impossible since τ is closed. □

2.4 Logical Equivalence

Definition 2.4.1. Given an L-V -formula A, let A′ = A[x_{1}/a_{1}, …, x_{k}/a_{k}], where x_{1}, …, x_{k} are the variables which occur freely in A, and a_{1}, …, a_{k} are parameters not occurring in A. Note that A′ has no free variables, i.e., it is an L-V -sentence. We define A to be satisfiable if and only if A′ is satisfiable, in the sense of Definition 2.3.11. We define A to be logically valid if and only if A′ is logically valid, in the sense of Definition 2.3.11.

Exercises 2.4.2. Let A be an L-V -formula.

1. Show that A is logically valid if and only if ¬ A is not satisfiable. Show that A is satisfiable if and only if ¬ A is not logically valid.

2. Let x be a variable. Show that A is logically valid if and only if ∀x A is logically valid. Show that A is satisfiable if and only if ∃x A is satisfiable.

3. Let x be a variable, and let a be a parameter not occurring in A. Show that A is logically valid if and only if A[x/a] is logically valid. Show that A is satisfiable if and only if A[x/a] is satisfiable.

Definition 2.4.3. Let A and B be L-V -formulas. A and B are said to be logically equivalent, written A ≡ B, if A ⇔ B is logically valid.

Exercise 2.4.4. Assume A ≡ B. Show that for any variable x, ∀x A ≡ ∀x B and ∃x A ≡ ∃x B. Show that for any variable x and parameter a, A[x/a] ≡ B[x/a].

Exercise 2.4.5. For an L-V -formula A, it is not in general true that A ≡ A′, where A′ is as in Definition 2.4.1. Also, it is not in general true that A ≡ ∀x A, or that A ≡ ∃x A, or that A ≡ A[x/a]. Give examples illustrating these remarks.

Solution. Let A be the formula P x where P is a unary predicate. It is straightforward to show that A ≢ A′, A ≢ ∀x A, A ≢ ∃x A and A ≢ A[x/a].

Exercise 2.4.6. Given L-V -formulas A and B, let A′ = A[x_{1}/a_{1}, …, x_{k}/a_{k}] and B′ = B[x_{1}/a_{1}, …, x_{k}/a_{k}], where x_{1}, …, x_{k} are the variables occurring freely in A and B, and a_{1}, …, a_{k} are parameters not occurring in A or in B. Show that A ≡ B if only if A′ ≡ B′.

Remark 2.4.7. The results of Exercises 1.3.3 and 1.3.4 and Remark 1.3.5 for formulas of the propositional calculus, also hold for formulas of the predicate calculus. In particular, if A_{1} ≡ A_{2}, then for any formula C containing A_{1} as a part, if we replace one or more occurrences of the part A_{1} by A_{2}, then the resulting formula is logically equivalent to C.

Remark 2.4.8. Some useful logical equivalences are:

1. (a) ∀x A ≡ A, provided x does not occur freely in A

(b) ∃x A ≡ A, provided x does not occur freely in A

(c) ∀x A ≡ ∀y A[x/y], provided y does not occur in A

(d) ∃x A ≡ ∃y A[x/y], provided y does not occur in A

Note that the last two equivalences provide for “replacement of bound variables”. In this way, we can convert any formula into a logically equivalent formula with the following properties: no variable occurs both free and bound, and each bound variable is bound by at most one quantifier.

2. (a) ∀x (A ∧ B) ≡ (∀x A) ∧ (∀x B)

(b) ∃x (A ∨ B) ≡ (∃x A) ∨ (∃x B)

(c) ∃x (A ⇒ B) ≡ (∀x A) ⇒ (∃x B)

Note however that, in general, ∃x (A ∧ B) ≢ (∃x A) ∧ (∃x B), and ∀x (A ∨ B) ≢ (∀x A) ∨ (∀x B), and ∀x (A ⇒ B) ≢ (∃x A) ⇒ (∀x B).

On the other hand, we have:

3. (a) ∃x (A ∧ B) ≡ A ∧ (∃x B), provided x does not occur freely in A

(b) ∃x (A ∧ B) ≡ (∃x A) ∧ B, provided x does not occur freely in B

(c) ∀x (A ∨ B) ≡ A ∨ (∀x B), provided x does not occur freely in A

(d) ∀x (A ∨ B) ≡ (∀x A) ∨ B, provided x does not occur freely in B

(e) ∃x (A ⇒ B) ≡ A ⇒ (∃x B), provided x does not occur freely in A

(f) ∀x (A ⇒ B) ≡ A ⇒ (∀x B), provided x does not occur freely in A

(g) ∃x (A ⇒ B) ≡ (∀x A) ⇒ B, provided x does not occur freely in B

(h) ∀x (A ⇒ B) ≡ (∃x A) ⇒ B, provided x does not occur freely in B

4. (a) ∃x ¬ A ≡ ¬ ∀x A

(b) ∀x ¬ A ≡ ¬ ∃x A

(c) ∀x A ≡ ¬ ∃x ¬ A

(d) ∃x A ≡ ¬ ∀x ¬ A

Definition 2.4.9 (variants). Let A be an L-F V -formula. A variant of A is any formula Â obtained from A by replacing some or all the bound variables of A by distinct new variables. Note that Â has the same free variables as A and is logically equivalent to A, in view of Remark 2.4.8, parts 1(c) and 1(d).

Example 2.4.10. Let A be ∀x ∃y Rxyz, and let Â be ∀u ∃v Ruvz. Then Â is a variant of A, hence Â ≡ A.

Definition 2.4.11 (prenex form). A formula is said to be quantifier-free if it contains no quantifiers. A formula is said to be in prenex form if it is of the form Q_{1}x_{1} ⋯ Q_{n}x_{n} B, where each Q_{i} is a quantifier (∀ or ∃), each x_{i} is a variable, and B is quantifier-free.

Example 2.4.12. The sentence

∀x ∀y ∃z ∀w (Rxy ⇒ (Rxz ∧ Rzy ∧ ¬ (Rzw ∧ Rwy)))

is in prenex form.

Exercise 2.4.13. Show that every L-V -formula is logically equivalent to an L-V -formula in prenex form. (Hint: Use the equivalences of Remark 2.4.8. First replace the given formula by a variant in which each bound variable is quantified only once and does not occur freely. Then use parts 3 and 4 to move all quantifiers to the front.)

Example 2.4.14. Consider the sentence (∃x P x) ∧ (∃x Qx). We wish to put this into prenex form. Applying the equivalences of Remark 2.4.8, we have

(∃x P x) ∧ (∃x Qx) ≡ (∃x P x) ∧ (∃y Qy)
≡ ∃x (P x ∧ (∃y Qy))
≡ ∃x ∃y (P x ∧ Qy)

and this is in prenex form.

Exercise 2.4.15. Find a sentence in prenex normal form which is logically equivalent to (∀x ∃y Rxy) ⇒ ¬ ∃x P x.

Solution. ∃x ∀y ∀z (Rxy ⇒ ¬ P z).

Exercises 2.4.16. Let A and B be L-V -formulas. Put the following into prenex form.

1. (∃x A) ∧ (∃x B)

2. (∀x A) ⇔ (∀x B)

3. (∀x A) ⇔ (∃x B)

Definition 2.4.17 (universal closure). Let A be an L-V -formula. The universal closure of A is the L-V -sentence A^{∗} = ∀x_{1} ⋯ ∀x_{k} A, where x_{1}, …, x_{k} are the variables which occur freely in A. Note that A^{∗∗} ≡ A^{∗}.

Exercises 2.4.18. Let A be an L-V -formula.

1. Show that A is logically valid if and only if A^{∗}, the universal closure of A, is logically valid.

2. It is not true in general that A ≡ A^{∗}. Give an example illustrating this.

3. It is not true in general that A is satisfiable if and only if A^{∗} is satisfiable. Give an example illustrating this.

4. For L-V -formulas A and B, it is not true in general that A ≡ B if and only if A^{∗} ≡ B^{∗}. Give an example illustrating this.

For completeness we state the following definition.

Definition 2.4.19. Let A_{1}, …, A_{k}, B be L-V -formulas. We say that B is a logical consequence of A_{1}, …, A_{k} if (A_{1} ∧ ⋯ ∧ A_{k}) ⇒ B is logically valid. This is equivalent to saying that the universal closure of (A_{1} ∧ ⋯ ∧ A_{k}) ⇒ B is logically valid.

Remark 2.4.20. A and B are logically equivalent if and only if each is a logical consequence of the other. A is logically valid if and only if A is a logical consequence of the empty set. ∃x A is a logical consequence of A[x/a], but the converse does not hold in general. A[x/a] is a logical consequence of ∀x A, but the converse does not hold in general.

2.5 The Completeness Theorem

Let U be a nonempty set, and let S be a set of (signed or unsigned) L-U-sentences.

Definition 2.5.1. S is closed if S contains a conjugate pair of L-U-sentences. In other words, for some L-U-sentence A, S contains T A, F A in the signed case, A, ¬ A in the unsigned case. S is open if it is not closed.

Definition 2.5.2. S is U-replete if S “obeys the tableau rules” with respect to U. We list some representative clauses of the definition.

1. If S contains T ¬ A, then S contains F A. If S contains F ¬ A, then S contains T A. If S contains ¬ ¬ A, then S contains A.

2. If S contains T A ∧ B, then S contains both T A and T B. If S contains F A ∧ B, then S contains at least one of F A and F B. If S contains A ∧ B, then S contains both A and B. If S contains ¬ (A ∧ B), then S contains at least one of ¬ A and ¬ B.

3. If S contains T ∃x A, then S contains T A[x/a] for at least one a ∈ U. If S contains F ∃x A, then S contains F A[x/a] for all a ∈ U. If S contains ∃x A, then S contains A[x/a] for at least one a ∈ U. If S contains ¬ ∃x A, then S contains ¬ A[x/a] for all a ∈ U.

4. If S contains T ∀x A, then S contains T A[x/a] for all a ∈ U. If S contains F ∀x A, then S contains F A[x/a] for at least one a ∈ U. If S contains ∀x A, then S contains A[x/a] for all a ∈ U. If S contains ¬ ∀x A, then S contains ¬ A[x/a] for at least one a ∈ U.

Lemma 2.5.3 (Hintikka’s Lemma). If S is U-replete and open^{7}, then S is satisfiable. In fact, S is satisfiable in the domain U.

Proof. Assume S is U-replete and open. We define an L-structure M by putting U_{M} = U and, for each n-ary predicate P of L,

P_{M} = {⟨a_{1}, …, a_{n}⟩ ∈ U^{n} | T P a_{1} ⋯ a_{n} ∈ S}

in the signed case, and

P_{M} = {⟨a_{1}, …, a_{n}⟩ ∈ U^{n} | P a_{1} ⋯ a_{n} ∈ S}

in the unsigned case.

We claim that for all L-U-sentences A,

(a) if S contains T A, then v_{M}(A) = T

(b) if S contains F A, then v_{M}(A) = F

in the signed case, and

(c) if S contains A, then v_{M}(A) = T

(d) if S contains ¬ A, then v_{M}(A) = F

in the unsigned case.

In both cases, the claim is easily proved by induction on the degree of A. We give the proof for some representative cases.

1. deg(A) = 0. In this case A is atomic, say A = P a_{1} ⋯ a_{n}.

(a) If S contains T P a_{1} ⋯ a_{n}, then by definition of M we have (a_{1}, …, a_{n}) ∈ P_{M}, so v_{M}(P a_{1} ⋯ a_{n}) = T.

7See also Exercise 2.5.7.

(b) If S contains F P a_{1} ⋯ a_{n}, then S does not contain T P a_{1} ⋯ a_{n} since S is open. Thus by definition of M we have (a_{1}, …, a_{n}) ∉ P_{M}, so v_{M}(P a_{1} ⋯ a_{n}) = F.

(c) If S contains P a_{1} ⋯ a_{n}, then by definition of M we have (a_{1}, …, a_{n}) ∈ P_{M}, so v_{M}(P a_{1} ⋯ a_{n}) = T.

(d) If S contains ¬ P a_{1} ⋯ a_{n}, then S does not contain P a_{1} ⋯ a_{n} since S is open. Thus by definition of M we have (a_{1}, …, a_{n}) ∉ P_{M}, so v_{M}(P a_{1} ⋯ a_{n}) = F.

2. deg(A) > 0 and A = ¬ B. Note that deg(B) < deg(A) so the inductive hypothesis applies to B.

3. deg(A) > 0 and A = B ∧ C. Note that deg(B) and deg(C) are < deg(A) so the inductive hypothesis applies to B and C.

(a) If S contains T B ∧ C, then by repleteness of S we see that S contains both TB and TC. Hence by inductive hypothesis we have v_{M}(B) = v_{M}(C) = T. Hence v_{M}(B ∧ C) = T.

(b) If S contains F B ∧ C, then by repleteness of S we see that S contains at least one of FB and FC. Hence by inductive hypothesis we have at least one of v_{M}(B) = F and v_{M}(C) = F. Hence v_{M}(B ∧ C) = F.

(c) If S contains B ∧ C, then by repleteness of S we see that S contains both B and C. Hence by inductive hypothesis we have v_{M}(B) = v_{M}(C) = T. Hence v_{M}(B ∧ C) = T.

(d) If S contains ¬ (B ∧ C), then by repleteness of S we see that S contains at least one of ¬ B and ¬ C. Hence by inductive hypothesis we have at least one of v_{M}(B) = F and v_{M}(C) = F. Hence v_{M}(B ∧ C) = F.

4. deg(A) > 0 and A = ∃x B. Note that for all a ∈ U we have deg(B[x/a]) < deg(A), so the inductive hypothesis applies to B[x/a].

5. deg(A) > 0 and A = ∀x B. Note that for all a ∈ U we have deg(B[x/a]) < deg(A), so the inductive hypothesis applies to B[x/a].

□

We shall now use Hintikka’s Lemma to prove the completeness of the tableau method. As in Section 2.3, Let V = {a_{1}, …, a_{n}, …} be the set of parameters. Recall that a tableau is a tree whose nodes carry L-V -sentences.

Lemma 2.5.4. Let τ_{0} be a finite tableau. By applying tableau rules, we can extend τ_{0} to a (possibly infinite) tableau τ with the following properties: every closed path of τ is finite, and every open path of τ is V -replete.

Proof. The idea is to start with τ_{0} and use tableau rules to construct a sequence of finite extensions τ_{0}, τ_{1}, …, τ_{i}, . . .. If some τ_{i} is closed, then the construction halts, i.e., τ_{j} = τ_{i} for all j ≥ i, and we set τ = τ_{i}. In any case, we set τ = τ_{∞} = ⋃_{i=0}^{∞} τ_{i}. In the course of the construction, we apply tableau rules systematically to ensure that τ_{∞} will have the desired properties, using the fact that V = {a_{1}, a_{2}, …, a_{n}, …} is countably infinite.

Here are the details of the construction. Call a node X of τ_{i} quasiuniversal if it is of the form T ∀x A or F ∃x A or ∀x A or ¬ ∃x A. Our construction begins with τ_{0}. Suppose we have constructed τ_{2i}. For each quasiuniversal node X of τ_{2i} and each n ≤ 2i, apply the appropriate tableau rule to extend each open path of τ_{2i} containing X by T A[x/a_{n}] or F A[x/a_{n}] or A[x/a_{n}] or ¬ A[x/a_{n}] as the case may be. Let τ_{2i+1} be the finite tableau so obtained. Next, for each non-quasiuniversal node X of τ_{2i+1}, extend each open path containing X by applying the appropriate tableau rule. Again, let τ_{2i+2} be the finite tableau so obtained.

In this construction, a closed path is never extended, so all closed paths of τ_{∞} are finite. In addition, the construction ensures that each open path of τ_{∞} is V -replete. Thus τ_{∞} has the desired properties. This proves our lemma. □

Theorem 2.5.5 (the Completeness Theorem). Let X_{1}, …, X_{k} be a finite set of (signed or unsigned) sentences with parameters. If X_{1}, …, X_{k} is not satisfiable, then there exists a finite closed tableau starting with X_{1}, …, X_{k}. If X_{1}, …, X_{k} is satisfiable, then X_{1}, …, X_{k} is satisfiable in the domain V.

Proof. By Lemma 2.5.4 there exists a (possibly infinite) tableau τ starting with X_{1}, …, X_{k} such that every closed path of τ is finite, and every open path of τ is V -replete. If τ is closed, then by König’s Lemma (Theorem 1.6.6), τ is finite. If τ is open, let S be an open path of τ. Then S is V -replete. By Hintikka’s Lemma 2.5.3, S is satisfiable in V. Hence X_{1}, …, X_{k} is satisfiable in V. □

Definition 2.5.6. Let L, U, and S be as in Definition 2.5.1. S is said to be atomically closed if S contains a conjugate pair of atomic L-U-sentences. In other words, for some n-ary L-predicate P and a_{1}, …, a_{n} ∈ U, S contains T P a_{1} ⋯ a_{n}, F P a_{1} ⋯ a_{n} in the signed case, and P a_{1} ⋯ a_{n}, ¬ P a_{1} ⋯ a_{n} in the unsigned case. S is atomically open if it is not atomically closed.

Exercise 2.5.7. Show that Lemmas 2.5.3 and 2.5.4 and Theorem 2.5.5 continue to hold with “closed” (“open”) replaced by “atomically closed” (“atomically open”).

Remark 2.5.8. Corollaries 1.5.9, 1.5.10, 1.5.11 carry over from the propositional calculus to the predicate calculus. In particular, the tableau method provides a test for logical validity of sentences of the predicate calculus.

Note however that the test is only partially effective. If a sentence A is logically valid, we will certainly find a finite closed tableau starting with ¬ A. But if A is not logically valid, we will not necessarily find a finite tableau which demonstrates this. See the following example.

Example 2.5.9. In 2.2.12 we have seen an example of a sentence A_{∞} which is satisfiable in a countably infinite domain but not in any finite domain. It is instructive to generate a tableau starting with A_{∞}.

A_{∞}
⋮
∀x ∀y ∀z ((Rxy ∧ Ryz) ⇒ Rxz)
∀x ∀y (Rxy ⇒ ¬ Ryx)
∀x ∃y Rxy
∃y Ra_{1}y
Ra_{1}a_{2}
∀y (Ra_{1}y ⇒ ¬ Rya_{1})
Ra_{1}a_{2} ⇒ ¬ Ra_{2}a_{1}
/ \
¬ Ra_{1}a_{2} ¬ Ra_{2}a_{1}
∃y Ra_{2}y
Ra_{2}a_{3}
⋮
¬ Ra_{3}a_{2}
∀y ∀z ((Ra_{1}y ∧ Ryz) ⇒ Ra_{1}z)
∀z ((Ra_{1}a_{2} ∧ Ra_{2}z) ⇒ Ra_{1}z)
(Ra_{1}a_{2} ∧ Ra_{2}a_{3}) ⇒ Ra_{1}a_{3})
/ \
¬ (Ra_{1}a_{2} ∧ Ra_{2}a_{3}) Ra_{1}a_{3}
/  \  ⋮
¬ Ra_{1}a_{2}  ¬ Ra_{2}a_{3}  ¬ Ra_{3}a_{1}

∃y Ra_{3}y ; Ra_{3}a_{4} ; ⋮

An infinite open path gives rise (via the proof of Hintikka’s Lemma) to an infinite L-structure M with U_{M} = {a_{1}, a_{2}, …, a_{n}, …}, R_{M} = {⟨a_{m}, a_{n}⟩ | 1 ≤ m < n}. Clearly M ⊧ A_{∞}.

Remark 2.5.10. In the course of applying a tableau test, we will sometimes find a finite open path which is U-replete for some finite set of parameters U ⊆ V. In this case, the proof of Hintikka’s Lemma provides a finite L-structure with domain U.

Example 2.5.11. Let A be the sentence (∀x (P x ∨ Qx)) ⇒ ((∀x P x) ∨ (∀x Qx)).

Testing A for logical validity, we have:

¬ A
∀x (P x ∨ Qx)
¬ ((∀x P x) ∨ (∀x Qx))
¬ ∀x P x
¬ ∀x Qx
¬ P a
¬ Qb
P a ∨ Qa
P b ∨ Qb
/ \
P a Qa
/ \
P b Qb

This tableau has a unique open path, which gives rise (via the proof of Hintikka’s Lemma) to a finite L-structure M with U_{M} = {a, b}, P_{M} = {b}, Q_{M} = {a}. Clearly M falsifies A.

Exercise 2.5.12. Using the predicate Rxy (“x is an ancestor of y”), translate the following argument into a sentence of the predicate calculus.

Every ancestor of an ancestor of an individual is an ancestor of the same individual. No individual is his own ancestor. Therefore, there is an individual who has no ancestor.

Is this argument valid? Justify your answer by means of an appropriate structure or tableau.

Solution. ((∀x ∀y ((∃z (Rxz ∧ Rzy)) ⇒ Rxy)) ∧ ¬ ∃x Rxx) ⇒ ∃x ¬ ∃y Ryx. A tableau starting with the negation of this sentence (left to the reader) fails to close off. The structure (ℕ, >_{ℕ}) falsifies the sentence, thus showing that it is not logically valid.

Exercise 2.5.13. Using the predicates Sx (“x is a set”) and Exy (“x is a member of y”), translate the following into a sentence of the predicate calculus.

There exists a set whose members are exactly those sets which are not members of themselves.

Use an unsigned tableau to test your sentence for consistency, i.e., satisfiability.

Exercise 2.5.14. Using the predicates Sx (“x is Socrates”), Hx (“x is a man”), Mx (“x is mortal”), translate the following argument into a sentence of the predicate calculus.

Socrates is a man. All men are mortal. Therefore, Socrates is mortal.

Use an unsigned tableau to test whether the argument is valid.

Exercises 2.5.15.

1. Using the predicates Sx (“x can solve this problem”), Mx (“x is a mathematician”), Jx (“x is Joe”), translate the following argument into a sentence of the predicate calculus.

If anyone can solve this problem, some mathematician can solve it. Joe is a mathematician and cannot solve it. Therefore, nobody can solve it.

Use an unsigned tableau to test whether the argument is valid.

2. Using the same predicates as above, translate the following argument into a sentence of the predicate calculus.

Any mathematician can solve this problem if anyone can. Joe is a mathematician and cannot solve it. Therefore, nobody can solve it.

Use an unsigned tableau to test whether the argument is valid.

2.6 The Compactness Theorem

Theorem 2.6.1 (the Compactness Theorem, countable case). Let S be a countably infinite set of sentences of the predicate calculus. S is satisfiable if and only if each finite subset of S is satisfiable.

Proof. We combine the ideas of the proofs of the Countable Compactness Theorem for propositional calculus (Theorem 1.7.1) and the Completeness Theorem for predicate calculus (Theorem 2.5.5).

Details: Let S = {A_{0}, A_{1}, …, A_{i}, …}. Start by letting τ_{0} be the empty tableau. Suppose we have constructed τ_{2i}. Extend τ_{2i} to τ′_{2i} by appending A_{i} to each open path of τ_{2i}. Since {A_{0}, A_{1}, …, A_{i}} is satisfiable, τ′_{2i} has at least one open path. Now extend τ′_{2i} to τ_{2i+1} and then to τ_{2i+2} as in the proof of Lemma 2.5.4. Finally put τ = τ_{∞} = ⋃_{i=1}^{∞} τ_{i}. As in Lemma 2.5.4 we have that every closed path of τ is finite, and every open path of τ is V -replete. Note also that τ is an infinite, finitely branching tree. By König’s Lemma (Theorem 1.6.6), let S′ be an infinite path in τ. Then S′ is a V -replete open set which contains S. By Hintikka’s Lemma for the predicate calculus (Lemma 2.5.3), S′ is satisfiable. Hence S is satisfiable. □

Theorem 2.6.2 (the Compactness Theorem, uncountable case). Let S be an uncountable set of sentences of the predicate calculus. S is satisfiable if and only if each finite subset of S is satisfiable.

Proof. Assume that S is finitely satisfiable. For each sentence A ∈ S of the form ∃x B or ¬ ∀x B, introduce a new parameter c_{A}. Let U_{S} be the set of parameters so introduced. Let S′ be S together with the sentences B[x/c_{A}] or ¬ B[x/c_{A}] as the case may be, for all c_{A} ∈ U_{S}. Then S′ is a set of L-U_{S}-sentences, and it is easy to verify that S′ is finitely satisfiable. By Zorn’s Lemma, let S′′ be a maximal finitely satisfiable set of L-U_{S}-sentences extending S′.

Now inductively define S_{0} = S, S_{n+1} = S′′_{n}, S_{∞} = ⋃_{n=0}^{∞} S_{n}, U = ⋃_{n=0}^{∞} U_{S_{n}}. It is straightforward to verify that S_{∞} is U-replete and open. Hence, by Hintikka’s Lemma, S_{∞} is satisfiable in the domain U. Since S ⊆ S_{∞}, it follows that S is satisfiable in U. □

Exercise 2.6.3. Let L be a language consisting of a binary predicate R and some additional predicates. Let M = (U_{M}, R_{M}, …) be an L-structure such that (U_{M}, R_{M}) is isomorphic to (ℕ, <_{ℕ}). Note that M contains no infinite R-descending sequence. Show that there exists an L-structure M′ such that:

1. M and M′ satisfy the same L-sentences.

2. M′ contains an infinite R-descending sequence. In other words, there exist elements a′_{1}, a′_{2}, …, a′_{n}, … ∈ U_{M′} such that ⟨a′_{n+1}, a′_{n}⟩ ∈ R_{M′} for all n = 1, 2, . . ..

Hint: Use the Compactness Theorem.

Exercise 2.6.4. Generalize Exercise 2.6.3 replacing (ℕ, <_{ℕ}) by an arbitrary infinite linear ordering with no infinite descending sequence. Show that M′ can be obtained such that (U_{M′}, R_{M′}) is a linear ordering which contains an infinite descending sequence.

Exercise 2.6.5. Let L = {R, …} be a language which includes a binary predicate R. Let S be a set of L-sentences. Assume that for each n ≥ 1 there exists an L-structure (U_{n}, R_{n}, …) satisfying S and containing elements a_{n1}, …, a_{nn} such that ⟨a_{ni}, a_{nj}⟩ ∈ R_{n} for all i and j with 1 ≤ i < j ≤ n. Prove that there there exists an L-structure (U_{∞}, R_{∞}, …) satisfying S and containing elements a_{∞i}, i = 1, 2, … such that ⟨a_{∞i}, a_{∞j}⟩ ∈ R_{∞} for all i and j with 1 ≤ i < j.

Solution. Let L^{∗} = L ∪ {P_{1}, P_{2}, …} where P_{1}, P_{2}, … are new unary predicates. Let S^{∗} be S plus ∃x P_{i}x plus ∀x ∀y ((P_{i}x ∧ P_{j}y) ⇒ Rxy), 1 ≤ i < j. Consider the L^{∗}-structures (U_{n}, R_{n}, …, P_{n1}, …, P_{nn}, …), n ≥ 1, where P_{ni} = {a_{ni}} for 1 ≤ i ≤ n, and P_{ni} = {} for i > n. Clearly each finite subset of S^{∗} is satisfied by all but finitely many of these structures. It follows by the Compactness Theorem that S^{∗} is satisfiable. Let (U_{∞}, R_{∞}, …, P_{∞1}, P_{∞2}, …) be an L^{∗}-structure satisfying S^{∗}. Clearly the L-structure (U_{∞}, R_{∞}, …) has the desired properties.

2.7 Satisfiability in a Domain

The notion of satisfiability in a domain was introduced in Definition 2.2.9.

Theorem 2.7.1. Let S be a set of L-sentences.

1. Assume that S is finite or countably infinite. If S is satisfiable, then S is satisfiable in a countably infinite domain.

2. Assume that S is of cardinality κ ≥ ℵ_{0}. If S is satisfiable, then S is satisfiable in a domain of cardinality κ.

Proof. Parts 1 and 2 follow easily from the proofs of Compactness Theorems 2.6.1 and 2.6.2, respectively. In the countable case we have that S is satisfiable in V, which is countably infinite. In the uncountable case we have that S is satisfiable in U, where U is as in the proof of 2.6.2. By the arithmetic of infinite cardinal numbers, the cardinality of U is κ · ℵ_{0} = κ. □

In Example 2.2.12 we have seen a sentence A_{∞} which is satisfiable in a countably infinite domain but not in any finite domain. Regarding satisfiability in finite domains, we have:

Example 2.7.2. Given a positive integer n, we exhibit a sentence A_{n} which is satisfiable in a domain of cardinality n but not in any domain of smaller cardinality. Our sentence A_{n} is (1) ∧ (2) ∧ (3) with

\begin{matrix}(1) & ∀x ∀y ∀z ((Rxy ∧ Ryz) ⇒ Ryz) \\ (2) & ∀x ∀y (Rxy ⇒ ¬ Ryx) \\ (3) & ∃x_{1} ⋯ ∃x_{n} (Rx_{1}x_{2} ∧ Rx_{2}x_{3} ∧ ⋯ ∧ Rx_{n−1}x_{n}) \end{matrix}

On the other hand, we have:

Theorem 2.7.3. Let M and M′ be L-structures. Assume that there exists an onto mapping ϕ : U_{M} → U_{M′} such that for all n-ary predicates P of L and all n-tuples ⟨a_{1}, …, a_{n}⟩ ∈ (U_{M})^{n}, ⟨a_{1}, …, a_{n}⟩ ∈ P_{M} if and only if ⟨ϕ(a_{1}), …, ϕ(a_{n})⟩ ∈ P_{M′}. Then as in Theorem 2.2.6 we have v_{M}(A) = v_{M′}(A′) for all L-U_{M}-sentences A, where A′ = A[a_{1}/ϕ(a_{1}), …, a_{k}/ϕ(a_{k})]. In particular, M and M′ satisfy the same L-sentences.

Proof. The proof is by induction on the degree of A. Suppose for example that A = ∀x B. Then by definition of v_{M} we have that v_{M}(A) = T if and only if v_{M}(B[x/a]) = T for all a ∈ U_{M}. By inductive hypothesis, this holds if and only if v_{M′}(B[x/a]′) = T for all a ∈ U_{M}. But for all a ∈ U_{M} we have B[x/a]′ = B′[x/ϕ(a)]. Thus our condition is equivalent to v_{M′}(B′[x/ϕ(a)]) = T for all a ∈ U_{M}. Since ϕ : U_{M} → U_{M′} is onto, this is equivalent to v_{M′}(B′[x/b]) = T for all b ∈ U_{M′}. By definition of v_{M′} this is equivalent to v_{M′}(∀x B′) = T. But ∀x B′ = A′, so our condition is equivalent to v_{M′}(A′) = T. □

Corollary 2.7.4. Let S be a set of L-sentences. If S is satisfiable in a domain U, then S is satisfiable in any domain of the same or larger cardinality.

Proof. Suppose S is satisfiable in domain U. Let U′ be a set of cardinality greater than or equal to that of U. Let ϕ : U′ → U be onto. If M is any L-structure with U_{M} = U, we can define an L-structure M′ with U_{M′} = U′ by putting P_{M′} = {⟨a_{1}, …, a_{n}⟩ | ⟨ϕ(a_{1}), …, ϕ(a_{n})⟩ ∈ P_{M}} for all n-ary predicates P of L. By Theorem 2.7.3, M and M′ satisfy the same L-sentences. In particular, if M ⊧ S, then M′ ⊧ S. □

Remark 2.7.5. We shall see later^{8} that Theorem 2.7.3 and Corollary 2.7.4 fail for normal satisfiability.

8See Section 4.1.

Proof Systems for Predicate Calculus

3.1 Introduction to Proof Systems

Definition 3.1.1. An abstract proof system consists of a set 𝔛 together with a relation ℜ ⊆ ⋃_{k=0}^{∞} 𝔛^{k+1}. Elements of 𝔛 are called objects. Elements of ℜ are called rules of inference. An object X ∈ 𝔛 is said to be derivable, or provable, if there exists a finite sequence of objects X_{1}, …, X_{n} such that X_{n} = X and, for each i ≤ n, there exist j_{1}, …, j_{k} < i such that ⟨X_{j_{1}}, …, X_{j_{k}}, X_{i}⟩ ∈ ℜ. The sequence X_{1}, …, X_{n} is called a derivation of X, or a proof of X.

Notation 3.1.2. For k ≥ 1 it is customary to write

\frac{X_{1} ⋯ X_{k}}{Y}

indicating that ⟨X_{1}, …, X_{k}, Y ⟩ ∈ ℜ. This is to be understood as “from the premises X_{1}, …, X_{k} we may immediately infer the conclusion Y ”. For k = 0 we may write

\overline{Y}

or simply Y, indicating that ⟨Y ⟩ ∈ ℜ. This is to be understood as “we may immediately infer Y from no premises”, or “we may assume Y ”.

Definition 3.1.3. Let L be a language. Recall that V is the set of parameters. A Hilbert-style proof system for L is a proof system with the following properties:

1. The objects are sentences with parameters. In other words,

𝔛 = {A | A is an L-V -sentence}.

2. For each rule of inference

\frac{A_{1} ⋯ A_{k}}{B}

(i.e., ⟨A_{1}, …, A_{k}, B⟩ ∈ ℜ), we have that B is a logical consequence of A_{1}, …, A_{k}. This property is known as soundness. It implies that every L-V -sentence which is derivable is logically valid.

3. For all L-V -sentences A, B, we have a rule of inference ⟨A, A ⇒ B, B⟩ ∈ ℜ, i.e.,

\frac{A A ⇒ B}{B} .

In other words, from A and A ⇒ B we immediately infer B. This collection of inference rules is known as modus ponens.

4. An L-V -sentence A is logically valid if and only if A is derivable. This property is known as completeness.

Remark 3.1.4. In Section 3.3 we shall exhibit a particular Hilbert-style proof system, LH . The soundness of LH will be obvious. In order to verify the completeness of LH , we shall first prove a result known as the Companion Theorem, which is also of interest in its own right.

3.2 The Companion Theorem

In this section we shall comment on the notion of logical validity for sentences of the predicate calculus. We shall analyze logical validity into two components: a propositional component (quasitautologies), and a quantificational component (companions).

Definition 3.2.1 (quasitautologies).

1. A tautology is a propositional formula which is logically valid.

2. A quasitautology is an L-V -sentence of the form F [p_{1}/A_{1}, …, p_{k}/A_{k}], where F is a tautology, p_{1}, …, p_{k} are the atoms occurring in F, and A_{1}, …, A_{k} are L-V -sentences.

For example, p ⇒ (q ⇒ p) is a tautology. This implies that, for all L-V -sentences A and B, A ⇒ (B ⇒ A) is a quasitautology.

Remarks 3.2.2.

1. Obviously, every quasitautology is logically valid.

2. There is a decision procedure^{1} for quasitautologies. One such decision procedure is based on truth tables. Another is based on propositional tableaux.

1In other words, there is a Turing algorithm which, given an L-V -sentence A as input, will eventually halt with output 1 if A is a quasitautology, 0 if A is not a quasitautology.

3. It can be shown that there is no decision procedure for logical validity. (This result is known as Church’s Theorem.) Therefore, in relation to the problem of characterizing logical validity, we regard the quasitautologies as trivial.

Let A be an L-V -sentence.

Definition 3.2.3 (companions). A companion of A is any L-V -sentence of one of the forms

\begin{matrix}(1) & (∀x B) ⇒ B[x/a] \\ (2) & B[x/a] ⇒ (∀x B) \\ (3) & (∃x B) ⇒ B[x/a] \\ (4) & B[x/a] ⇒ (∃x B) \end{matrix}

where, in (2) and (3), the parameter a may not occur in A or in B.

Lemma 3.2.4. Let C be a companion of A.

1. A is satisfiable if and only if C ∧ A is satisfiable.

2. A is logically valid if and only if C ⇒ A is logically valid.

Proof. Let C be a companion of A.

For part 1, assume that A is satisfiable. In accordance with Definition 2.3.11, let M, ϕ be an L-V -structure satisfying A. If C is of the form 3.2.3(1) or 3.2.3(4), then C is logically valid, hence M, ϕ satisfies C ∧ A. Next, consider the case when C is of the form 3.2.3(2). If M, ϕ satisfies ∀x B, then M, ϕ satisfies C. Otherwise we have v_{M}(∀x B^{ϕ}) = F, so let c ∈ U_{M} be such that v_{M}(B^{ϕ}[x/c]) = F. Define ϕ′ : V → U_{M} by putting ϕ′(a) = c, ϕ′(b) = ϕ(b) for b ≠ a. Since a does not occur in A, we have that M, ϕ′ satisfies A. Also, since a does not occur in B, we have B[x/a]^{ϕ′} = B^{ϕ′}[x/c] = B^{ϕ}[x/c], hence v_{M}(B[x/a]^{ϕ′}) = v_{M}(B^{ϕ}[x/c]) = F, i.e., M, ϕ′ satisfies ¬ B[x/a]. Thus M, ϕ′ satisfies C ∧ A. The case when C is of the form 3.2.3(3) is handled similarly.

For part 2 note that, since C is a companion of A, C is a companion of ¬ A. Thus we have that A is logically valid if and only if ¬ A is not satisfiable, if and only if C ∧ ¬ A is not satisfiable (by part 1), if and only if ¬ (C ∧ ¬ A) is logically valid, i.e., C ⇒ A is logically valid. □

Definition 3.2.5 (companion sequences). A companion sequence of A is a finite sequence C_{1}, …, C_{n} such that, for each i < n, C_{i+1} is a companion of

(C_{1} ∧ ⋯ ∧ C_{i}) ⇒ A.

Lemma 3.2.6. If C_{1}, …, C_{n} is a companion sequence of A, then A is logically valid if and only if (C_{1} ∧ ⋯ ∧ C_{n}) ⇒ A is logically valid.

Proof. Note that (C_{1} ∧ ⋯ ∧ C_{n}) ⇒ A is quasitautologically equivalent to

C_{n} ⇒ (C_{n−1} ⇒ ⋯ ⇒ (C_{1} ⇒ A)).

Our lemma follows by n applications of part 2 of Lemma 3.2.4. □

Theorem 3.2.7 (the Companion Theorem). A is logically valid if and only if there exists a companion sequence C_{1}, …, C_{n} of A such that

(C_{1} ∧ ⋯ ∧ C_{n}) ⇒ A

is a quasitautology.

Proof. The “if” part is immediate from Lemma 3.2.6. For the “only if” part, assume that A is logically valid. By Theorem 2.5.5 let τ be a finite closed unsigned tableau starting with ¬ A. Thus we have a finite sequence of tableaux τ_{0}, τ_{1}, …, τ_{n} where τ_{0} = ¬ A, τ_{n} = τ, and each τ_{i+1} is obtained by applying a tableau rule R_{i} to τ_{i}. If R_{i} is a quantifier rule, let C_{i} be an appropriate companion. Thus C_{1}, …, C_{n} is a companion sequence for A, and we can easily transform τ into a closed tableau τ′ starting with

¬ A ; C_{1} ; ⋮ ; C_{n}

in which only propositional tableau rules are applied. Thus (C_{1} ∧ ⋯ ∧ C_{n}) ⇒ A is a quasitautology. This proves our theorem.

For instance, if R_{i} is the tableau rule

(∗)  ⋮ ; ∀x B ; ⋮ ; | ; B[x/a] ,

where a is an arbitrary parameter, let C_{i} be the companion (∀x B) ⇒ B[x/a], and replace the application of (∗) by

⋮
(∀x B) ⇒ B[x/a]
⋮
∀x B
⋮
/ \
¬ ∀x B B[x/a]

noting that the left-hand path is closed.

Similarly, if R_{i} is the tableau rule

(∗∗)  ⋮ ; ¬ ∀x B ; ⋮ ; | ; ¬ B[x/a]

where a is a new parameter, let C_{i} be the companion B[x/a] ⇒ (∀x B), and replace the application of (∗∗) by

⋮
B[x/a] ⇒ (∀x B)
⋮
¬ ∀x B
⋮
/ \
¬ B[x/a] ∀x B

noting that the right-hand path is closed. □

Example 3.2.8. As an example illustrating Theorem 3.2.7 and its proof, let A be the sentence (∃x (P x ∨ Qx)) ⇒ ((∃x P x) ∨ (∃x Qx)). Let τ be the closed tableau

¬ A
∃x(P x ∨ Qx)
¬ ((∃x P x) ∨ (∃x Qx))
¬ ∃x P x
¬ ∃x Qx
P a ∨ Qa
¬ P a
¬ Qa
/ \
P a Qa

which shows that A is logically valid. Examining the applications of quantifier rules in τ, we obtain the companion sequence C_{1}, C_{2}, C_{3} for A, where C_{1} is (∃x (P x ∨ Qx)) ⇒ (P a ∨ Qa), C_{2} is P a ⇒ ∃x P x, C_{3} is Qa ⇒ ∃x Qx. Clearly (C_{1} ∧ C_{2} ∧ C_{3}) ⇒ A is a quasitautology.

Exercise 3.2.9. Let A be the logically valid sentence ∃x (P x ⇒ ∀y P y). Find a companion sequence C_{1}, …, C_{n} for A such that (C_{1} ∧ ⋯ ∧ C_{n}) ⇒ A is a quasitautology.

Solution. The unsigned tableau

¬ ∃x (P x ⇒ ∀y P y)
¬ (P a ⇒ ∀y P y)
P a
¬ ∀y P y
¬ P b
¬ (P b ⇒ ∀y P y)
P b

is closed and shows that A is logically valid. From this tableau we read off the companion sequence C_{1}, C_{2}, C_{3}, where

\begin{matrix}C_{1} & is & (P a ⇒ ∀y P y) ⇒ ∃x (P x ⇒ ∀y P y), \\ C_{2} & is & P b ⇒ ∀y P y, \\ C_{3} & is & (P b ⇒ ∀y P y) ⇒ ∃x (P x ⇒ ∀y P y). \end{matrix}

A simpler companion sequence for A is C′_{1}, C′_{2} where

\begin{matrix}C′_{1} & is & P a ⇒ ∀y P y, \\ C′_{2} & is & (P a ⇒ ∀y P y) ⇒ ∃x (P x ⇒ ∀y P y). \end{matrix}

Exercise 3.2.10. Let A be the logically valid sentence ∃x (P x ⇔ ∀y P y). Find a companion sequence C_{1}, …, C_{n} for A such that (C_{1} ∧ ⋯ ∧ C_{n}) ⇒ A is a quasitautology.

Solution. To find a companion sequence for A, we first construct a closed unsigned tableau starting with ¬ A.

¬ ∃x (P x ⇔ ∀y P y)
¬ (P a ⇔ ∀y P y)
/ \

\begin{matrix}P a \\ ¬ ∀y P y \\ ¬ P b \\ ¬ (P b ⇔ ∀y P y) \\ /  \ \\ \begin{matrix}P b \\ ¬ ∀y P y \end{matrix} & \begin{matrix}¬ P b \\ ∀y P y \end{matrix} \end{matrix} \begin{matrix}¬ P a \\ ∀y P y \\ P a \end{matrix}

From this tableau, we read off the companion sequence C_{1}, C_{2}, C_{3}, C_{4} where

C_{1} is (P a ⇔ ∀y P y) ⇒ ∃x (P x ⇔ ∀y P y),
C_{2} is P b ⇒ (∀y P y),
C_{3} is (P b ⇔ ∀y P y) ⇒ ∃x (P x ⇔ ∀y P y),
C_{4} is (∀y P y) ⇒ P a.

A simpler companion sequence for A is C′_{1}, C′_{2}, C′_{3} where

\begin{matrix}C′_{1} & is & P a ⇒ ∀y P y, \\ C′_{2} & is & (∀y P y) ⇒ P a, \\ C′_{3} & is & (P a ⇔ ∀y P y) ⇒ ∃x (P x ⇔ ∀y P y). \end{matrix}

3.3 Hilbert-Style Proof Systems

Let L be a language. Recall that V is the set of parameters. Definition 3.3.1 (the system LH ). Our Hilbert-style proof system LH for the predicate calculus is as follows:

1. The objects are L-V -sentences.

2. For each quasitautology A, ⟨A⟩ is a rule of inference.

3. ⟨(∀x B) ⇒ B[x/a]⟩ and ⟨B[x/a] ⇒ (∃x B)⟩ are rules of inference.

4. ⟨A, A ⇒ B, B⟩ is a rule of inference.

5. ⟨A ⇒ B[x/a], A ⇒ (∀x B)⟩ and ⟨B[x/a] ⇒ A, (∃x B) ⇒ A⟩ are rules of in-

ference, provided the parameter a does not occur in A or in B. Schematically, LH consists of:

1. A, where A is any quasitautology

2. (a) (∀x B) ⇒ B[x/a] (universal instantiation)

(b) B[x/a] ⇒ (∃x B) (existential instantiation)

3. \frac{A A ⇒ B}{B} (modus ponens)

4. (a) \frac{A ⇒ B[x/a]}{A ⇒ (∀x B)} (universal generalization)

(b) \frac{B[x/a] ⇒ A}{(∃x B) ⇒ A} (existential generalization), where a does not occur in A, B.

Lemma 3.3.2 (soundness of LH ). LH is sound. In other words, for all L-V - sentences A, if A is derivable, then A is logically valid. Proof. The proof is straightforward by induction on the length of a derivation. The induction step is similar to the proof of Lemma 3.2.4. □ Example 3.3.3. In LH we have the following derivation:

1. (∀x A) ⇒ A[x/a] (by universal instantiation)

2. A[x/a] ⇒ (∃x A) (by existential instantiation)

3. ((∀x A) ⇒ A[x/a]) ⇒ ((A[x/a] ⇒ (∃x A)) ⇒ ((∀x A) ⇒ (∃x A)))

(This is a quasitautology, obtained from the tautology (p ⇒ q) ⇒ ((q ⇒ r) ⇒ (p ⇒ r)).)

4. (A[x/a] ⇒ (∃x A)) ⇒ ((∀x A) ⇒ (∃x A)) (from 1, 3, and modus ponens)

5. (∀x A) ⇒ (∃x A) (from 2, 4, and modus ponens)

Thus, by Lemma 3.3.2, (∀x A) ⇒ (∃x A) is logically valid.

Example 3.3.4. In LH we have the following derivation:

1. B[x/a] ⇒ (∃x B) (by existential instantiation)

2. (B[x/a] ⇒ (∃x B)) ⇒ ((A ∧ B)[x/a] ⇒ (∃x B)) (a quasitautology)

3. (A ∧ B)[x/a] ⇒ (∃x B) (from 1, 2, and modus ponens)

4. (∃x (A ∧ B)) ⇒ (∃x B) (from 3 and existential generalization)

Thus, by Lemma 3.3.2, (∃x (A ∧ B)) ⇒ (∃x B) is logically valid.

We now turn to the proof that LH is complete.

Lemma 3.3.5. LH is closed under quasitautological consequence. In other words, if A_{1}, …, A_{k} are derivable, and if B is a quasitautological consequence of A_{1}, …, A_{k}, then B is derivable.

Proof. We are assuming that B is a quasitautological consequence of A_{1}, …, A_{k}. Thus A_{1} ⇒ (A_{2} ⇒ ⋯ ⇒ (A_{k} ⇒ B)) is a quasitautology, hence derivable. We are also assuming that A_{1}, …, A_{k} are derivable. Thus we obtain B by k applications of modus ponens. □

Lemma 3.3.6. If C is a companion of A, and if C ⇒ A is derivable in LH , then A is derivable in LH .

Proof. First, suppose C is of the form 3.2.3(1), namely (∀x B) ⇒ B[x/a]. By universal instantiation, C is derivable. In addition, we are assuming that C ⇒ A is derivable. Hence, by modus ponens, A is derivable.

Next, suppose C is of the form 3.2.3(2), namely B[x/a] ⇒ (∀x B), where a does not occur in A, B. We are assuming that C ⇒ A is derivable, i.e., (B[x/a] ⇒ (∀x B)) ⇒ A is derivable. It follows by Lemma 3.3.5 that both (i) (¬ A) ⇒ B[x/a] and (ii) (¬ A) ⇒ (¬ ∀x B) are derivable. Applying universal generalization to (i), we see that (¬ A) ⇒ (∀x B) is derivable. From this plus (ii), it follows by Lemma 3.3.5 that A is derivable.

The other cases, where C is of the form 3.2.3(3) or 3.2.3(4), are handled similarly. □

Theorem 3.3.7 (completeness of LH ). LH is sound and complete. In other words, for all L-V -sentences A, A is derivable if and only if A is logically valid.

Proof. The “only if” part is Lemma 3.3.2. For the “if” part, assume that A is logically valid. By Theorem 3.2.7, there exists a companion sequence C_{1}, …, C_{n} for A such that (C_{1} ∧ ⋯ ∧ C_{n}) ⇒ A is a quasitautology. Hence C_{n} ⇒ (C_{n−1} ⇒ ⋯ ⇒ (C_{1} ⇒ A)) is a quasitautology, hence derivable. From this and n applications of Lemma 3.3.6, we obtain derivability of A. □

Remark 3.3.8. For convenience in writing proofs, we supplement the rules of LH with

\frac{A_{1} ⋯ A_{k}}{B}

whenever B is a quasitautological consequence of A_{1}, …, A_{k}. This is justified by Lemma 3.3.5. We indicate applications of this rule by QT, for quasitautology. Similarly we use UI, EI, UG, EG to indicate universal instantiation, existential instantiation, universal generalization, existential generalization, respectively.

Exercise 3.3.9. Construct a Hilbert-style proof of the sentence

(∃x ∀y Rxy) ⇒ (∀y ∃x Rxy).

Solution. A proof in LH is

1. (∀y Ray) ⇒ Rab  UI
2. Rab ⇒ (∃x Rxb)  EI
3. (∀y Ray) ⇒ (∃x Rxb)  1,2,QT
4. (∀y Ray) ⇒ (∀y ∃x Rxy)  3,UG
5. (∃x ∀y Rxy) ⇒ (∀y ∃x Rxy)  4,EG

Exercise 3.3.10. Construct a Hilbert-style proof of the sentence

(∀x (P x ∧ Qx)) ⇔ ((∀x P x) ∧ (∀x Qx))

Solution. A proof in LH is

1. (∀x (P x ∧ Qx)) ⇒ (P a ∧ Qa)  UI
2. (∀x (P x ∧ Qx)) ⇒ P a  1,QT
3. (∀x (P x ∧ Qx)) ⇒ ∀x P x  2,UG
4. (∀x (P x ∧ Qx)) ⇒ Qa  1,QT
5. (∀x (P x ∧ Qx)) ⇒ ∀x Qx  4,UG
6. (∀x P x) ⇒ P a  UI
7. (∀x Qx) ⇒ Qa  UI
8. ((∀x P x) ∧ (∀x Qx)) ⇒ (P a ∧ Qa)  6,7,QT
9. ((∀x P x) ∧ (∀x Qx)) ⇒ ∀x (P x ∧ Qx)  8,UG
10. (∀x (P x ∧ Qx)) ⇔ ((∀x P x) ∧ (∀x Qx)) 3,5,9,QT

Exercise 3.3.11. Construct a Hilbert-style proof of ¬ ∃x ∀y (Eyx ⇔ ¬ Eyy).

Solution. A proof in LH is

1. ∀y (Eya ⇔ ¬ Eyy) ⇒ (Eaa ⇔ ¬ Eaa)  UI
2. ¬ ∀y (Eya ⇔ ¬ Eyy)  1,QT
3. (∀y (Eya ⇔ ¬ Eyy)) ⇒ ¬ ∃x ∀y (Eyx ⇔ ¬ Eyy)  2,QT
4. (∃x ∀y (Eyx ⇔ ¬ Eyy)) ⇒ ¬ ∃x ∀y (Eyx ⇔ ¬ Eyy) 3,EG
5. ¬ ∃x ∀y (Eyx ⇔ ¬ Eyy)  4,QT

Exercise 3.3.12. Construct a Hilbert-style proof of the sentence

¬ ∃x (Sx ∧ ∀y (Eyx ⇔ (Sy ∧ ¬ Eyy))).

Solution. A proof in LH is

1. (∀y (Eya ⇔ (Sy ∧ ¬ Eyy))) ⇒ (Eaa ⇔ (Sa ∧ ¬ Eaa))  UI
2. (Sa ∧ (∀y (Eya ⇔ (Sy ∧ ¬ Eyy)))) ⇒ (Sb ∧ ¬ Sb)  1,QT
3. (∃x (Sx ∧ (∀y (Eyx ⇔ (Sy ∧ ¬ Eyy))))) ⇒ (Sb ∧ ¬ Sb) 2,EG
4. ¬ ∃x (Sx ∧ (∀y (Eyx ⇔ (Sy ∧ ¬ Eyy))))  3,QT

Exercise 3.3.13. Construct a Hilbert-style proof of ∃x (P x ⇒ ∀y P y). Solution. A proof in LH is

1. (P a ⇒ ∀y P y) ⇒ ∃x (P x ⇒ ∀y P y)  EI
2. (¬ ∃x (P x ⇒ ∀y P y)) ⇒ P a  1,QT
3. (¬ ∃x (P x ⇒ ∀y P y)) ⇒ ∀y P y  2,UG
4. ∃x (P x ⇒ ∀y P y)  1,3,QT

Exercise 3.3.14. Construct a Hilbert-style proof of ∃x (P x ⇔ ∀y P y). Solution. A proof in LH is

1. (P a ⇔ ∀y P y) ⇒ ∃x (P x ⇔ ∀y P y)  EI
2. (∀yP y) ⇒ P a  UI
3. (¬ ∃x (P x ⇔ ∀y P y)) ⇒ P a  1,2,QT
4. (¬ ∃x (P x ⇔ ∀y P y)) ⇒ ∀y P y  3,UG
5. ∃x (P x ⇔ ∀y P y)  1,2,4,QT

Exercise 3.3.15. Consider the following proof system LH′, which is a “stripped down” version of LH . The objects of LH′ are L-V -sentences containing only ∀, ⇒, ¬ (i.e., not containing ∃, ⇔, ∧, ∨). The rules of LH′ are:

(a) quasitautologies

(b) (∀x B) ⇒ B[x/a]

(c) (∀x (A ⇒ B)) ⇒ (A ⇒ ∀x B)

(d) \frac{A A ⇒ B}{B} (modus ponens)

(e) \frac{B[x/a]}{∀x B} (generalization), where a does not occur in B.

Show that LH′ is sound and complete.

Solution. Soundness is proved just as for LH .

Just as for the full tableau method, we can prove soundness and completeness of the restricted tableau method with ∀, ⇒, ¬, and from this we obtain the restricted Companion Theorem. There are now only two kinds of companions, the ones involving ∀. It remains to prove the following lemma: If C is a companion of A, and if C ⇒ A is derivable in LH′, then A is derivable in LH′.

Consider a companion of the form B[x/a] ⇒ (∀x B). Assume that

(B[x/a] ⇒ (∀x B)) ⇒ A

is derivable in LH′, where a does not occur in A, B. It follows quasitautologically that both (1) (¬ A) ⇒ B[x/a] and (2) (¬ A) ⇒ ¬ ∀x B are derivable in LH′. From (1) and the generalization rule (e) of LH′, we see that ∀x ((¬ A) ⇒ B) is derivable in LH′. Also, by rule (c) of LH′,

(∀x ((¬ A) ⇒ B)) ⇒ ((¬ A) ⇒ ∀x B)

is derivable in LH′. Hence, by modus ponens, (¬ A) ⇒ ∀x B is derivable in LH′. It follows quasitautologically from this and (2) that A is derivable in LH′. This completes the proof.

Exercise 3.3.16.

1. Let S be a set of L-sentences. Consider a proof system LH (S) consisting of LH with additional rules of inference ⟨A⟩, A ∈ S. Show that an L-V - sentence B is derivable in LH (S) if and only if B is a logical consequence of S.

2. Indicate the modifications needed when S is a set of L-V -sentences.

Solution.

1. By induction on the length of derivations, it is straightforward to prove that each sentence derivable in LH (S) is a logical consequence of S. The assumption that S is a set of L-sentences (not L-V -sentences) is used in the inductive steps corresponding to rules 4(a) and 4(b), universal and existential generalization, because we need to know that the parameter a does not occur in S. Conversely, assume B is a logical consequence of S. By the Compactness Theorem, it follows that B is a logical consequence of a finite subset of S, say A_{1}, …, A_{n}. Hence (A_{1} ∧ ⋯ ∧ A_{n}) ⇒ B is logically valid. Hence, by completeness of LH , (A_{1} ∧ ⋯ ∧ A_{n}) ⇒ B is derivable in LH . Since LH (S) includes LH , we have that

(A_{1} ∧ ⋯ ∧ A_{n}) ⇒ B

is derivable in LH (S). But A_{1}, …, A_{n} are derivable in LH (S). It follows quasitautologically that B is derivable in LH (S). This completes the proof.

2. If S is a set of L-V -sentences, we modify our system as follows. Let V′ be a countably infinite set of new parameters, disjoint from V. Define LH (S) as before, but allowing parameters from V ∪ V′. The objects are L-V ∪V′-sentences. In rules 4(a) and 4(b), one must impose the restriction that a does not occur in A, B, S. With this modification, everything goes through as before.

Notation 3.3.17. We write S ⊢ B to indicate that B is derivable in LH (S).

Exercise 3.3.18. Let S be an infinite set of L-sentences, and let B be an Lsentence. Prove that S ⊧ B (i.e., B is true in all L-structures satisfying S) if and only if there exists a finite set of L-sentences A_{1}, …, A_{k} ∈ S such that A_{1}, …, A_{k} ⊢ B (i.e., B is provable from A_{1}, …, A_{k}).

Solution. The “if” part follows from the soundness of our proof system. For the “only if” part, assume that S ⊧ B, i.e., S ∪ {¬ B} is not satisfiable. It follows by the Compactness Theorem that there exists a finite set {A_{1}, …, A_{k}} ⊂ S such that A_{1}, …, A_{k}, ¬ B is not satisfiable. Thus B is a logical consequence of A_{1}, …, A_{k}. It follows by completeness of our proof system that A_{1}, …, A_{k} ⊢ B.

3.4 Gentzen-Style Proof Systems

Throughout this section, let L be a language. As usual, V is the set of parameters.

Before presenting our Gentzen-style proof system for L, we first discuss the block tableau method, a trivial variant of the signed tableau method.

Definition 3.4.1. A block is a finite set of signed L-V -sentences. A block is said to be closed if it contains T A and F A for some L-V -sentence A.

Notation 3.4.2. If S is a block and X is a signed L-V -sentence, we write S, X instead of S ∪ {X}, etc.

Definition 3.4.3. A block tableau is a rooted dyadic tree where each node carries a block. A block tableau is said to be closed if each of its end nodes is closed. Given a block S, a block tableau starting with S is a block tableau generated from S by means of block tableau rules. The block tableau rules are obtained from the signed tableau rules (pages 13 and 31) as follows. Corresponding to signed tableau rules of the form

⋮ ; X ; ⋮ ; | ; Y  ⋮ ; X ; ⋮ ; | ; Y_{1} ; Y_{2}  ⋮ ; X ; ⋮ ; / \ ; Y Z  ⋮ ; X ; ⋮ ; / \ ; Y_{1} Z_{1} ; Y_{2} Z_{2}

we have block tableau rules

\begin{matrix}S, X \\ | \\ S, X, Y \end{matrix}  \begin{matrix}S, X \\ | \\ S, X, Y_{1}, Y_{2} \end{matrix}  \begin{matrix}S, X \\ / \ \\ S, X, Y S, X, Z \end{matrix}  \begin{matrix}S, X \\ / \ \\ S, X, Y_{1}, Y_{2} S, X, Z_{1}, Z_{2} \end{matrix}

respectively.

For example, we have the following block tableau rules:

\begin{matrix}S, T A ∧ B \\ | \\ S, T A ∧ B, T A, T B \end{matrix}  \begin{matrix}S, F A ∧ B \\ / \ \\ S, F A ∧ B, F A S, F A ∧ B, F B \end{matrix}

\begin{matrix}S, T A ⇒ B \\ / \ \\ S, T A ⇒ B, FA S, T A ⇒ B, TB \end{matrix}  \begin{matrix}S, F A ⇒ B \\ | \\ S, F A ⇒ B, T A, F B \end{matrix}

\begin{matrix}S, T ∀x A \\ | \\ S, T ∀x A, T A[x/a] \end{matrix} S, F ∀x A

|

S, F ∀x A, F A[x/a] where a is new.

Example 3.4.4. We exhibit a closed block tableau demonstrating that ∃x A is a logical consequence of ∀x A.

T ∀x A, F ∃x A
|
T ∀x A, F ∃x A, T A[x/a]
|
T ∀x A, F ∃x A, T A[x/a], F A[x/a]

This block tableau is of course similar to the signed tableau

\begin{matrix}T ∀x A \\ F ∃x A \\ T A[x/a] \\ F A[x/a] \end{matrix}

which demonstrates the same thing.

We now define our Gentzen-style system, LG. Definition 3.4.5. A sequent is an expression of the form Γ → Δ where Γ and Δ are finite sets of L-V -sentences. If S = T A_{1}, …, T A_{m}, F B_{1}, …, F B_{n} is a block, let |S| be the sequent A_{1}, …, A_{m} → B_{1}, …, B_{n}. This gives a one-to-one correspondence between blocks and sequents. Definition 3.4.6 (the system LG). Our Gentzen-style proof system LG for the predicate calculus is as follows.

1. The objects of LG are sequents.^{2}

2. For each closed block S, we have a rule of inference ⟨|S|⟩. In other words, for all finite sets of L-V -sentences Γ and Δ and all L-V -sentences A, we assume the sequent Γ, A → A, Δ.

3. For each non-branching block tableau rule

\begin{matrix}S \\ | \\ S′ \end{matrix}

we have a rule of inference ⟨|S′|, |S|⟩, i.e., \frac{|S′|}{|S|}.

4. For each branching block tableau rule

\begin{matrix}S \\ / \ \\ S′ S′′ \end{matrix}

we have a rule of inference ⟨|S′|, |S′′|, |S|⟩, i.e., \frac{|S′| |S′′|}{|S|}.

Thus LG includes the following rules of inference:

2For this reason, LG is sometimes called a sequent calculus.

\overline{Γ, A → A, Δ}

\frac{Γ, ¬ A → A, Δ}{Γ, ¬ A → Δ}  \frac{Γ, A → ¬ A, Δ}{Γ → ¬ A, Δ}

\frac{Γ, A ∧ B, A, B → Δ}{Γ, A ∧ B → Δ}  \frac{Γ → A ∧ B, A, Δ Γ → A ∧ B, B, Δ}{Γ → A ∧ B, Δ}

\frac{Γ, A ⇒ B → A, Δ Γ, A ⇒ B, B → Δ}{Γ, A ⇒ B → Δ}  \frac{Γ, A → A ⇒ B, B, Δ}{Γ → A ⇒ B, Δ}

\frac{Γ, ∀x A, A[x/a] → Δ}{Γ, ∀x A → Δ}  \frac{Γ → ∀x A, A[x/a], Δ}{Γ → ∀x A, Δ}

where a does not occur in the conclusion.

Exercise 3.4.7. Explicitly display the remaining inference rules of LG.

Definition 3.4.8. A sequent A_{1}, …, A_{m} → B_{1}, …, B_{n} is said to be logically valid if and only if the L-V -sentence

(A_{1} ∧ ⋯ ∧ A_{m}) ⇒ (B_{1} ∨ ⋯ ∨ B_{n})

is logically valid.^{3}

Theorem 3.4.9 (soundness and completeness of LG). LG is sound and complete. In other words, a sequent Γ → Δ is logically valid if and only if it is derivable in LG. In particular, an L-V -sentence A is logically valid if and only if the sequent

→ A

is derivable in LG.

Proof. Note that the sequent A_{1}, …, A_{m} → B_{1}, …, B_{n} is logically valid if and only if the block T A_{1}, …, T A_{m}, F B_{1}, …, F B_{n} is not satisfiable. Thus, soundness and completeness of LG is equivalent to soundness and completeness of the block tableau method. The latter is in turn easily seen to be equivalent to soundness and completeness of the signed tableau method, as presented in Theorems 2.3.13 and 2.5.5. □

3In particular, the sequents A_{1}, …, A_{m} → and → B_{1}, …, B_{n} are said to be logically valid if and only if the L-V -sentences ¬ (A_{1} ∧ ⋯ ∧ A_{m}) and B_{1} ∨ ⋯ ∨ B_{n} are logically valid, respectively. The empty sequent → is deemed not logically valid.

Exercise 3.4.10. Construct a Gentzen-style proof of the sequent

∃x ∀y Rxy → ∀y ∃x Rxy.

Solution. A proof in LG is

\begin{matrix}1. & ∃x ∀y Rxy, ∀y Ray, Rab → Rab, ∃x Rxb, ∀y ∃x Rxy \\ 2. & ∃x ∀y Rxy, ∀y Ray, Rab → ∃x Rxb, ∀y ∃x Rxy \\ 3. & ∃x ∀y Rxy, ∀y Ray → ∃x Rxb, ∀y ∃x Rxy \\ 4. & ∃x ∀y Rxy → ∃x Rxb, ∀y ∃x Rxy \\ 5. & ∃x ∀y Rxy → ∀y ∃x Rxy \end{matrix}

Definition 3.4.11. In order to simplify the writing of Gentzen-style proofs, let LG^{+} be LG augmented with the so-called weakening rules or padding rules:

\frac{Γ → Δ}{Γ, A → Δ}  \frac{Γ → Δ}{Γ → A, Δ}

where A is an L-V -sentence. Clearly LG^{+} is sound and complete.

Remark 3.4.12. Any proof in LG is a proof in LG^{+}, and any proof in LG^{+} may be straightforwardly “padded out” to a proof in LG. Thus LG^{+} differs only slightly from LG. However, proofs in LG^{+} are easier. For example, patterned on the above proof in LG, we have the following proof in LG^{+}:

\begin{matrix}1. & Rab → Rab \\ 1.5. & ∀y Ray, Rab → Rab \\ 2. & ∀y Ray → Rab \\ 2.5. & ∀y Ray → Rab, ∃x Rxb \\ 3. & ∀y Ray → ∃x Rxb \\ 3.5. & ∃x ∀y Rxy, ∀y Ray → ∃x Rxb \\ 4. & ∃x ∀y Rxy → ∃x Rxb \\ 4.5. & ∃x ∀y Rxy → ∃x Rxb, ∀y ∃x Rxy \\ 5. & ∃x ∀y Rxy → ∀y ∃x Rxy \end{matrix}

or, omitting the applications of the padding rules,

\begin{matrix}1. & Rab → Rab \\ 2. & ∀y Ray → Rab \\ 3. & ∀y Ray → ∃x Rxb \\ 4. & ∃x ∀y Rxy → ∃x Rxb \\ 5. & ∃x ∀y Rxy → ∀y ∃x Rxy \end{matrix}

Exercise 3.4.13. Construct a Gentzen-style proof of the sequent

→ (∃x ∀y Rxy) ⇒ (∀y ∃x Rxy).

Solution. A proof in LG^{+} consists of the previous proof followed by

\begin{matrix}5.5. & ∃x ∀y Rxy → ∀y ∃x Rxy, (∃x ∀y Rxy) ⇒ (∀y ∃x Rxy) \\ 6. & → (∃x ∀y Rxy) ⇒ (∀y ∃x Rxy) \end{matrix}

Exercise 3.4.14. Construct a Gentzen-style proof of the sequent

→ ¬ ∃x (Sx ∧ ∀y (Eyx ⇔ (Sy ∧ ¬ Eyy))).

Solution. A proof in LG^{+} with padding rules omitted is

1. Eaa → Eaa  axiom
2. Eaa, ¬ Eaa →  from 1
3. Eaa, Sa ∧ ¬ Eaa →  from 2
4. Sa → Sa  axiom
5. → Eaa, ¬ Eaa  from 1
6. Sa → Eaa, Sa ∧ ¬ Eaa  from 4 and 5
7. Sa, Eaa ⇔ (Sa ∧ ¬ Eaa) →  from 4 and 6
8. Sa, ∀y (Eya ⇔ (Sy ∧ ¬ Eyy)) →  from 7
9. Sa ∧ ∀y (Eya ⇔ (Sy ∧ ¬ Eyy)) →  from 8
10. ∃x (Sx ∧ ∀y (Eyx ⇔ (Sy ∧ ¬ Eyy)) →  from 9
11. → ¬ ∃x (Sx ∧ ∀y (Eyx ⇔ (Sy ∧ ¬ Eyy))  from 10

Exercise 3.4.15. Construct a Gentzen-style proof of ∃x (P x ⇒ ∀y P y). Solution. A proof in LG^{+} with padding rules omitted is

1. P a → P a  axiom
2. → P a, P a ⇒ ∀y P y  from 1
3. → P a, ∃x (P x ⇒ ∀y P y)  from 2
4. → ∀y P y, ∃x (P x ⇒ ∀y P y)  from 3
5. → P a ⇒ ∀y P y, ∃x (P x ⇒ ∀y P y) from 4
6. → ∃x (P x ⇒ ∀y P y)  from 5

Exercise 3.4.16. Construct a Gentzen-style proof of ∃x (P x ⇔ ∀y P y). Solution. A proof in LG^{+} with padding rules omitted is

1. P a → P a, ∀y P y  axiom
2. ∀y P y → P a, ∀y P y  axiom
3. → P a ⇔ ∀y P y, P a, ∀y P y  from 1 and 2 via → ⇔
4. → P a ⇔ ∀y P y, ∀y P y  from 3 via →∀
5. P b → P b  axiom
6. ∀y P y → P b  from 5 via ∀→
7. → P a ⇔ ∀y P y, P b ⇔ ∀y P y  from 4 and 6 via → ⇔
8. → P a ⇔ ∀y P y, ∃x (P x ⇔ ∀y P y) from 7 via →∃
9. → ∃x (P x ⇔ ∀y P y)  from 8 via →∃

The above proof was derived from the tableau in Exercise 3.2.10. Exercise 3.4.17. Let LG(atomic) be a variant of LG in which Γ, A → A, Δ is assumed only for atomic L-V -sentences A. Show that LG(atomic) is sound and complete. (Hint: Use the result of Exercise 2.5.7.)

Exercise 3.4.18.

1. The modified block tableau rules are a variant of the block tableau rules of Definition 3.4.3, replacing each non-branching rule of the form

\begin{matrix}S, X \\ | \\ S, X, Y_{1}, Y_{2} \end{matrix}

by a pair of rules

\begin{matrix}S, X \\ | \\ S, X, Y_{1} \end{matrix}  \begin{matrix}S, X \\ | \\ S, X, Y_{2} \end{matrix}

Show that the modified block tableau rules are sound and complete.

2. Let LG′ be the variant of LG corresponding to the modified block tableau rules. Write out all the rules of LG′ explicitly. Show that LG′ is sound and complete.

3.5 The Interpolation Theorem

As usual, let L be a language and let V be the set of parameters.

Theorem 3.5.1 (the Interpolation Theorem). Let A and B be L-V -sentences. If A ⇒ B is logically valid, we can find an L-V -sentence I such that:

1. A ⇒ I and I ⇒ B are logically valid.

2. Each predicate and parameter occurring in I occurs in both A and B.

Such an I is called an interpolant for A ⇒ B. We indicate this by writing

A ⇒^{I} B.

Remark 3.5.2. If A and B have no predicates in common, then obviously the theorem is incorrect as stated, because all L-V -sentences necessarily contain at least one predicate. In this case, we modify the conclusion of the theorem to say that at least one of ¬ A and B is logically valid.^{4} The conclusion is obvious in this case.

In order to prove the Interpolation Theorem, we introduce a “symmetric” variant of LG, wherein sentences do not move from one side of → to the other.

Definition 3.5.3. A signed sequent is an expression of the form M → N where M and N are finite sets of signed L-V -sentences. A variant of M → N is a signed sequent obtained from M → N by transferring sentences from one side of → to the other, changing signs. In particular, M, X → N and M → \overline{X}, N are variants of each other, where we use an overline to denote conjugation, i.e., \overline{T A} = F A, \overline{F A} = T A.

4This amounts to saying that at least one of the truth values T and F is an interpolant for A ⇒ B.

Definition 3.5.4. Let

C_{1}, …, C_{m} → D_{1}, …, D_{n}

be an unsigned sequent^{5}. A signed variant of C_{1}, …, C_{m} → D_{1}, …, D_{n} is any variant of the signed sequent

T C_{1}, …, T C_{m} → T D_{1}, …, T D_{n} .

Note that each signed sequent is a signed variant of one and only one unsigned sequent. We define a signed sequent to be logically valid if and only if the corresponding unsigned sequent is logically valid. Definition 3.5.5. LG(symmetric) is the following proof system.

1. The objects are signed sequents.

2. We have

\overline{M, X → X, N}

and

\overline{M, X, \overline{X} → N}

and

\overline{M → X, \overline{X}, N}

for all X.

3. For each signed tableau rule of the form

⋮ ; X ; ⋮ ; | ; Y  ⋮ ; X ; ⋮ ; | ; Y_{1} ; Y_{2}  ⋮ ; X ; ⋮ ; / \ ; Y Z  ⋮ ; X ; ⋮ ; / \ ; Y_{1} Z_{1} ; Y_{2} Z_{2}

we have a corresponding pair of signed sequent rules

5An unsigned sequent is just what we have previously called a sequent.

\begin{matrix}\frac{M, X, Y → N}{M, X → N} & \frac{M → \overline{X}, \overline{Y} , N}{M → \overline{X}, N} \\ \frac{M, X, Y_{1}, Y_{2} → N}{M, X → N} & \frac{M → \overline{X}, \overline{Y_{1}}, \overline{Y_{2}}, N}{M → \overline{X}, N} \\ \frac{M, X, Y → N M, X, Z → N}{M, X → N} & \frac{M → \overline{X}, \overline{Y} , N M → \overline{X}, \overline{Z}, N}{M → \overline{X}, N} \\ \frac{M, X, Y_{1}, Y_{2} → N M, X, Z_{1}, Z_{2} → N}{M, X → N} & \frac{M → \overline{X}, \overline{Y_{1}}, \overline{Y_{2}}, N M → \overline{X}, \overline{Z_{1}}, \overline{Z_{2}}, N}{M → \overline{X}, N} \end{matrix}

respectively.

Lemma 3.5.6. An unsigned sequent is derivable in LG if and only if all of its signed variants are derivable in LG(symmetric).

Proof. The proof is by induction on the length of derivations in LG. The base step consists of noting that all signed variants of Γ, A → A, Δ are of the form M, X → X, N or M, X, \overline{X} → N or M → X, \overline{X}, N, hence derivable in LG(symmetric). The inductive step consists of checking that, for each rule of inference of LG, if all signed variants of the premises are derivable in LG(symmetric), then so are all signed variants of the conclusion. This is straightforward. □

Theorem 3.5.7. LG(symmetric) is sound and complete. In other words, a signed sequent is logically valid if and only if it is derivable in LG(symmetric). In particular, an L-V -sentence A ⇒ B is logically valid if and only if the signed sequent T A → T B is derivable in LG(symmetric).

Proof. Soundness and completeness of LG(symmetric) follows from Theorem 3.4.9, soundness and completeness of LG, using Lemma 3.5.6. □

We now prove the Interpolation Theorem.

Definition 3.5.8. Let M → N be a signed sequent. An interpolant for M → N is an L-V -sentence I such that the signed sequents M → T I and T I → N are logically valid, and all predicates and parameters occurring in I occur in both M and N.^{6} We indicate this by writing M →^{I} N.

In order to prove the Interpolation Theorem, it suffices by Theorem 3.5.7 to prove that every signed sequent derivable in LG(symmetric) has an interpolant. We prove this by induction on the length of derivations.

6In the special case when M and N have no predicates in common, we require instead that at least one of the signed sequents M → and → N be logically valid. This amounts to requiring that at least one of T, F be an interpolant for M → N.

For the base step, we note that X is an interpolant for M, X → X, N, and that M, X, \overline{X} → and → X, \overline{X}, N are logically valid. Thus we have M, X →^{X} X, N

and M, X, \overline{X} →^{F} N and M →^{T} X, \overline{X}, N.

For the induction step we show that, for each rule of LG(symmetric), given interpolants for the premises of the rule, we can find an interpolant for the conclusion. We present some representative special cases.

\frac{M, T A ∧ B, T A, T B →^{I} N}{M, T A ∧ B →^{I} N}  \frac{M →^{I} F A ∧ B, F A, FB, N}{M →^{I} F A ∧ B, N}

\frac{M, F A ∧ B, F A →^{I} N M, F A ∧ B, F B →^{J} N}{M, F A ∧ B ⟶^{I ∨ J} N}

\frac{M →^{I} T A ∧ B, T A, N M →^{J} T A ∧ B, T B, N}{M ⟶^{I ∧ J} T A ∧ B, N}

\frac{M, T ¬ A, F A →^{I} N}{M, T ¬ A →^{I} N}  \frac{M →^{I} F ¬ A, T A, N}{M →^{I} F ¬ A, N}

\frac{M, F ¬ A, T A →^{I} N}{M, F ¬ A →^{I} N}  \frac{M →^{I} T ¬ A, F A, N}{M →^{I} T ¬ A, N}

\frac{M, F ∀x A, F A[x/a] →^{I} N}{M, F ∀x A →^{I} N}

where a does not occur in the conclusion.

\frac{M →^{I} T ∀x A, T A[x/a], N}{M →^{I} T ∀x A, N}

where a does not occur in the conclusion.

\frac{M, T ∀x A, T A[x/a] →^{I} N}{M, T ∀x A →^{K} N}

where K = I if a occurs in M, T ∀x A, otherwise K = ∀z I[a/z] where z is a new variable.

\frac{M →^{I} F ∀x A, F A[x/a], N}{M →^{K} F ∀x A, N}

where K = I if a occurs in F ∀x A, N, otherwise K = ∃z I[a/z] where z is a new variable.

This completes the proof.

Example 3.5.9. We give an example illustrating the Interpolation Theorem. Let n be a large positive integer, say n = 1000. Let A_{n} say that the universe consists of the vertices of a simple, undirected graph with a clique of size n. Let B_{n} say that the graph is not (n − 1)-colorable. Both A_{n} and B_{n} contain a predicate R denoting adjacency in the graph. A_{n} contains a unary predicate Q denoting a clique. B_{n} contains a binary predicate E saying that two vertices get the same color.

A_{n} is:

R and G are irreflexive relations on the universe, R is symmetric, G is transitive, ∀x ∀y ((Qx ∧ Qy ∧ Gxy) ⇒ Rxy), and there exist x_{1}, …, x_{n} such that Qx_{1} ∧ ⋯ ∧ Qx_{n} ∧ Gx_{1}x_{2} ∧ ⋯ ∧ Gx_{n−1}x_{n}.

B_{n} is the negation of:

E is an equivalence relation on the universe, ∀x ∀y (Rxy ⇒ ¬ Exy), and there exist x_{1}, …, x_{n−1} such that ∀y (Ex_{1}y ∨ ⋯ ∨ Ex_{n−1}y).

Clearly A_{n} ⇒ B_{n} is logically valid. Note that the lengths of A_{n} and B_{n} are O(n), i.e., proportional to n. The obvious interpolant I_{n} says there exists a clique of size n, i.e., there exist x_{1}, …, x_{n} such that Rx_{1}x_{2} ∧ Rx_{1}x_{3} ∧ ⋯ ∧ Rx_{n−1}x_{n}. Note that the length of I_{n} is O(n^{2}), i.e., proportional to n^{2}. It appears that there is no interpolant of length O(n).

Extensions of Predicate Calculus

In this chapter we consider various extensions of the predicate calculus. These extensions may be regarded as inessential features or “bells and whistles” which are introduced solely in order to make the predicate calculus more user-friendly.

4.1 Predicate Calculus with Identity

Definition 4.1.1. A language with identity consists of a language L with a particular binary predicate, I, designated as the identity predicate. Definition 4.1.2. Let L be a language with identity. The identity axioms for L are the following sentences:

1. ∀x Ixx (reflexivity)

2. ∀x ∀y (Ixy ⇔ Iyx) (symmetry)

3. ∀x ∀y ∀z ((Ixy ∧ Iyz) ⇒ Ixz) (transitivity)

4. For each n-ary predicate P of L, we have an axiom ∀x_{1} ⋯ ∀x_{n} ∀y_{1} ⋯ ∀y_{n} ((Ix_{1}y_{1} ∧ ⋯ ∧ Ix_{n}y_{n}) ⇒ (P x_{1} ⋯ x_{n} ⇔ P y_{1} ⋯ y_{n})) (congruence).

Exercise 4.1.3. Show that the identity predicate is unique in the following sense. If L contains two identity predicates I_{1} and I_{2}, then ∀x ∀y (I_{1}xy ⇔ I_{2}xy) is a logical consequence of the identity axioms for I_{1} and I_{2}.

Let L be a language with identity. Definition 4.1.4. An L-structure M is said to be normal if the identity predicate denotes the identity relation, i.e., I_{M} = {⟨a, a⟩ | a ∈ U_{M}}.

Note that any normal L-structure automatically satisfies the identity axioms for L. Conversely, we have:

Theorem 4.1.5. Let M be an L-structure satisfying the identity axioms for L. For each a ∈ U_{M} put \overline{a} = \{b ∈ U_{M} | v_{M}(Iab) = T\}. Then we have a normal L-structure \overline{M} and an onto mapping ϕ : U_{M} → U\overline{M} as in Theorem 2.7.3, defined by putting U\overline{M} = \{\overline{a} | a ∈ U_{M}\}, and P\overline{M} = \{⟨\overline{a}_{1}, …, \overline{a}_{n}⟩ | ⟨a_{1}, …, a_{n}⟩ ∈ P_{M}\} for all n-ary predicates P.

Proof. This is straightforward, using the fact that I_{M} is a congruence with respect to each of the relations P_{M}, P ∈ L. □

Theorem 4.1.6. If M is an L-structure satisfying the identity axioms for L, then we have a normal L-structure \overline{M} satisfying the same sentences as M.

Proof. This is immediate from Theorems 4.1.5 and 2.7.3. □

Let S be a set of L-sentences.

Definition 4.1.7. S is normally satisfiable if there exists a normal L-structure which satisfies S.

Corollary 4.1.8. S is normally satisfiable if and only if

S ∪ {identity axioms for L}

is satisfiable.

We also have the Compactness Theorem for normal satisfiability:

Corollary 4.1.9. S is normally satisfiable if and only if each finite subset of S is normally satisfiable.

Proof. This is immediate from Corollary 4.1.8 plus the Compactness Theorem for predicate calculus without identity (Theorems 2.6.1 and 2.6.2), applied to the set S ∪ {identity axioms for L}. □

Regarding normal satisfiability in particular domains, we have:

Example 4.1.10. Given a positive integer n, we exhibit a sentence E_{n} which is normally satisfiable in domains of cardinality n but not in domains of any other cardinality. The sentence

∃x_{1} ⋯ ∃x_{n} (∀y (Ix_{1}y ∨ ⋯ ∨ Ix_{n}y) ∧ ¬ (Ix_{1}x_{2} ∨ Ix_{1}x_{3} ∨ ⋯ ∨ Ix_{n−1}x_{n}))

has this property. Intuitively, E_{n} says that there exist exactly n things.

Exercise 4.1.11. Let M = (U_{M}, f_{M}, g_{M}, I_{M}) where U_{M} = {0, 1, 2, 3, 4}, I_{M} is the identity relation on U_{M}, and f_{M}, g_{M} are the binary operations of addition and multiplication modulo 5. Thus M is essentially just the ring of integers modulo 5. Let L be the language consisting of f, g, I. Note that M is a normal L-structure.

Write an L-sentence A such that for all normal L-structures M′, M′ satisfies A if and only if M′ is isomorphic to M.

Solution. A brute force solution is to let A be ∃x_{0} ∃x_{1} ∃x_{2} ∃x_{3} ∃x_{4} B, where B is the conjunction of {∀y (Ix_{0}y ∨ Ix_{1}y ∨ Ix_{2}y ∨ Ix_{3}y ∨ Ix_{4}y)} ∪ {¬ Ix_{i}x_{j} : i ≠ j} ∪ {Ifx_{i}x_{j}x_{k} | i + j = k mod 5} ∪ {Igx_{i}x_{j}x_{k} | ij = k mod 5} with i, j, k ranging over 0, 1, 2, 3, 4.

Another solution is to let A be a sentence describing a field consisting of 5 elements. Namely, let A be the conjunction of the field axioms plus “there exist exactly 5 things”. We are using the algebraic fact that, up to isomorphism, there is exactly one field of 5 elements.

Exercise 4.1.12. Let L be a finite language with identity, and let M be a finite normal L-structure. Construct an L-sentence A such that, for all normal L-structures M′, M′ ⊧ A if and only if M′ is isomorphic to M.

Solution. Let a_{1}, …, a_{k} be the elements of U_{M}, and let P, …, Q be the predicates of L. As A we may take

∃x_{1} ⋯ ∃x_{k} (D_{P} ∧ ⋯ ∧ D_{Q} ∧ ∀y (Ix_{1}y ∨ ⋯ ∨ Ix_{k}y))

where for each n-ary predicate P of L, D_{P} is the conjunction of P x_{i_{1}} ⋯ x_{i_{n}} for each n-tuple ⟨a_{i_{1}}, …, a_{i_{n}}⟩ ∈ P_{M}, and ¬ P x_{i_{1}} ⋯ x_{i_{n}} for each n-tuple ⟨a_{i_{1}}, …, a_{i_{n}}⟩ ∉ P_{M}.

On the other hand, we have:

Theorem 4.1.13 (Löwenheim/Skolem Theorem).

1. If S is normally satisfiable in arbitrarily large finite domains, then S is normally satisfiable in some infinite domain.

2. If S is normally satisfiable in some infinite domain, then S is normally satisfiable in all infinite domains of cardinality ≥ the cardinality of S.

Proof. For the first part, let S^{∗} = S ∪ {H_{n} | n = 1, 2, …} where H_{n} is the sentence

∃x_{1} ⋯ ∃x_{n} ¬ (Ix_{1}x_{2} ∨ Ix_{1}x_{3} ∨ ⋯ ∨ Ix_{n−1}x_{n})

saying that there exist at least n things. Since S is normally satisfiable in arbitrarily large finite domains, each finite subset of S^{∗} is normally satisfiable. Hence, by Corollary 4.1.9, S^{∗} is normally satisfiable. But any normal L-structure satisfying S^{∗} satisfies S and has an infinite domain.

For the second part, let κ be a cardinal number ≥ the cardinality of S. Let L^{∗} = L∪{Q_{i} | i ∈ X}, where each Q_{i} is a new 1-ary predicate, and X is a set of cardinality κ. Let S^{∗} = S ∪ {∃x Q_{i}x | i ∈ X} ∪ {¬ ∃x (Q_{i}x ∧ Q_{j}x) | i, j ∈ X, i ≠ j} ∪ {identity axioms for L^{∗}}. Thus S^{∗} is a set of L^{∗}-sentences of cardinality κ. Furthermore, any domain in which S^{∗} is satisfiable will contain pairwise distinct elements a_{i}, i ∈ X, and will therefore have cardinality ≥ κ. By assumption, S is normally satisfiable in some infinite domain. It follows that each finite subset of S^{∗} is satisfiable. Hence, by the Compactness Theorems 2.6.1 and 2.6.2, S^{∗} is satisfiable. Hence, by part 2 of Theorem 2.7.1, S^{∗} is satisfiable in a domain of cardinality κ. Therefore, by Theorems 4.1.5 and 4.1.6, S^{∗} is normally satisfiable in a domain of cardinality ≤ κ, hence = κ. Let M^{∗} be a normal L^{∗}-structure with U_{M^{∗}} of cardinality κ. Let M be the reduct of M^{∗} to L, i.e., M is the L-structure with U_{M} = U_{M^{∗}} and P_{M} = P_{M^{∗}} for each predicate P in L. Then M normally satisfies S and U_{M} is of cardinality κ. □

Exercise 4.1.14. Let L be the following language:

Ox: x = 1

P xyz: x + y = z

Qxyz: x × y = z

Rxy: x < y

Sxy: x + 1 = y

Ixy: x = y (identity predicate)

For each positive integer n, let M_{n} be the normal L-structure

M_{n} = (U_{n}, O_{n}, P_{n}, Q_{n}, R_{n}, S_{n}, I_{n})

where

U_{n} = {1, …, n}

O_{n} = {1}

P_{n} = {⟨i, j, k⟩ ∈ (U_{n})^{3} | i + j = k}

Q_{n} = {⟨i, j, k⟩ ∈ (U_{n})^{3} | i × j = k}

R_{n} = {⟨i, j⟩ ∈ (U_{n})^{2} | i < j}

S_{n} = {⟨i, j⟩ ∈ (U_{n})^{2} | i + 1 = j}

I_{n} = {⟨i, j⟩ ∈ (U_{n})^{2} | i = j}

Exhibit an L-sentence Z such that, for all finite normal L-structures M′, M′ ⊧ Z if and only if M′ is isomorphic to M_{n} for some n.

Solution. As Z we may take the conjunction of the following clauses.

(a) ∀x ∀y (Rxy ∨ Ryx ∨ Ixy)

(b) ∀x ∀y (Rxy ⇒ ¬ Ryx)

(c) ∀x ∀y ∀z ((Rxy ∧ Ryz) ⇒ Rxz)

(d) ∀x ∀z (Sxz ⇔ (Rxz ∧ ¬ ∃y (Rxy ∧ Ryz)))

(e) ∀u (Ou ⇔ ¬ ∃x Rxu)

(f) ∀u (Ou ⇒ ∀x ∀z (P uxz ⇔ Sxz))
(g) ∀v ∀w (Svw ⇒ ∀x ∀z (P wxz ⇔ ∃y (Syz ∧ P vxy)))
(h) ∀u (Ou ⇒ ∀x ∀z (Quxz ⇔ Ixz))
(i) ∀v ∀w (Svw ⇒ ∀x ∀z (Qwxz ⇔ ∃y (Qvxy ∧ P xyz)))

Clauses (a), (b) and (c) say that R is an irreflexive linear ordering of the universe. Clause (d) says that S is the immediate successor relation, with respect to R. Clause (e) says that 1 is the first element of the universe, with respect to R. Clauses (f) and (g) define the addition predicate P, by induction along R, in terms of S. Clauses (h) and (i) define the multiplication predicate Q, by induction along R, in terms of S and P.

Exercise 4.1.15. Let L and M_{n} be as in Exercise 4.1.14. Show that there exists an infinite normal L-structure M = M_{∞} with the following property: for all L-sentences A, if M_{p} ⊧ A for all sufficiently large primes p, then M_{∞} ⊧ A. (Hint: Use the Compactness Theorem.)

Solution. Let S be the set of L-sentences A with the following property: there exists n = n_{A} such that for all primes p > n_{A}, M_{p} satisfies A. We claim that every finite subset of S is normally satisfiable. To see this, let S_{0} = {A_{1}, …, A_{k}} be a finite subset of S. Put n = max(n_{A_{1}}, …, n_{A_{k}}). Let p be any prime > n. Then M_{p} satisfies A_{1}, …, A_{k}. This proves our claim. By the Compactness Theorem for normal satisfiability (Corollary 4.1.9), it follows that S is normally satisfiable. Let M_{∞} be a normal L-structure satisfying S. Among the sentences of S are those asserting that the universe has at least k elements, for each positive integer k. Since M_{∞} satisfies these sentences, M_{∞} is infinite.

4.2 The Spectrum Problem

Definition 4.2.1. Let A be a sentence of the predicate calculus with identity. The spectrum of A is the set of positive integers n such that A is normally satisfiable in a domain of cardinality n. A spectrum is a set X of positive integers, such that X = spectrum(A) for some A.

Remark 4.2.2. The spectrum problem is the problem of characterizing the spectra, among all sets of positive integers. This is a famous and apparently difficult open problem.^{1} In particular, it is unknown whether the complement of a spectrum is necessarily a spectrum.

Example 4.2.3. We show that the set {n ≥ 1 | n is even} is a spectrum.

1Jones/Selman [1] show that X is a spectrum if and only if there exists a nondeterministic Turing machine which accepts X in time 2^{ck}, where k is the length of the input. Since the input is a positive integer n, we have k = [log_{2} n], as usual in computational number theory.

Let U be a nonempty set. A binary relation R ⊆ U^{2} is said to be an equivalence relation on U if it is reflexive, symmetric, and transitive, i.e., if the structure (U, R) satisfies (1) ∧ (2) ∧ (3):

\begin{matrix}(1) & ∀x Rxx \\ (2) & ∀x ∀y (Rxy ⇔ Ryx) \\ (3) & ∀x ∀y ∀z ((Rxy ∧ Ryz) ⇒ Rxz) \end{matrix}

In this situation, the equivalence classes [a]_{R} = {b ∈ U | ⟨a, b⟩ ∈ R}, a ∈ U, form a partition of U, i.e., a decomposition of the set U into pairwise disjoint, nonempty subsets.

Let A be the following sentence of the predicate calculus with identity:

(1) ∧ (2) ∧ (3) ∧ ∀x ∃y ((¬ Ixy) ∧ ∀z (Rxz ⇔ (Ixz ∨ Iyz)))

Intuitively, A says that R is an equivalence relation with the property that each equivalence class consists of exactly two elements. Obviously, a finite set U admits an equivalence relation with this property if and only if the cardinality of U is even. Thus the spectrum of A is the set of even numbers.

Exercises 4.2.4. Prove the following.

1. If X is a finite or cofinite^{2} set of positive integers, then X is a spectrum.

2. The set of even numbers is a spectrum.

3. The set of odd numbers is a spectrum.

4. If r and m are positive integers, {n ≥ 1 | n ≡ r mod m} is a spectrum.

5. If X and Y are spectra, X ∪ Y and X ∩ Y are spectra.

Solution.

1. Let E_{n} be sentence in the language with only the identity predicate I, saying that the universe consists of exactly n elements (Exercise 4.1.10). If X = {n_{1}, …, n_{k}}, then X is the spectrum of E_{n_{1}} ∨ ⋯ ∨ E_{n_{k}}, and the complement of X is spectrum of ¬ (E_{n_{1}} ∨ ⋯ ∨ E_{n_{k}}).

2. The even numbers are the spectrum of a sentence which says: R is an equivalence relation on the universe, such that each equivalence class consists of exactly two elements. For more details, see Example 4.2.3.

3. The odd numbers are the spectrum of a sentence which says: R is an equivalence relation on the universe, such that each equivalence class consists of exactly two elements, except for one equivalence class, which consists of exactly one element.

4. We may assume that 0 ≤ r < m. If r = 0, the set

2A set of positive integers is said to be cofinite if its complement is finite.

{n ≥ 1 : n ≡ 0 mod m} = {n ≥ 1 : m divides n with no remainder}

is the spectrum of a sentence which says: R is an equivalence relation on the universe, such that each equivalence class consists of exactly m elements. If r > 0, the set

{n ≥ 1 : n ≡ r mod m} = {n ≥ 1 : m divides n with remainder r}

is the spectrum of a sentence which says: R is an equivalence relation on the universe, such that each equivalence class consists of exactly m elements, except for one equivalence class, which consists of exactly r elements.

5. Assume that X is the spectrum of A and Y is the spectrum of B. Then X∪ Y is the spectrum of A ∨ B. Also, X∩Y is the spectrum of A ∧ B, provided A and B have no predicates in common except the identity predicate. To arrange for this, replace B by an analogous sentence in a different language.

Exercise 4.2.5. Prove that, for any sentence A of the predicate calculus with identity, at least one of spectrum(A) and spectrum(¬ A) is cofinite. (Hint: Use part 1 of Theorem 4.1.13.)

Example 4.2.6. We show that the set of composite numbers^{3} is a spectrum.

Let L be a language consisting of two binary predicates, R and S, as well as the identity predicate, I. Let A be an L-sentence saying that R and S are equivalence relations, each with more than one equivalence class, and

∀x ∀y (∃ exactly one z)(Rxz ∧ Syz).

Thus, for any normal L-structure M = (U_{M}, R_{M}, S_{M}, I_{M}) satisfying A, we have that R_{M} and S_{M} partition U_{M} into “rows” and “columns”, respectively, in such a way that the intersection of any “row” with any “column” consists of exactly one element of U_{M}. Thus, if U_{M} is finite, the elements of U_{M} are arranged in an m × n “matrix”, where m, n ≥ 2. Therefore, the number of elements in U_{M} is mn, a composite number. Conversely, for any m, n ≥ 2, there is an L-structure M as above, which satisfies A. Thus spectrum(A) is the set of composite numbers.

Exercise 4.2.7. Use the result of Exercise 4.1.14 to prove the following:

1. The set of prime numbers and its complement are spectra.

2. The set of squares {1, 4, 9, …} and its complement are spectra.

3. The set of powers of 2, {2^{n} | n = 1, 2, 3, …}, and its complement, are spectra.

3A composite number is an integer greater than 1 which is not prime.

4. The set of prime powers {p^{n} | p prime, n = 1, 2, …} and its complement are spectra.

Solution. Let Z be as in Exercise 4.1.14 above. For each of the given sets X, we exhibit a sentence A with the following properties: X is the spectrum of Z ∧ A, and the complement of X is the spectrum of Z ∧ ¬ A.

1. ∃z ((¬ ∃w Rzw) ∧ (¬ ∃x ∃y (Rxz ∧ Ryz ∧ Qxyz)) ∧ (¬ Oz)).

2. ∃z ((¬ ∃w Rzw) ∧ ∃x Qxxz).

3. ∃z ∃v ((¬ ∃w Rzw) ∧ (∃u (Ou ∧ Suv))

∧ ∀x ((¬ Ox ∧ ∃y Qxyz) ⇒ ∃w Qvwx)).

4. ∃z ∃v ((¬ ∃w Rzw) ∧ (¬ ∃x ∃y (Rxv ∧ Ryv ∧ Qxyv)) ∧ (¬ Ov)

∧ ∀x ((¬ Ox ∧ ∃y Qxyz) ⇒ ∃w Qvwx)).

Exercise 4.2.8.

1. The Fibonacci numbers are defined recursively by F_{1} = 1, F_{2} = 2, F_{n} = F_{n−1} + F_{n−2} for n ≥ 3. Show that the set of Fibonacci numbers

{F_{n} | n = 1, 2, …} = {1, 2, 3, 5, 8, 13, 21, 34, 55, …}

and its complement are spectra.

2. Show that {x^{y} | x, y ≥ 2} and its complement are spectra.

Exercise 4.2.9. Let X be a subset of {1, 2, 3, …}. Prove that if X is a spectrum then {n^{2} | n ∈ X} is a spectrum.

4.3 Predicate Calculus With Operations

In this section we extend the syntax and semantics of the predicate calculus, to encompass operations. As examples of operations, we may cite the familiar mathematical operations of addition (+) and multiplication (×). Such operations are considered binary, because they take two arguments. More generally, we consider n-ary operations.

Definition 4.3.1 (languages). A language is a set of predicates P, Q, R, … and operations f, g, h, . . .. Each predicate and each operation is designated as n-ary for some nonnegative^{4} integer n.

Definition 4.3.2 (terms, formulas, sentences). Let L be a language, and let U be a set. The set of L-U-terms is generated as follows.

1. Each variable is an L-U-term.

4A 0-ary operation is known as a constant. Syntactically, constants behave as parameters.

2. Each element of U is an L-U-term.

3. If f is an n-ary operation of L, and if t_{1}, …, t_{n} are L-U-terms, then ft_{1} ⋯ t_{n} is an L-U-term.

An L-U-term is said to be variable-free if no variables occur in it. An atomic L-U-formula is an expression of the form

P t_{1} ⋯ t_{n}

where P is an n-ary predicate of L, and t_{1}, …, t_{n} are L-U-terms. The set of L-U-formulas is generated as in clauses 2, 3, 4 and 5 of Definition 2.1.3. The notions of substitution, free variables, and L-U-sentences are defined as in Section 2.1. Note that P t_{1} ⋯ t_{n} is a sentence if and only if it is variable-free.

Definition 4.3.3 (structures). An L-structure M consists of a nonempty set U_{M}, an n-ary relation P_{M} ⊆ (U_{M})^{n} for each n-ary predicate P of L, and an n-ary function f_{M} : (U_{M})^{n} → U_{M} for each n-ary operation f of L.

Definition 4.3.4 (isomorphism). Two L-structures M and M′ are said to be isomorphic if there exists an isomorphism of M onto M′, i.e., a one-to-one correspondence ϕ : U_{M} ≅ U_{M′} such that:

1. for all n-ary predicates P of L and all n-tuples ⟨a_{1}, …, a_{n}⟩ ∈ (U_{M})^{n}, ⟨a_{1}, …, a_{n}⟩ ∈ P_{M} if and only if ⟨ϕ(a_{1}), …, ϕ(a_{n})⟩ ∈ P_{M′}.

2. for all n-ary operations f of L and all n-tuples ⟨a_{1}, …, a_{n}⟩ ∈ (U_{M})^{n}, ϕ(f_{M}(a_{1}, …, a_{n}) = f_{M′}(ϕ(a_{1}), …, ϕ(a_{n})).

Lemma 4.3.5 (valuations). Let M be an L-structure.

1. There is a unique valuation

v_{M} : {t | t is a variable-free L-U_{M}-term} → U_{M}

defined as follows:

(a) v_{M}(a) = a for all a ∈ U_{M}.

(b) v_{M}(ft_{1} ⋯ t_{n}) = f_{M}(v_{M}(t_{1}), …, v_{M}(t_{n})) for all n-ary operations f of L and all variable-free L-U_{M}-terms t_{1}, …, t_{n}.

2. There is a unique valuation

v_{M} : {A | A is an L-U_{M}-sentence} → {T, F}

defined as follows. For atomic L-U-sentences, we have

v_{M}(P t_{1} ⋯ t_{n}) = \{ \begin{matrix}T & if ⟨v_{M}(t_{1}), …, v_{M}(t_{n})⟩ ∈ P_{M}, \\ F & if ⟨v_{M}(t_{1}), …, v_{M}(t_{n})⟩ ∉ P_{M}. \end{matrix}

For non-atomic L-U_{M}-sentences, v_{M}(A) is defined as in clauses 2 through 8 of Lemma 2.2.4.

Proof. The proof is as for Lemma 2.2.4. □

Definition 4.3.6 (tableau method). The signed and unsigned tableau methods carry over to predicate calculus with operations. We modify the tableau rules as follows.

Signed:

⋮ ; T ∀x A ; ⋮ ; | ; T A[x/t]  ⋮ ; F ∃x A ; ⋮ ; | ; F A[x/t]

where t is a variable-free term

⋮ ; T ∃x A ; ⋮ ; | ; T A[x/a]  ⋮ ; F ∀x A ; ⋮ ; | ; F A[x/a]

where a is a new parameter

Unsigned:

⋮ ; ∀x A ; ⋮ ; | ; A[x/t]  ⋮ ; ¬ ∃x A ; ⋮ ; | ; ¬ A[x/t]

where t is a variable-free term

⋮ ; ∃x A ; ⋮ ; | ; A[x/a]  ⋮ ; ¬ ∀x A ; ⋮ ; | ; ¬ A[x/a]

where a is a new parameter Remark 4.3.7 (soundness and completeness). With the tableau rules as above, the Soundness Theorem 2.3.13 carries over unchanged to the context of predicate calculus with operations. The results of Section 2.4 on logical equivalence also carry over. The notion of U-repleteness (Definition 2.5.2) is modified to say that, for example, if S contains ∀x A then S contains A[x/t] for all variable-free L-U-terms t. The conclusion of Hintikka’s Lemma 2.5.3 is modified to say that S is satisfiable in the domain of variable-free L-U-terms. The conclusion of the Completeness Theorem 2.5.5 is modified to say that X_{1}, …, X_{k} is satisfiable in the domain of variable-free L-V -terms. The Compactness Theorems 2.6.1 and 2.6.2 carry over unchanged.

Remark 4.3.8 (satisfiability in a domain). The notion of satisfiability in a domain carries over unchanged to the context of predicate calculus with operations. Theorems 2.2.6 and 2.2.11 on isomorphism, and Theorem 2.7.1 on satisfiability in infinite domains, also carry over. Theorem 2.7.3 carries over in an appropriately modified form. See Theorem 4.3.9 and Exercise 4.3.10 below.

Theorem 4.3.9. Let M and M′ be L-structures. Assume that ϕ : U_{M} → U_{M′} is an onto mapping such that conditions 1 and 2 of Definition 4.3.4 hold. Then as in Theorem 2.2.6 we have v_{M}(A) = v_{M′}(A′) for all L-U_{M}-sentences A, where A′ = A[a_{1}/ϕ(a_{1}), …, a_{k}/ϕ(a_{k})]. In particular, M and M′ satisfy the same L-sentences.

Proof. The proof is similar to that of Theorem 2.7.3. □

Exercise 4.3.10. Use Theorem 4.3.9 to show that Corollary 2.7.4 carries over to the context of predicate calculus with operations.

Remark 4.3.11 (companions and proof systems). In our notion of companion (Definition 3.2.3), clauses (1) and (4) are modified as follows:

\begin{matrix}(1) & (∀x B) ⇒ B[x/t] \\ (4) & B[x/t] ⇒ (∃x B) \end{matrix}

where t is any variable-free term. In our Hilbert-style proof system LH , the instantiation rules are modified as follows:

(a) (∀x B) ⇒ B[x/t] (universal instantiation)

(b) B[x/t] ⇒ (∃x B) (existential instantiation)

where t is any variable-free term. Also, our Gentzen-style proof system LG is modified in accordance with the modified tableau rules. With these changes, the soundness and completeness of LG and LH carry over.

Exercise 4.3.12 (the Interpolation Theorem). Strengthen the Interpolation Theorem 3.5.1 to say that each operation, predicate and parameter occurring in I occurs in both A and B. (Hint: The version with operations can be deduced from the version without operations.)

Exercise 4.3.13. Skolemization.

4.4 Predicate Calculus with Identity and Operations

Remark 4.4.1 (predicate calculus with identity and operations). We augment the identity axioms (Definition 4.1.2) as follows:

5. For each n-ary operation f of L, we have an axiom

∀x_{1} ⋯ ∀x_{n} ∀y_{1} ⋯ ∀y_{n} ((Ix_{1}y_{1} ∧ ⋯ ∧ Ix_{n}y_{n}) ⇒ Ifx_{1} ⋯ x_{n}fy_{1} ⋯ y_{n}).

The notions of normal structure and normal satisfiability are defined as before. The results of Section 4.1 on the predicate calculus with identity carry over unchanged to the predicate calculus with identity and operations. See also Exercise 4.4.2 below.

Exercise 4.4.2 (elimination of operations). Let L be a language with identity and operations. Let L^{o} be the language with identity and without operations, obtained by replacing each n-ary operation f belonging to L by a new (n + 1)- ary predicate P_{f} belonging to L^{o}. Each normal L-structure M gives rise to a normal L^{o}-structure M^{o} where

(P_{f})_{M^{o}} = {⟨a_{1}, …, a_{n}, b⟩ ∈ (U_{M})^{n+1} | f_{M}(a_{1}, …, a_{n}) = b}.

For each n-ary operation f of L, let G_{f} be the L^{o}-sentence

∀x_{1} ⋯ ∀x_{n} ∃y ∀z (Iyz ⇔ P_{f}x_{1} ⋯ x_{n}z).

1. Show that to each L-sentence A we may associate an L^{o}-sentence A^{o} such that, for all L-structures M, M ⊧ A if and only if M^{o} ⊧ A^{o}.

2. Show that a normal L^{o}-structure satisfies the sentences G_{f}, f in L, if and only if it is of the form M^{o} for some L-structure M.

Exercise 4.4.3. Show that the spectrum problem for predicate calculus with identity and operations is equivalent to the spectrum problem for predicate calculus with identity and without operations, as previously discussed in Section 4.2. In other words, given a sentence A involving some operations, construct a sentence A^{oo} involving no operations, such that spectrum(A) = spectrum(A^{oo}). (Hint: Use the result of Exercise 4.4.2. Note that A^{oo} will not be the same as the A^{o} of Exercise 4.4.2.)

Remark 4.4.4 (predicate calculus with equality). The predicate calculus with identity and operations is well suited for the study of algebraic structures such as number systems, groups, rings, etc. In such a context, one often writes t_{1} = t_{2} instead of It_{1}t_{2}, and one refers to predicate calculus with equality rather than predicate calculus with identity. In this notation, the equality axioms (i.e., the identity axioms) read as follows:

∀x (x = x),

∀x ∀y (x = y ⇔ y = x),

∀x ∀y ∀z ((x = y ∧ y = z) ⇒ x = z),

∀x_{1} ∀y_{1} ⋯ ∀x_{n} ∀y_{n} ((x_{1} = y_{1} ∧ ⋯ ∧ x_{n} = y_{n}) ⇒ (P x_{1} ⋯ x_{n} ⇔ P y_{1} ⋯ y_{n})), for each n-ary predicate P,

∀x_{1} ∀y_{1} ⋯ ∀x_{n} ∀y_{n} ((x_{1} = y_{1} ∧ ⋯ ∧ x_{n} = y_{n}) ⇒ fx_{1} ⋯ x_{n} = fy_{1} ⋯ y_{n}), for each n-ary operation f .

One also uses customary algebraic notation, e.g., t_{1} + t_{2} instead of +t_{1}t_{2}, t_{1} × t_{2} or t_{1}t_{2} instead of ×t_{1}t_{2}, etc. To avoid ambiguity, parentheses are used.

Examples 4.4.5 (groups and rings). Using predicate calculus with identity and operations, a group may be viewed as a normal L-structure

G = (U_{G}, f_{G}, i_{G}, e_{G}, I_{G}).

Here U_{G} is the underlying set of the group, and L is the language {f, i, e, I}, where f is the group composition law (a binary operation), i is group inversion (a unary operation), e is the group identity element (a 0-ary operation, i.e., a constant), and I is the identity predicate (a binary predicate). We could refer to L as the language of groups. It is customary to write G instead of U_{G}, t_{1} · t_{2} or t_{1}t_{2} instead of ft_{1}t_{2}, t^{−1} instead of it, 1 instead of e, and t_{1} = t_{2} instead of It_{1}t_{2}. Thus

G = (G, ·_{G},^{−1}_{G}, 1_{G}, =_{G})

and G is required to satisfy the group axioms, consisting of the identity axioms for L, plus ∀x ∀y ∀z ((xy)z = x(yz)), ∀x (x^{−1}x = xx^{−1} = 1), ∀x (1x = x1 = x).

Similarly, a ring may be viewed as a normal structure

R = (R, +_{R}, ·_{R}, −_{R}, 0_{R}, 1_{R}, =_{R})

where + and · are binary operations, − is a unary operation, 0 and 1 are constants, and = is the equality predicate. We could refer to the language {+, ·, −, 0, 1, =} as the language of rings. R is required to satisfy the ring axioms, consisting of the identity axioms plus ∀x ∀y ∀y (x + (y + z) = (x + y) + z), ∀x ∀y (x + y = y + x), ∀x (x + 0 = x), ∀x (x + (−x) = 0), ∀x ∀y ∀z (x · (y · z) = (x · y) · z), ∀x (x · 1 = 1 · x = x), ∀x ∀y ∀z (x · (y + z) = (x · y) + (x · z)), ∀x ∀y ∀z ((x + y) · z = (x · z) + (y · z)), 0 ≠ 1.

Exercise 4.4.6. Let G be a group. For a ∈ G write a^{n} = a · · · · · a (n times). Thus a^{1} = a and a^{n+1} = a^{n} · a. We say that G is a torsion group if for all a ∈ G there exists a positive integer n such that a^{n} = 1. We say that G is torsion-free if for all a ∈ G, if a ≠ 1 then a^{n} ≠ 1 for all positive integers n.

1. Show that the class of torsion-free groups can be characterized by a set of sentences. I.e., there is a set of sentences S such that, for all groups G, G is torsion-free if and only if G ⊧ S.

Solution. Let S = {A_{n} : n ≥ 2}, where A_{n} is the sentence

∀x (x ≠ 1 ⇒ x^{n} ≠ 1).

Clearly the groups satisfying S are exactly the torsion-free groups.

2. Show that the class of torsion-free groups cannot be characterized by a finite set of sentences.

Solution. Suppose S′ were a finite of sentences such that the groups satisfying S′ are exactly the torsion-free groups. In particular, each sentence in S′ is a logical consequence of the group axioms plus S = {A_{n} : n ≥ 2} as above. By the Compactness Theorem, each sentence in S′ is a logical consequence of the group axioms plus {A_{2}, …, A_{n}} for sufficiently large n. Since S′ is finite, there is a fixed n such that all of the sentences in S′ are logical consequences of the group axioms plus {A_{2}, …, A_{n}}. Now let G be a torsion group satisfying {A_{2}, …, A_{n}}. (For example, we may take G to be the additive group of integers modulo p, where p is a prime number greater than n.) Then G satisfies S′ yet is not torsion-free, contradicting our assumption on S′.

3. Show that the class of torsion groups cannot be characterized by a set of sentences. I.e., there is no set of sentences S with the property that, for all groups G, G is a torsion group if and only if G ⊧ S.

Exercise 4.4.7. Let L be the language of groups. Let S be the set of Lsentences which are true in all finite groups. Define a pseudo-finite group to be a group which satisfies S. Note that every finite group is pseudo-finite.

Does there exist an infinite, pseudo-finite group? Prove your answer.

4.5 Many-Sorted Predicate Calculus

Definition 4.5.1 (many-sorted languages). A many-sorted language consists of

1. a set of sorts σ, τ, …,

2. a set of predicates P, Q, …, each designated as n-ary of type (σ_{1}, …, σ_{n}) for some nonnegative integer n and sorts σ_{1}, …, σ_{n},

3. a set of operations f, g, …, each designated as n-ary of type (σ_{1}, …, σ_{n}, τ) for some nonnegative integer n and sorts σ_{1}, …, σ_{n}, τ.

Definition 4.5.2 (terms, formulas, sentences). Let L be a many-sorted language. For each sort σ, we assume a fixed, countably infinite set of variables of sort σ, denoted x^{σ}, y^{σ}, z^{σ}, . . .. Let U = (U^{σ}, U^{τ} , …) consist of a set U^{σ} for each sort σ of L. The L-U-terms are generated as follows.

1. Each variable of sort σ is a term of sort σ.

2. Each element of U^{σ} is a term of sort σ.

3. If f is an n-ary operaton of type (σ_{1}, …, σ_{n}, τ), and if t_{1}, …, t_{n} are terms of sort σ_{1}, …, σ_{n} respectively, then ft_{1} … t_{n} is a term of sort τ.

An atomic L-U-formula is an expression of the form P t_{1} … t_{n}, where P is an n-ary predicate of type (σ_{1}, …, σ_{n}), and t_{1}, …, t_{n} are terms of sort σ_{1}, …, σ_{n} respectively. The L-U-formulas are generated as in Definition 2.1.3, with clause 5 modified as follows:

5′. If x^{σ} is a variable of sort σ, and if A is an L-U-formula, then ∀x^{σ} A and ∃x^{σ} A are L-U-formulas.

Our notions of substitution, free and bound variables, sentences, etc., are extended in the obvious way to the many-sorted context. Naturally, the substitution A[x^{σ}/t] makes sense only when t is a term of sort σ. An L-formula is an L-U-formula where U_{σ} = ∅ for each sort σ.

Definition 4.5.3 (many-sorted structures). An L-structure M consists of

1. a nonempty set U_{M}^{σ} for each sort σ of L,

2. an n-ary relation P_{M} ⊆ U_{M}^{σ_{1}} × ⋯ × U_{M}^{σ_{n}} for each n-ary predicate P of type (σ_{1}, …, σ_{n}) belonging to L,

3. an n-ary function f_{M} : U_{M}^{σ_{1}} × ⋯ × U_{M}^{σ_{n}} → U_{M}^{τ} for each n-ary operation f of type (σ_{1}, …, σ_{n}, τ) belonging to L.

Notions such as isomorphism, valuation, truth, satisfiability, and results such as Theorem 2.2.6 on isomorphism, and Theorem 4.3.9 on onto mappings, carry over to the many-sorted context in the obvious way.

Definition 4.5.4 (many-sorted domains). We define a domain or universe for L to be an indexed family of nonempty sets U = (U^{σ}, U^{τ} , …), where σ, τ, … are the sorts of L. In this way, the notion of satisfiability in a domain generalizes to the many-sorted context.

Remark 4.5.5 (tableau method, proof systems). For each sort σ of L, fix a countably infinite set V^{σ} = {a^{σ}, b^{σ}, …}, the set of parameters of sort σ. Then the tableau method carries over in the obvious way, generalizing Remark 4.3.7. In the Completeness Theorem for the tableau method, we obtain satisfiability in the domain U = (U^{σ}, U^{τ} , …), where U^{σ} is the set of variable-free L-V -terms of sort σ, with V = (V^{σ}, V^{τ} , …). The soundness and completeness of our proof systems LH and LG and the Interpolation Theorem also carry over, just as in Section 4.3.

Remark 4.5.6 (identity predicates). For each sort σ of L, L may or may not contain a binary predicate I^{σ} of type (σ, σ) designated as the identity predicate for σ. As identity axioms we may take the universal closures of all L-formulas of the form

∀x^{σ} ∀y^{σ} (I^{σ}xy ⇒ (A ⇔ A[x/y]))

where A is atomic. An L-structure M is said to be normal if I_{M}^{σ} = {⟨a, a⟩ | a ∈ U_{M}^{σ}} for all σ such that I^{σ} belongs to L. The results of Section 4.1 concerning normal satisfiability carry over to the many-sorted context.

Definition 4.5.7 (languages with identity). A many-sorted language with identity is a many-sorted language which contains an identity predicate for each sort.

Remark 4.5.8 (many-sorted spectrum problem). Let L be a many-sorted language with identity. If A is an L-sentence and σ_{1}, …, σ_{k} are the sorts occurring in A, the spectrum of A is the set of k-tuples of positive integers (n_{1}, …, n_{k}) such that there exists a normal L-structure M with U_{M}^{σ_{i}} of cardinality n_{i}, for i = 1, …, k. In this way, the spectrum problem carries over to many-sorted predicate calculus. So far as I know, the problem of characterizing many-sorted spectra has not been investigated thoroughly.

Remark 4.5.9 (many-sorted Löwenheim/Skolem theorems). It is natural to try to generalize the Löwenheim/Skolem Theorem 4.1.13 to many-sorted predicate calculus. This is straightforward provided we consider only normal structures M where all of the domains U_{M}^{σ}, U_{M}^{τ}, … are of the same infinite cardinality. However, if we require U_{M}^{σ}, U_{M}^{τ}, … to be of specified distinct cardinalities, then this leads to difficult issues. Even for two sorts, the topic of so-called twocardinal theorems turns out to be rather delicate and complicated. See for example the model theory textbook of Marker [2].

Remark 4.5.10. Our reasons for including many-sorted predicate calculus in this course are as follows:

1. it is more useful ….

FIXME

Remark 4.5.11 (one-sorted languages). A language or structure is said to be one-sorted if it has only one sort. This term is used for contrast with the many-sorted generalization which we are considering in this section. Generally speaking, one-sorted logic tends to be a little simpler than many-sorted logic.

Theories, Models, Definability

5.1 Theories and Models

Definition 5.1.1. A theory T consists of a language L, called the language of T, together with a set of L-sentences called the axioms of T. Thus T = (L, S), where L is the language of T, and S is the set of axioms of T.

Definition 5.1.2. Let T = (L, S) be a theory.

1. A model of T is an L-structure M such that M satisfies S. If L contains identity predicates, then M is required to be normal with respect to these predicates.

2. A theorem of T is an L-sentence A such that A is true in all models of T, i.e., A is a logical consequence of the axioms of T. Equivalently, A is derivable in LH (S ∪ {identity axioms for L}).

If A is a theorem of T, we denote this by T ⊢ A.

3. T is finitely axiomatized if S is finite.

4. Two theories are equivalent if they have the same language and the same theorems. I.e., they have the same language and the same models.

5. T is finitely axiomatizable if it is equivalent to a finitely axiomatized theory.

Definition 5.1.3 (consistency, categoricity, completeness). Let T = (L, S) be a theory.

1. T is consistent if there exists at least one model of T. Equivalently, T is consistent if and only if there is no L-sentence A such that both T ⊢ A and T ⊢ ¬ A. Equivalently, T is consistent if and only if there exists an L-sentence A such that T ⊬ A.

2. T is categorical if T is consistent and all models of T are isomorphic.

3. T is complete if T is consistent and all models of T are elementarily equivalent. Equivalently, T is complete if and only if for all L-sentences A either T ⊢ A or T ⊢ ¬ A but not both.

Remark 5.1.4. Our formal notion of theory, as defined above, is intended as a precise explication of the informal notion of “deductive scientific theory”. The language of T is the vocabulary of our theory. The theorems of T are the assertions of our theory. The axioms of T are the basic assertions, from which all others are deduced. Consistency of T means that our theory is free of internal contradictions. Categoricity of T means that our theory is fully successful in that it fully captures the structure of the underlying reality described by the theory. Completeness of T means that our theory is sufficiently successful to decide the truth values of all statements expressible in the language of the theory.

Remark 5.1.5 (mathematical theories, foundational theories). Later in this chapter we shall present several interesting examples of theories. Loosely speaking, the examples are of two kinds.

The first kind consists of mathematical theories. By a mathematical theory we mean a theory which is introduced in order to describe a certain class of mathematical structures. See Section 5.2. Since the class is diverse, the theory is typically not intended to be complete. Nevertheless we shall see that, remarkably, several of these mathematical theories turn out to be complete.

The second kind consists of foundational theories, i.e., theories which are introduced in order to serve as a general axiomatic foundation for all of mathematics, or at least a large part of it. See Sections 5.5 and 5.6. Each such theory is intended to fully describe a specific, foundationally important model, known as the intended model of the theory. Although such theories are intended to be complete, we shall see in Chapter 6 that, regrettably, most of these theories turn out to be incomplete.

One way to show that a theory is complete is to show that it is categorical.

Theorem 5.1.6. If T is categorical, then (1) T is complete, and (2) the language of T is a language with identity.

Proof. Assume that T is categorical. Then any two models of T are isomorphic. Hence by Theorem 2.2.6 (see also Definition 4.5.3), any two models of T are elementarily equivalent. Hence T is complete. Also, by Theorem 2.7.3 (see also Theorem 4.3.9 and Definition 4.5.3), T contains an identity predicate for each sort in the language of T. □

On the other hand, we have:

Exercise 5.1.7. Let T be a complete theory in a language with identity. Let M be a model of T.

1. In the one-sorted case, show that T is categorical if and only if the universe U_{M} is finite.

2. In the many-sorted case with sorts σ, τ, …, show that T is categorical if and only if each of the universes U_{M}^{σ}, U_{M}^{τ}, … is finite.

Solution. If one of the universes U_{M}^{σ} is infinite, we can use the Löwenheim/Skolem Theorem 4.1.13 to blow it up to an arbitrarily large uncountable cardinality.

Remark 5.1.8. Theorem 5.1.6 and Exercise 5.1.7 show that we cannot use categoricity as a test for completeness, except in very special circumstances. A similar but more useful test is provided by the following theorem.

Definition 5.1.9. Let κ be an infinite cardinal number. A one-sorted theory T is said to be κ-categorical if all models of T of cardinality κ are isomorphic.

Theorem 5.1.10 (Vaught’s Test). Let T be a one-sorted theory. Assume that (a) T is consistent, (b) all models of T are infinite, and (c) there exists an infinite cardinal κ ≥ the cardinality of the language of T such that T is κ-categorical. Then T is complete.

Proof. Suppose T is not complete. Since T is consistent, there exist M_{1} and M_{2} which are models of T and not elementarily equivalent. By assumption (b), M_{1} and M_{2} are infinite. Let κ be an infinite cardinal ≥ the cardinality of the language of T. By the Löwenheim/Skolem Theorem 4.1.13, there exist models M′_{1}, M′_{2} of cardinality κ elementarily equivalent to M_{1}, M_{2} respectively. Clearly M′_{1}, M′_{2} are not elementarily equivalent. Hence, by Theorem 2.2.6, M′_{1} and M′_{2} are not isomorphic. This contradicts assumption (c). □

Exercise 5.1.11. Generalize Vaught’s Test to many-sorted theories.

5.2 Mathematical Theories

In this section we give several examples of theories suggested by abstract algebra and other specific mathematical topics. We point out that several of these mathematical theories are complete.

Example 5.2.1 (groups). The language of groups consists of a binary operation · (multiplication), a unary operation ^{−1} (inverse), a constant 1 (the identity element), and a binary predicate = (equality). The theory of groups consists of the equality axioms plus

∀x ∀y ∀z (x · (y · z) = (x · y) · z) (associativity),
∀x (x · x^{−1} = x^{−1} · x = 1) (inverses),
∀x (x · 1 = 1 · x = x) (identity).

A group is a model of the theory of groups. A group is said to be Abelian if it satisfies the additional axiom

∀x ∀y (x · y = y · x) (commutativity).

A torsion group is a group G such that for all a ∈ G there exists a positive integer n such that a^{n} = 1. A group G is torsion-free if for all a ∈ G, if a ≠ 1 then a^{n} ≠ 1 for all positive integers n. Note that G is torsion-free if and only if it satisfies the axioms ∀x (x^{n} = 1 ⇒ x = 1) for n = 2, 3, . . .. A group is said to be divisible if it satisfies the axioms ∀x ∃y (y^{n} = x), for n = 2, 3, . . ..

Exercise 5.2.2. Show that the theory of torsion-free Abelian groups is not finitely axiomatizable. Deduce that the theory of torsion-free groups is not finitely axiomatizable.

Solution. Suppose that the theory of torsion-free Abelian groups were finitely axiomatizable. By Compactness, the axioms would be logical consequences of the Abelian group axioms plus finitely many axioms of the form ∀x (x^{n} = 1 ⇒ x = 1), say n = 1, …, k. Let p be a prime number greater than k. Then the additive group of integers modulo p satisfies these axioms but is not torsion-free. This is a contradiction.

If the theory of torsion-free groups were finitely axiomatizable, then the theory of torsion-free Abelian groups would also be finitely axiomatizable, by adjoining the single axiom ∀x ∀y (x · y = y · x).

Exercise 5.2.3. Show that there exist Abelian groups G_{1} and G_{2} such that G_{1} is a torsion group, G_{1} is elementarily equivalent to G_{2}, yet G_{2} is not a torsion group. Deduce that there is no theory in the language of groups whose models are precisely the Abelian torsion groups. Hence, there is no theory in the language of groups whose models are precisely the torsion groups.

Solution. Let G_{1} be a torsion group with elements of arbitrarily large finite order. (For example, we could take G_{1} to be the additive group of rational numbers modulo 1.) Let L be the language of groups, and let S be the set of all L-sentences true in G_{1}. Let L^{∗} = L ∪ {c} where c is a new constant, and let S^{∗} = S ∪ {c^{n} ≠ 1 | n = 1, 2, …}. By choosing c ∈ G_{1} appropriately, we see that any finite subset of S^{∗} is normally satisfiable. By the Compactness Theorem for normal satisfiability (Corollary 4.1.9), it follows that S^{∗} is normally satisfiable, so let (G_{2}, c) be a model of S^{∗}. Then G_{2} is an Abelian group which is elementarily equivalent to G_{1} yet contains an element c of infinite order, hence is not a torsion group.

If T were an L-theory whose models are just the Abelian torsion groups, then G_{1} would be a model of T but G_{2} would not, contradicting the fact that G_{1} and G_{2} are elementarily equivalent.

If T were an L-theory whose models are just the torsion groups, then T ∪ {∀x ∀y (x · y = y · x)} would be an L-theory whose models are just the Abelian torsion groups.

Remark 5.2.4. Let DAG_{0} be the theory of infinite torsion-free divisible Abelian groups. It can be shown that DAG_{0} is κ-categorical for all uncountable cardinals κ. (This is because such groups may be viewed as vector spaces over the rational field, ℚ.) It follows by Vaught’s Test that DAG_{0} is complete.

Example 5.2.5 (linear orderings). The language of linear orderings consists of a binary predicate < plus the equality predicate =. The axioms for linear orderings are ∀x ∀y ∀z ((x < y ∧ y < z) ⇒ x < z), and ∀x (¬ x < x), and ∀x ∀y (x < y ∨ x = y ∨ x > y). A linear ordering is a model of these axioms.

A linear ordering is said to be nontrivial if it satisfies ∃x ∃y (x < y). It is said to be dense if it is nontrivial and satisfies ∀x ∀y (x < y ⇒ ∃z (x < z < y)). It is said to be without end points if it satisfies ∀x ∃y (y < x) and ∀x ∃y (y > x). It is said to with end points if it satisfies ∃x ¬ ∃y (y < x) and ∃x ¬ ∃y (y > x). An example of a dense linear ordering without end points is (ℚ, <), where ℚ is the set of rational numbers, and < is the usual ordering of ℚ.

Remark 5.2.6. It can be shown that, up to isomorphism, (ℚ, <) is the unique countable dense linear ordering without end points. (This is proved by a backand-forth argument.) Hence, if we let DLO be the theory of dense linear ordering without end points, DLO is ℵ_{0}-categorical. It follows by Vaught’s Test that DLO is complete.

Example 5.2.7 (graphs). The language of graphs consists of a binary predicate, R, plus the equality predicate, =. The theory of graphs consists of the equality axioms plus ∀x ∀y (Rxy ⇔ Ryx) and ∀x ¬ Rxx. A graph is a model of the theory of graphs.

Thus a graph is essentially an ordered pair G = (V_{G}, R_{G}), where V_{G} is a nonempty set and R_{G} is a symmetric, irreflexive relation on V_{G}. The elements of V_{G} are called vertices. Two vertices a, b ∈ V_{G} are said to be adjacent if ⟨a, b⟩ ∈ R_{G}. A path from a to b is a finite sequence of pairwise distinct vertices a = v_{0}, v_{1}, …, v_{n} = b such that a = v_{0} is adjacent to v_{1}, v_{1} is adjacent to v_{2}, …, v_{n−1} is adjacent to v_{n} = b. G is said to be connected if for all a, b ∈ V_{G} there exists a path from a to b. Equivalently, G is connected if and only if, for all partitions of V_{G} into two disjoint nonempty sets X and Y, there exist a ∈ X and b ∈ Y such that a and b are adjacent.

Exercise 5.2.8. Show that there exist graphs G_{1} and G_{2} such that G_{1} is connected, G_{1} is elementarily equivalent to G_{2}, yet G_{2} is not connected. Deduce that there is no theory T in the language of graphs such that the models of T are exactly the connected graphs.

Solution. If a and b are two vertices in a graph, we define d(a, b), the distance from a to b, to be the smallest length of a path from a to b, or ∞ if there is no such path. Let G_{1} be a graph which is connected yet contains pairs of vertices which are at distance n for arbitrarily large n. (For example, we may take G_{1} = (ℕ, R_{1}) where R_{1} = {⟨n, n + 1⟩, ⟨n + 1, n⟩ | n ∈ ℕ}.) Let L = {R, =} be the language of graphs, and let S be the set of L-sentences satisfied by G_{1}. Let L^{∗} = L∪{a, b} where a, b are new constants, and let S^{∗} = S∪{A_{n} | n = 1, 2, …} where A_{n} is an L^{∗}-sentence saying that there is no path of length n from a to b. By choosing a, b ∈ G_{1} appropriately, we see that all finite subsets of S^{∗} are normally satisfiable. Hence by the Compactness Theorem S^{∗} is normally satisfiable, so let (G_{2}, a, b) be a model of S^{∗}. Then G_{2} is a graph which is elementarily equivalent to G_{1}, yet a, b ∈ G_{2} are such that d(a, b) = ∞, hence G_{2} is not connected.

If there were an L-theory T whose models are exactly the connected graphs, then G_{1} would be a model of T but G_{2} would not, contradicting the fact that G_{1} and G_{2} are elementarily equivalent.

Exercise 5.2.9. A graph G is said to be random if for all finite sets of distinct vertices a_{1}, …, a_{m}, b_{1}, …, b_{n} there exists a vertex c such that c is adjacent to a_{1}, …, a_{m} and not adjacent to b_{1}, …, b_{n}. Show that the theory of random graphs is ℵ_{0}-categorical. It follows by Vaught’s Test that this theory is complete.

Solution. Let G and G′ be two random graphs of cardinality ℵ_{0}, say G = {a_{k} | k ∈ ℕ} and G′ = {a′_{k} | k ∈ ℕ}. We use a back-and-forth argument to construct an isomorphism of G onto G′. At stage n of the construction, we have a finite partial isomorphism, f_{n}, which maps a finite subset of G isomorphically onto a finite subset of G′. Start with f_{0} = ∅. Suppose we have already constructed f_{n}. To construct f_{n+1}, consider two cases. If n is even, let k_{n} be the least k such that a_{k} ∉ dom(f_{n}), and put c = a_{k_{n}}. By randomness of G′, find c′ ∈ G′ such that for all a ∈ dom(f_{n}), c′ is adjacent to f_{n}(a) if and only if c is adjacent to a. If n is odd, let k_{n} be the least k such that a′_{k} ∉ ran(f_{n}), and put c′ = a′_{k_{n}}. By randomness of G, find c ∈ G such that for all a ∈ dom(f_{n}), c is adjacent to a if and only if c′ is adjacent to f_{n}(a). In either case, let f_{n+1} = f_{n} ∪ {(c, c′)}. Finally, by construction, f = ⋃_{n=0}^{∞} f_{n} is an isomorphism of G onto G′.

Example 5.2.10 (rings). The language of rings consists of binary operations + and · (addition and multiplication), a unary operation − (subtraction), constants 0 and 1 (the additive and multiplicative identity elements), and a binary predicate = (equality). The theory of rings consists of the equality axioms plus

∀x ∀y ∀z (x + (y + z) = (x + y) + z),

∀x ∀y (x + y = y + x),

∀x (x + (−x) = 0),

∀x (x + 0 = x),

∀x ∀y ∀z (x · (y · z) = (x · y) · z),

∀x ∀y ∀z (x · (y + z) = (x · y) + (x · z)) (left distributivity),

∀x ∀y ∀z ((x + y) · z = (x · z) + (y · z)) (right distributivity),

∀x (x · 1 = 1 · x = x),

∀x (x · 0 = 0 · x = 0),

0 ≠ 1.

A ring is a model of the theory of rings. A ring is said to be commutative if it satisfies the additional axiom

∀x ∀y (x · y = y · x).

An example of a commutative ring is the ring of integers,

ℤ = {…, −2, −1, 0, 1, 2, …}.

An example of a non-commutative ring is the ring of 2 × 2 matrices.

Example 5.2.11 (fields). A field is a commutative ring satisfying the additional axiom

∀x (x ≠ 0 ⇒ ∃y (x · y = 1)).

A field is said to be of characteristic 0 if it satisfies

\underbrace{1 + ⋯ + 1}_{n} ≠ 0

for all positive integers n. Familiar fields such as the field of rational numbers, ℚ, the field of real numbers, ℝ, and the field of complex numbers, ℂ, are of characteristic 0. It can be shown that if a field satisfies \underbrace{1 + ⋯ + 1}_{n} = 0 for some

positive integer n, then the least such n is a prime number, p. In this case, our field is said to be of characteristic p. An example of a field of characteristic p is the ring of integers modulo p.

A field F is said to be algebraically closed if for all nontrivial polynomials f(z) = a_{n}z^{n} + ⋯ + a_{1}z + a_{0}, a_{n}, …, a_{1}, a_{0} ∈ F, a_{n} ≠ 0, n ≥ 1, there exists z ∈ F such that f(z) = 0. It is known that the complex field ℂ is algebraically closed. (This theorem is known as the Fundamental Theorem of Algebra.) Note that a field is algebraically closed if and only if it satisfies the axioms

∀x_{0} ∀x_{1} ⋯ ∀x_{n} (x_{n} ≠ 0 ⇒ ∃z (x_{n}z^{n} + ⋯ + x_{1}z + x_{0} = 0))

for n = 1, 2, 3, . . ..

Exercise 5.2.12. Show that the theory of fields of characteristic 0 is not finitely axiomatizable. Show that the theory ACF of algebraically closed fields is not finitely axiomatizable. Show that the theory ACF_{0} of algebraically closed fields of characteristic 0 is not finitely axiomatizable.

Solution. Suppose that the theory of fields of characteristic 0 were finitely axiomatizable. By Compactness, the axioms would be logical consequences of the field axioms plus finitely many axioms of the form \underbrace{1 + ⋯ + 1}_{n} ≠ 0, say

n = 1, …, k. Let p be a prime number greater than k. The field of integers modulo p satisfies these axioms but is not of characteristic 0, a contradiction.

Suppose ACF or ACF_{0} were finitely axiomatizable. By Compactness, the axioms would be logical consequences of the field axioms plus finitely many of the ACF_{0} axioms as presented in Example 5.2.11 above. But, for any finite subset of the ACF_{0} axioms, we can construct a field which satisfies these axioms yet is not algebraically closed. (The construction of such a field is perhaps somewhat delicate.) This gives a contradiction.

Exercise 5.2.13. Let L be the language of rings. Let S be the set of L-sentences which are true in the ring of integers modulo p for all but finitely many prime numbers p. Does there exist a field of characteristic 0 satisfying S? Prove your answer.

Solution. The answer is yes. Note first that, for each prime p, the ring of integers modulo p is actually a field. Hence S includes the field axioms. Let S_{0} = S ∪ \{\underbrace{1 + ⋯ + 1}_{n} ≠ 0 | n = 1, 2, …\}. Any finite subset of S_{0} is normally

satisfiable, e.g., in the integers modulo p for all sufficiently large primes p. By the Compactness Theorem for normal satisfiability (Corollary 4.1.9), it follows that S_{0} is normally satisfiable. The normal structures which satisfy S_{0} are fields of characteristic 0 satisfying S.

Remark 5.2.14. Let ACF_{0} be the theory of algebraically closed fields of characteristic 0. For each prime number p, let ACF_{p} be the theory of algebraically closed fields of characteristic p. It can be shown that the theories ACF_{0} and ACF_{p} are κ-categorical for all uncountable cardinals κ. It follows by Vaught’s Test that these theories are complete.

Example 5.2.15 (vector spaces). The language of vector spaces is a 2-sorted language with sorts σ and τ, denoting scalars and vectors respectively. For the scalars we have binary operations + and · of type (σ, σ, σ), a unary operation − of type (σ, σ), constants 0 and 1 of type σ, and an equality predicate = of type (σ, σ). For the vectors we have a binary operation + of type (τ, τ, τ), a unary operation − of type (τ, τ), a constant 0 of type τ, and an equality predicate = of type (τ, τ). In addition we have a binary operation · of “mixed” type (σ, τ, τ), denoting scalar multiplication.

The theory of vector spaces consists of the field axioms for scalars, the Abelian group axioms for vectors, and the axioms

∀x^{σ} ∀v^{τ} ∀w^{τ} (x · (v + w) = (x · v) + (x · w)),
∀x^{σ}∀v^{τ} (x · (−v) = −(x · v)),
∀x^{σ} (x · 0^{τ} = 0),
∀x^{σ} ∀y^{σ} ∀v^{τ} ((x + y) · v = (x · v) + (y · v)),
∀x^{σ}∀v^{τ} ((−x) · v = −(x · v)),
∀x^{σ} ∀y^{σ} ∀v^{τ} ((x · y) · v = x · (y · v)),
∀v^{τ} (1 · v = v),
∀v^{τ} (0 · v = 0)

for scalar multiplication. A vector space is a model of these axioms.

If V is a vector space, a set of vectors S in V is said to span V if every vector v in V can be written as a linear combination of vectors in S, i.e., v = a_{1} ·v_{1} +⋯+a_{n} ·v_{n} for some v_{1}, …, v_{n} ∈ S and scalars a_{1}, …, a_{n}. An important invariant of a vector space is its dimension, i.e., the minimum cardinality of a spanning set. It can be shown that, up to isomorphism over a field F, the unique vector space over F of dimension κ is the familiar space ⨁_{i<κ} F. Here the vectors are sequences ⟨a_{i} | i < κ⟩, with a_{i} ∈ F for all i, and a_{i} = 0 for all but finitely many i. Vector addition is given by

⟨a_{i} | i < κ⟩ + ⟨b_{i} | i < κ⟩ = ⟨a_{i} + b_{i} | i < κ⟩,

and scalar multiplication is given by

c · ⟨a_{i} | i < κ⟩ = ⟨c · a_{i} | i < κ⟩.

Example 5.2.16 (ordered algebraic structures). The language of ordered rings consists of the language of rings +, ·, −, 0, 1, =, together with <. The ordered field axioms consist of the field axioms, plus the linear ordering axioms, plus

∀x ∀y ∀z (x < y ⇔ x + z < y + z),
∀x ∀y ((x > 0 ∧ y > 0) ⇒ x · y > 0).

An ordered field is a model of these axioms. An example of an ordered field is the field of rational numbers (ℚ, <) with its usual ordering.

An ordered field (F, <) is said to be real-closed if for all polynomials f(x) = a_{n}x^{n} + ⋯ + a_{1}x + a_{0}, a_{n}, …, a_{1}, a_{0} ∈ F, and for all b, c ∈ F, if f(b) < 0 < f(c) then there exists x ∈ F between b and c such that f(x) = 0. Clearly the ordered field of real numbers (ℝ, <) is real-closed. Note that an ordered field is real-closed if and only if it satisfies the axioms

∀u ∀v ∀w_{0} ∀w_{1} ⋯ ∀w_{n}
((u < v ∧ w_{n}u^{n} + ⋯ + w_{1}u + w_{0} < 0 < w_{n}v^{n} + ⋯ + w_{1}v + w_{0})
⇒ ∃x (u < x < v ∧ w_{n}x^{n} + ⋯ + w_{1}x + w_{0} = 0))

for n = 1, 2, 3, . . ..

Remark 5.2.17 (elimination of quantifiers). Let RCOF be the theory of realclosed ordered fields. A famous and important theorem of Tarski says that RCOF is complete. This holds despite the fact that RCOF is not κ-categorical for any κ.

Tarski’s method of proof is as follows. A theory T = (L, S) is said to admit elimination of quantifiers if for all L-formulas A there exists a quantifier-free Lformula A^{∗} such that T ⊢ the universal closure of A ⇔ A^{∗}. Tarski uses algebraic methods to show that the theory RCOF admits elimination of quantifiers. For example, the formula ∃x (ax^{2} + bx + c = 0) is equivalent over RCOF to the quantifier-free formula (a = b = c = 0) ∨ (a = 0 ≠ b) ∨ (a ≠ 0 ≤ b^{2} − 4ac).

As a special case of quantifier elimination, we have that each sentence in the language of RCOF is equivalent over RCOF to a quantifier-free sentence. On the other hand, it is evident that the quantifier-free sentences of the language of RCOF are of a very simple nature, e.g., 1 + 0 = 1 ∧ (1 · 1) + 1 < 1 + 1 + 1. Since the truth values of such sentences are decided by the axioms of RCOF, it follows that RCOF is complete.

Exercise 5.2.18. Which of the following theories are complete? Justify your answers.

1. The theory of dense linear orderings with end points.

2. The theory of fields of characteristic 0.

3. The theory of infinite, torsion-free, Abelian groups.

4. The theory of finite-dimensional vector spaces over a field of 5 elements.

5. The theory of infinite-dimensional vector spaces over a field of 5 elements.

Solution.

1. As noted in Remark 5.2.6, the theory of dense linear orderings without end points is ℵ_{0}-categorical. It follows immediately that the theory of dense linear orderings with end points is ℵ_{0}-categorical. Hence, by Vaught’s Test, each of these theories is complete.

2. The fields ℚ, ℝ, and ℂ are of characteristic 0, yet they are not elementarily equivalent, as can be seen by considering the sentences ∃x (x · x = 1 + 1) and ∃z (z · z = −1). Therefore, the theory of fields of characteristic 0 is incomplete.

3. The additive groups of ℤ and ℚ are infinite, Abelian, and torsion-free, yet they are not elementary equivalent, as can be seen by considering the sentence ∃x (x + x = 1). Therefore, the theory of infinite, Abelian, torsion-free groups is incomplete.

4. The vector spaces of dimension n = 0, 1, 2, … over a particular finite field F are not elementarily equivalent, because they have different finite cardinalities 1, q, q^{2}, … where q is the cardinality of F. Therefore, the theory of finite-dimensional vector spaces over F is incomplete.

5. As noted in Example 5.2.15, any two vector spaces over the same field of the same dimension are isomorphic. On the other hand, for any infinite cardinal number κ, any vector space of cardinality κ over a finite field is of dimension κ. Combining these facts, we see that for any particular finite field F, the theory T_{F} of infinite-dimensional vector spaces over F is κ-categorical. Hence, by Vaught’s Test, T_{F} is complete.

5.3 Definability over a Model

Definition 5.3.1 (explicit definability). Let L be a language, let M be an Lstructure, and let R be an n-ary relation on U_{M}. We say that R is explicitly definable over M, or just definable over M, if there exists an L-formula D with n free variables x_{1}, …, x_{n} such that

R = {⟨a_{1}, …, a_{n}⟩ | M ⊧ D[x_{1}/a_{1}, …, x_{n}/a_{n}]}.

Example 5.3.2. Consider the binary relation < = {⟨a, b⟩ ∈ ℝ^{2} | a < b} on the set ℝ of real numbers. Viewing ℝ as a commutative ring, we see that for all a, b ∈ ℝ, a < b if and only if ℝ ⊧ ∃x (x ≠ 0 ∧ a + x^{2} = b). Thus < is explicitly definable over the commutative ring ℝ = (ℝ, +, −, ·, 0, 1, =) by the formula ∃z (z ≠ 0 ∧ x + z^{2} = y) with free variables x, y.

On the other hand, in view of Tarski’s theorem on elimination of quantifiers for RCOF (see Remark 5.2.17), any subset of ℝ which is definable over ℝ consists of a union of finitely many points and intervals. From this it follows that, for example, the set of integers is not definable over ℝ.

Example 5.3.3. Let ℕ = (ℕ, +, ·, 0, 1, <, =) be the natural number system. It can be shown that the class of relations which are explicitly definable over ℕ includes all relations which are computable in the sense of Turing. In particular, the 3-ary relation {⟨m, n, k⟩ ∈ ℕ^{3} | m = n^{k}} is definable over ℕ, as we now show.

Theorem 5.3.4. The exponential function (n, k) ↦ n^{k} is explicitly definable over the natural number system.

Proof. The proof uses some number-theoretic lemmas, as follows.

Lemma 5.3.5 (the Chinese Remainder Theorem). Let m_{1}, …, m_{k} be pairwise relatively prime. Given r_{1}, …, r_{k}, we can find r such that r ≡ r_{i} mod m_{i} for all i = 1, …, k.

Proof. We omit the proof of this well-known result. □

Lemma 5.3.6. For each k ∈ ℕ we can find infinitely many a ∈ ℕ such that the integers a + 1, 2a + 1, …, ka + 1 are pairwise relatively prime.

Proof. Let a be any multiple of k!. Suppose p is a prime number which divides both ai + 1 and aj + 1 where 1 ≤ i < j ≤ k. Since p divides ai + 1 and a is a multiple of k!, we clearly have p > k. On the other hand, p divides a(j − i), and j − i < k, hence p divides a, a contradiction since p divides ai + 1. □

Definition 5.3.7 (Gödel’s beta-function). We define β(a, r, i) = the remainder of r upon division by a·(i+1)+1. Note that the β-function is explicitly definable over the natural number system.

Lemma 5.3.8. Given a finite sequence of natural numbers n_{0}, n_{1}, …, n_{k}, we can find natural numbers a, r such that β(a, r, i) = n_{i} for all i = 0, 1, …, k.

Proof. Let a ≥ max{n_{i} | i ≤ k} be such that a · (i + 1) + 1, i ≤ k, are pairwise relatively prime. By the Chinese Remainder Theorem, we can find r such that r ≡ n_{i} mod a · (i + 1) + 1 for all i ≤ k. Since 0 ≤ n_{i} ≤ a < a · (i + 1) + 1, it follows that β(a, r, i) = n_{i}. □

Now, to prove Theorem 5.3.4, note that m = n^{k} holds if and only if ∃a ∃r (β(a, r, 0) = 1 ∧ β(a, r, k) = m ∧ ∀i (i < k ⇒ β(a, r, i) · n = β(a, r, i + 1))). □

Exercise 5.3.9. Let p_{n} be the nth prime number. Thus p_{0} = 2, p_{1} = 3, p_{2} = 5, p_{3} = 7, p_{4} = 11, etc. Show that the function k ↦ p_{k} is explicitly definable over the natural number system ℕ. (This means, show that the binary relation {⟨k, p_{k}⟩ | k ∈ ℕ} is explicitly definable over ℕ.)

Solution. Let A be a formula expressing that x is prime, for example

1 < x ∧ ¬ ∃u ∃v (u < x ∧ v < x ∧ u · v = x).

We then have p_{k} = n if and only if ∃a ∃r (B ∧ C), where B is

β(a, r, k) = n ∧ ∀i (i < k ⇒ β(a, r, i) < β(a, r, i + 1))

and C is

∀x (x ≤ n ⇒ (A ⇔ ∃i (i ≤ k ∧ β(a, r, i) = x))).

We now turn to implicit definability.

Definition 5.3.10 (implicit definability). Let L be a language, let M be an L-structure, and let R be an n-ary relation on U_{M}. We say that R is implicitly definable over M if there exists a sentence D^{∗} in the language L^{∗} = L ∪ \{\underline{R}\} with an additional n-ary predicate \underline{R}, such that for all n-ary relations R′ on U_{M}, (M, R′) ⊧ D^{∗} if and only if R′ = R.

Example 5.3.11. Let ℝ = (ℝ, +, −, ·, 0, 1, <, =) be the ordered field of real numbers. Consider the set of integers, ℤ ⊂ ℝ. As noted above, ℤ is not explicitly definable over ℝ. However, ℤ is implicitly definable over ℝ, by the following sentence with an additional unary predicate Z:

Z0 ∧ Z1 ∧ (¬ ∃x (Zx ∧ 0 < x < 1)) ∧ (∀x (Zx ⇔ Z(x + 1))).

Example 5.3.12. It can be shown that there exists a subset of ℕ which is implicitly definable over the natural number system ℕ = (ℕ, +, ·, 0, 1, <, =) but is not explicitly definable over ℕ. See Remark 6.4.6 and Exercise 6.4.7 below.

Definition 5.3.13 (automorphisms). Let M be a structure. An automorphism of M is an isomorphism of M onto itself. An n-ary relation R on U_{M} is said to be invariant if

R = {⟨f(a_{1}), …, f(a_{n})⟩ | ⟨a_{1}, …, a_{n}⟩ ∈ R}

for all automorphisms f of M.

Exercise 5.3.14. Let M be a structure. Show that any relation which is explicitly definable over M is implicitly definable over M. Show that any relation which is implicitly definable over M is invariant under all automorphisms of M. Give counterexamples showing that the converses of these assertions fail in general.

Solution. Let R be an n-ary relation over U_{M}. If R is explicitly defined over M by a formula D with free variables x_{1}, …, x_{n}, then R is implicitly defined over M by the L∪\{\underline{R}\}-sentence ∀x_{1} ⋯ ∀x_{n} (\underline{R}x_{1} ⋯ x_{n} ⇔ D). Now suppose R is implicitly defined over M by an L∪\{\underline{R}\}-sentence D^{∗}. Let f be an automorphism of M, and put R′ = {⟨f(a_{1}), …, f(a_{n})⟩ | ⟨a_{1}, …, a_{n}⟩ ∈ R}. Then f is an isomorphism of (M, R) onto (M, R′). Since (M, R) ⊧ D^{∗}, it follows by Theorem 2.2.6 that (M, R′) ⊧ D^{∗}. Hence R′ = R, i.e., R is invariant under f.

Consider the ordered field ℝ of real numbers. Example 5.3.11 shows that the subset ℤ of ℝ is implicitly definable over ℝ but not explicitly definable over ℝ. Since there are only countably many sentences, only countably many subsets of ℝ are implicitly definable over ℝ. However, all subsets of ℝ are invariant under automorphisms of ℝ, inasmuch as ℝ has no automorphisms except the identity.

Exercise 5.3.15. Let ℝ = (ℝ, +, −, ·, 0, 1, <, =) be the ordered field of real numbers. Show that the relations y = e^{x} and y = sin x are implicitly definable over ℝ. It can be shown that these relations are not explicitly definable over ℝ. (Hint: The relations y = e^{x} and y = sin x are implicitly defined by differential equations which can be expressed as formulas of the predicate calculus, using the ϵ-δ-method.)

Exercise 5.3.16. Show that if U_{M} is finite, then any relation which is implicitly definable over M is explicitly definable over M.

Solution. Let us say that ⟨a_{1}, …, a_{n}⟩, ⟨b_{1}, …, b_{n}⟩ ∈ (U_{M})^{n} are of the same ntype if (M, a_{1}, …, a_{n}) is elementarily equivalent to (M, b_{1}, …, b_{n}). Thus (U_{M})^{n} is partitioned into equivalence classes, the n-types. Since U_{M} is finite, there are only finitely many n-types, and each n-type is explicitly definable over M. Moreover, by Theorem 2.2.6 and Exercise 4.1.12, the n-types are just the orbits of (U_{M})^{n} under the automorphism group of M. If R ⊆ (U_{M})^{n} is implicitly definable over M, then R is invariant under automorphisms of M, hence R is the union of some of the n-types, hence R is explicitly definable over M.

Exercise 5.3.17. (In this exercise we assume familiarity with saturated models.) Show that if a structure M is saturated, then any relation which is implicitly definable over M is explicitly definable over M.

Exercise 5.3.18. Let G be a group which has infinitely many distinct subgroups. Prove that there exists a countable group G′ such that

1. G′ is elementarily equivalent to G, and

2. G′ has a subgroup which is not explicitly definable over G′.

Solution. Let S be the set of sentences which are true in G. Introduce a new unary predicate P, and let S′ consist of S plus the sentences P 1 and ∀x (P x ⇒ P x^{−1}) and ∀x ∀y ((P x ∧ P y) ⇒ P (x · y)) and ¬ ∀x (P x ⇔ D) where D is any formula with x as its only free variable. Since G has infinitely many subgroups, each finite subset of S′ is normally satisfiable in G by letting P be an appropriately chosen subgroup of G. It follows by Compactness plus Löwenheim/Skolem that we can find a countable normal structure (G′, P′) satisfying S′. Then G′ is a countable group which is elementarily equivalent to G, and P′ is a subgroup of G′ which is not explicitly definable over G′.

Remark 5.3.19. In this section we have considered explicit and implicit definability over a model, M. We have given examples showing that, in general, implicit definability over M does not imply explicit definability over M.

In Sections 5.4 and 5.8 below, we shall consider the related but more restrictive notions of explicit and implicit definability over a theory, T. It will be obvious that explicit definability over T implies explicit definability over any model of T, and implicit definability over T implies implicit definability over any model of T. A pleasant surprise is that explicit definability over T is equivalent to implicit definability over T. This is the content of Beth’s Definability Theorem, Theorem 5.8.2 below.

5.4 Definitional Extensions of Theories

We now show how theories can be usefully extended by adding new predicates and operations which are explicitly definable in terms of old predicates and operations. This method of extending a theory is known as definitional extension.

In this section we are considering only explicit definitional extensions. Later, in Section 5.8, we shall consider implicit definitional extensions. It will turn out that, in principle, an implicit definitional extension of a theory is always equivalent to an explicit definitional extension of the same theory.

Definition 5.4.1 (defining a new predicate). Let T = (L, S) be a theory, and let D be an L-formula with free variables x_{1}, …, x_{n}. Introduce a new n-ary predicate P, and let T′ = (L′, S′) where L′ = L ∪ {P } and S′ = S ∪ {∀x_{1} ⋯ ∀x_{n} (P x_{1} ⋯ x_{n} ⇔ D)}.

Definition 5.4.2 (defining a new operation). Let T = (L, S) be a theory with an identity predicate I. Let D be an L-formula with free variables x_{1}, …, x_{n}, y such that

T ⊢ ∀x_{1} ⋯ ∀x_{n} (∃ exactly one y) D,

i.e.,

T ⊢ ∀x_{1} ⋯ ∀x_{n} ∃z ∀y (Iyz ⇔ D)

where z is a new variable. Introduce a new n-ary operation f, and let T′ = (L′, S′) where L′ = L ∪ {f} and S′ = S ∪ {∀x_{1} ⋯ ∀x_{n} ∀y (Ifx_{1} … x_{n}y ⇔ D)}.

Remark 5.4.3. In Definition 5.4.2 above, we have assumed for simplicity that T is one-sorted. In case T is many-sorted, we make the obvious modifications. Namely, letting σ_{1}, …, σ_{n}, τ be the sorts of the variables x_{1}, …, x_{n}, y respectively, we require that z is a new variable of sort τ, I is an identity predicate of sort τ, and f is an operation of type (σ_{1}, …, σ_{n}, τ).

Remark 5.4.4. We are going to prove that these extensions of T are “trivial” or “harmless” or “inessential”, in the sense that each formula in the extended language L ∪ {P } or L ∪ {f} can be straightforwardly translated into an equivalent formula of the original language L. See Theorem 5.4.10 below.

Lemma 5.4.5. Let T = (L, S) and T′ = (L′, S′) be as in Definition 5.4.1 or 5.4.2. Then for all L-sentences A we have T′ ⊢ A if and only if T ⊢ A.

Proof. It suffices to show that, for each model M of T, there exists a model M′ of T′ such that M = M′↾L, i.e., M is the reduct of M′ to L. In the case of Definition 5.4.1, let M′ = (M, P_{M′}) where

P_{M′} = {⟨a_{1}, …, a_{n}⟩ | M ⊧ D[x_{1}/a_{1}, …, x_{n}/a_{n}]}.

In the case of Definition 5.4.2, let M′ = (M, f_{M′}) where f_{M′}(a_{1}, …, a_{n}) = the unique b such that M ⊧ D[x_{1}/a_{1}, …, x_{n}/a_{n}, y/b]. Clearly M′ is as desired. □

Definition 5.4.6 (translation). Let T = (L, S) and T′ = (L′, S′) be as in Definition 5.4.1 or 5.4.2. To each L′-formula A we associate an L-formula A′, the translation of A into L. In order to define A′, we first modify D, replacing the free and bound variables of D by new variables which do not occur in A. (Compare Definition 2.4.9.) In the case of Definition 5.4.1, where we are adding a new predicate P, we obtain A′ from A by replacing each atomic formula of the form P t_{1} … t_{n} by D[x_{1}/t_{1}, …, x_{n}/t_{n}].

In the case of Definition 5.4.2, where we are adding a new operation f, the translation is more complicated. For non-atomic A we obtain A′ by induction on the degree of A, putting (¬ A)′ = ¬ A′, (A ∧ B)′ = A′ ∧ B′, (∀x A)′ = ∀x A′, etc. For atomic A we obtain A′ by induction on the number of occurrences of f in A. If there are no occurrences of f in A, let A′ be just A. Otherwise, write A in the form B[w/ft_{1} ⋯ t_{n}] where w is a new variable and f does not occur in t_{1}, …, t_{n}, and let A′ be

∃w (D[x_{1}/t_{1}, …, x_{n}/t_{n}, y/w] ∧ B′)

or equivalently

∀w (D[x_{1}/t_{1}, …, x_{n}/t_{n}, y/w] ⇒ B′).

Lemma 5.4.7. Let T and T′ be as in Definition 5.4.1 or 5.4.2, and let A ↦ A′ be our translation of L′-formulas to L-formulas as in Definition 5.4.6. Then:

1. A′ has the same free variables as A and is equivalent to it over T′, i.e., T′ ⊢ A ⇔ A′.

2. Propositional connectives and quantifiers are respected, i.e., we have (¬ A)′ ≡ ¬ A′, (A ∧ B)′ ≡ A′ ∧ B′, (∀x A)′ ≡ ∀x A′, etc.

3. If A happens to be an L-formula, then A′ is just A.

Consequently, for all L′-sentences A we have T′ ⊢ A if and only if T ⊢ A′.

Proof. The first part is straightforward. For the last part, since T′ ⊢ A ⇔ A′, we obviously have T′ ⊢ A if and only if T′ ⊢ A′. But then, since A′ is an L-sentence, it follows by Lemma 5.4.5 that T′ ⊢ A if and only if T ⊢ A′. □

Definition 5.4.8 (definitional extensions). Let T be a theory. A definitional extension of T is a theory T^{∗} which is a union of sequences of theories T_{0}, T_{1}, …, T_{k} beginning with T_{0} = T such that each T_{i+1} is obtained by extending T_{i} as in Definition 5.4.1 or 5.4.2.

Definition 5.4.9 (conservative extensions). Let T = (L, S) and T^{∗} = (L^{∗}, S^{∗}) be theories such that L^{∗} ⊇ L. We say that T^{∗} is a conservative extension of T if, for all L-sentences A, T^{∗} ⊢ A if and only if T ⊢ A.

Theorem 5.4.10. Let T^{∗} be a definitional extension of T. Then T^{∗} is a conservative extension of T. Moreover, there is a straightforward translation A ↦ A^{∗} of L^{∗}-formulas to L-formulas, with the following properties.

1. A^{∗} has the same free variables as A and is equivalent to it over T^{∗}, i.e., T^{∗} ⊢ A ⇔ A^{∗}.

2. Propositional connectives and quantifiers are respected, i.e., we have (¬ A)^{∗} ≡ ¬ A^{∗}, (A ∧ B)^{∗} ≡ A^{∗} ∧ B^{∗}, (∀x A)^{∗} ≡ ∀x A^{∗}, etc.

3. If A happens to be an L-formula, then A^{∗} is just A.

Consequently, for all L^{∗}-sentences A, we have

T^{∗} ⊢ A if and only if T ⊢ A^{∗}.

Proof. This is clear from Lemmas 5.4.5 and 5.4.7. □

Remark 5.4.11. In practice, when it comes to working with specific theories T, the technique of definitional extensions is very useful. This is because formulas written in the extended language L^{∗} tend to be much shorter than their translations in L. This is particularly important for the foundational theories Z_{1}, Z_{2}, …, Z_{n}, …, Z_{∞}, ZC, ZFC which are discussed in Sections 5.5 and 5.6 below.

Exercise 5.4.12. Show that for any theory T there is a definitional extension of T which admits elimination of quantifiers.

Solution. Let L be the language of T. For each L-formula A with free variables x_{1}, …, x_{n} introduce a new n-ary predicate P_{A} and a new axiom

∀x_{1} ⋯ ∀x_{n} (P_{A}x_{1} ⋯ x_{n} ⇔ A).

The resulting theory admits elimination of quantifiers.

Exercise 5.4.13. Let T = (L, S) be a theory. Let A be an L-formula with free variables x_{1}, …, x_{n}, y. Let T′ = (L′, S′) where L′ consists of L plus a new nary operation f, and S′ consists of S plus ∀x_{1} ⋯ ∀x_{n} (A[y/fx_{1} ⋯ x_{n}] ⇔ ∃y A). Show that T′ is a conservative extension of T.

Solution. Let B be an L-sentence such that T′ ⊢ B. We must show that T ⊢ B. If T ⊬ B, let M be a model of T ∪ {¬ B}. Let M′ = (M, f_{M′}) where f_{M′} is an n-ary function on U_{M} with the following property: for all a_{1}, …, a_{n} ∈ U_{M} such that M ⊧ ∃y A[x_{1}/a_{1}, …, x_{n}/a_{n}], we have M ⊧ A[x_{1}/a_{1}, …, x_{n}/a_{n}, y/b] where b = f_{M′}(a_{1}, …, a_{n}). (Note that f_{M′} is not necessarily unique and is not necessarily definable over M. The existence of an f_{M′} with the desired property follows from the axiom of choice.) Clearly M′ is a model of T′ ∪ {¬ B}, hence T′ ⊬ B, a contradiction.

5.5 Foundational Theories

In this section and the next, we present several specific theories which are of significance in the foundations of mathematics. We point out that these theories are, in certain senses, “almost complete” or “practically complete.” On the other hand, we shall see in Chapter 6 that these theories are not complete.

Definition 5.5.1 (first-order arithmetic). One of the most famous and important foundational theories is first-order arithmetic, Z_{1}, also known as Peano Arithmetic, PA. The language of first-order arithmetic is L_{1} = {+, ·, 0, S, =} where + and · are binary operations, S is a unary operation, 0 is a constant, and = is the equality predicate. Let Q be the finitely axiomatizable L_{1}-theory with axioms

∀x (Sx ≠ 0),
∀x ∀y (Sx = Sy ⇒ x = y),
∀x (x + 0 = x),
∀x ∀y (x + Sy = S(x + y)),
∀x (x · 0 = 0),
∀x ∀y (x · Sy = (x · y) + x).

The axioms of Z_{1} consist of the axioms of Q plus the induction scheme, i.e., the universal closure of

(A[x/0] ∧ ∀x (A ⇒ A[x/Sx])) ⇒ ∀x A

where A is any L_{1}-formula.

Note that the induction scheme consists of an infinite set of axioms. It can be shown that Z_{1} is not finitely axiomatizable.

Remark 5.5.2 (practical completeness of first-order arithmetic). The intended model of Z_{1} is the natural number system

ℕ = (ℕ, +, ·, 0, S, =)

where ℕ = {0, 1, 2, …} and +, ·, 0, = are as expected, and S is the successor function, S(n) = n + 1 for all n ∈ ℕ. Obviously the axioms of Z_{1} are true in this model. The idea behind the axioms of Z_{1} is that we are trying to write down a set S_{1} of L_{1}-sentences with the property that, for all L_{1}-sentences A, S_{1} ⊢ A if and only if ℕ ⊧ A. In particular, the axioms of Z_{1} are intended to be complete. Unfortunately this intention cannot be fulfilled, as shown by Gödel’s First Incompleteness Theorem (see Chapter 6). However, it is known that Z_{1} “almost” fulfills the intention. This is because it has been found that, in practice, all or most of the theorems of number theory which can be written in (definitional extensions of) Z_{1} are either provable or refutable in Z_{1}. Exceptions are known, but the exceptions are obscure and marginal. In this sense, we can say that Z_{1} is “practically complete.”

Remark 5.5.3 (definitional extensions of first-order arithmetic). We have seen in Theorem 5.3.4 and Exercise 5.3.9 that the exponential function (n, k) ↦ n^{k} and the “kth prime” function k ↦ p_{k} are definable over ℕ, the intended model of Z_{1}. It can be shown that the same definitions work abstractly over the theory Z_{1}. Thus we have a definitional extension of Z_{1} in which basic properties such as ∀m ∀n ∀k (m^{k}n^{k} = (mn)^{k}) and ∀n ∀i ∀j (n^{i}n^{j} = n^{i+j}) can be stated and proved. Similarly, many other number-theoretical operations can be introduced, and their properties proved, in definitional extensions of Z_{1}. Our remarks above concerning practical completeness of Z_{1} apply all the more to these definitional extensions of Z_{1}.

Exercise 5.5.4. Show that the commutative laws ∀x ∀y (x + y = y + x) and ∀x ∀y (x · y = y · x) are theorems of Z_{1}. Similarly it can be shown that the associative laws ∀x ∀y ∀z (x + (y + z) = (x + y) + z) and ∀x ∀y ∀z (x · (y · z) = (x · y) · z) and the distributive law ∀x ∀y ∀z (x · (y + z) = (x · y) + (x · z)) are theorems of Z_{1}.

Definition 5.5.5 (second-order arithmetic). Another important foundational theory is second-order arithmetic, Z_{2}. See also my book [3].

The language of Z_{2} is a 2-sorted language, L_{2}, with sorts σ and τ designating numbers and sets respectively. The number variables x^{σ}, y^{σ}, … are written as i, j, k, l, m, n, …, while the set variables x^{τ} , y^{τ} , … are written as X, Y, Z, . . ..

The predicates and operations of L_{2} are +, ·, 0, S, =, ∈. Here + and · are binary number operations, S is a unary number operation, and 0 is a numerical constant. Thus + and · are of type (σ, σ, σ), S is of type (σ, σ), and 0 is of type σ. In addition, the numerical equality predicate = is a binary predicate of type (σ, σ), and the membership predicate ∈ is a binary predicate of “mixed” type (σ, τ).

We identify the variables x, y, … of L_{1} with the number variables m, n, … of L_{2}. Also, we identify the operations and predicates +, ·, 0, S, = of L_{1} with the +, ·, 0, S, = of L_{2}. Thus L_{1} is a sublanguage of L_{2}.

The axioms of Z_{2} consist of Q (Definition 5.5.1), i.e.,

∀m (Sm ≠ 0),

∀m ∀n (Sm = Sn ⇒ m = n),

∀m (m + 0 = m),

∀m ∀n (m + Sn = S(m + n)),

∀m (m · 0 = 0),

∀m ∀n (m · Sn = (m · n) + m),

plus the induction axiom

∀X ((0 ∈ X ∧ ∀n (n ∈ X ⇒ Sn ∈ X)) ⇒ ∀n (n ∈ X)),

plus the comprehension scheme, i.e., the universal closure of

∃X ∀n (n ∈ X ⇔ A)

where A is any L_{2}-formula in which X does not occur.

Note that the comprehension scheme consists of an infinite set of axioms. It can be shown that Z_{2} is not finitely axiomatizable.

Remark 5.5.6 (practical completeness of second-order arithmetic). The intended model of Z_{2} is the 2-sorted structure

P (ℕ) = (ℕ, P (ℕ), +, ·, 0, S, =, ∈)

where (ℕ, +, ·, 0, S, =) is the natural number system (see Remark 5.5.2), P (ℕ) is the power set of ℕ, i.e., the set of all subsets of ℕ,

P (ℕ) = {X | X ⊆ ℕ},

and ∈ is the membership relation between natural numbers and sets of natural numbers, i.e.,

∈ = {⟨n, X⟩ ∈ ℕ × P (ℕ) | n ∈ X}.

As in the case of Z_{1} (compare Remark 5.5.2), it is obvious that the axioms of Z_{2} are true in the 2-sorted structure P (ℕ), and again, the idea behind Z_{2} is that we are trying to write down axioms for the complete theory of P (ℕ). This intention cannot be fulfilled because of the Gödel Incompleteness Theorem, but again, Z_{2} is “practically complete.”

Remark 5.5.7 (definitional extensions of second-order arithmetic). The foundational significance of Z_{2} is that, within definitional extensions of Z_{2}, it is possible and convenient to develop the bulk of ordinary countable and separable mathematics. This includes differential equations, analysis, functional analysis, algebra, geometry, topology, combinatorics, descriptive set theory, etc. For details of how this can be done, see my book [3].

Exercise 5.5.8. As noted in Defintion 5.5.5, L_{1} is a sublanguage of L_{2}. Show that all of the axioms of Z_{1} are theorems of Z_{2}. In this sense Z_{1} is a subtheory of Z_{2}.

Solution. Recall that Q is a subtheory of Z_{2}. It remains to show that, for any L_{1}-formula A, the universal closure of (A[n/0] ∧ ∀n (A ⇒ A[n/Sn])) ⇒ ∀n A is a theorem of Z_{2}. More generally, we shall prove this when A is any L_{2}-formula. Let the free variables of A be among n, n_{1}, …, n_{k}, X_{1}, …, X_{l}. Within Z_{2} we reason as follows. Given n_{1}, …, n_{k}, X_{1}, …, X_{l}, we use the comprehension scheme of Z_{2} to prove the existence of a set X such that ∀n (n ∈ X ⇔ A). From the induction axiom of Z_{2} we have (0 ∈ X ∧ ∀n (n ∈ X ⇒ Sn ∈ X)) ⇒ ∀n (n ∈ X). From this it follows that (A[n/0] ∧ ∀n (A ⇒ A[n/Sn])) ⇒ ∀n A. Since this holds for arbitrary n_{1}, …, n_{k}, X_{1}, …, X_{l}, we obtain the universal closure.

Remark 5.5.9 (nth order arithmetic). Similarly we can define third-order arithmetic, Z_{3}, a 3-sorted theory with variables intended to range over numbers, sets of numbers, and sets of sets of numbers. The intended model of Z_{3} is the 3-sorted structure

P^{2}(ℕ) = (ℕ, P (ℕ), P (P (ℕ)), +, ·, 0, S, =, ∈_{1}, ∈_{2})

where

∈_{1} = {⟨n, X⟩ ∈ ℕ × P (ℕ) | n ∈ X}

and

∈_{2} = {⟨X, A⟩ ∈ P (ℕ) × P (P (ℕ)) | X ∈ A}.

More generally, for each positive integer n ≥ 1 we can define nth-order arithmetic, Z_{n}, an n-sorted theory whose intended model is the n-sorted structure

P^{n−1}(ℕ) = \underbrace{P (P ⋯ (P}_{n−1}(ℕ)) ⋯)

where P is the power set operation. Thus we have a sequence of theories

Z_{1} ⊆ Z_{2} ⊆ ⋯ ⊆ Z_{n} ⊆ Z_{n+1} ⊆ · · · .

The union Z_{∞} = ⋃_{n=1}^{∞} Z_{n} is known as simple type theory. This theory is historically important, because it or something like it was offered by Russell as a solution of the Russell Paradox.

5.6 Axiomatic Set Theory

We now turn to another kind of foundational theory, known as axiomatic set theory.

Definition 5.6.1 (the language of set theory). The language of set theory, L_{set}, consists of two binary predicates, ∈ and =, the membership predicate and the identity predicate. The variables u, v, w, x, y, z, … are intended to range over sets. Note that u ∈ x means that u is an element of the set x, i.e., a member of x. We also use notations such as x = {u, v, …} meaning that x is a set whose elements are u, v, …, and x = {u | …} meaning that x is a set whose elements are all u such that ….

Remark 5.6.2 (pure well-founded sets). In order to motivate and clarify our presentation of the axioms of set theory, we first note that the axioms are intended to apply only to sets which are pure and well-founded. A set x is said to be pure if all elements of x are sets, all elements of elements of x are sets, all elements of elements of elements of x are sets, etc. A set x is said to be well-founded if there is no infinite descending ∈-chain

⋯ ∈ u_{n+1} ∈ u_{n} ∈ ⋯ ∈ u_{2} ∈ u_{1} ∈ u_{0} = x.

Remark 5.6.3. In order to state the axioms and theorems of set theory efficiently, we shall tacitly employ the technique of definitional extensions, which has been discussed in Section 5.4.

Definition 5.6.4 (Zermelo set theory). Zermelo set theory with the axiom of choice, ZC, is a theory in the language L_{set} consisting of the following axioms.

1. The axiom of extensionality: ∀x ∀y (x = y ⇔ ∀u (u ∈ x ⇔ u ∈ y)).

We define a binary predicate ⊆ by x ⊆ y ⇔ ∀u (u ∈ x ⇒ u ∈ y), i.e., x is a subset of y. Extensionality^{1} says that x = y is equivalent to x ⊆ y ∧ y ⊆ x.

2. The pairing axiom: ∀x ∀y ∃z ∀u (u ∈ z ⇔ (u = x ∨ u = y)).

By extensionality this z is unique, so we define a binary operation {x, y} = this z. Note that {x, y} is the unordered pair consisting of x and y. In addition, we define a unary operation {x} = {x, x}. Note that {x} is the singleton set consisting of x.

We also define a binary operation (x, y) = {{x}, {x, y}}, the ordered pair consisting of x and y. Using extensionality, we can prove the basic property

∀x ∀y ∀u ∀v ((x, y) = (u, v) ⇔ (x = u ∧ y = v)).

3. The union axiom: ∀x ∃z ∀u (u ∈ z ⇔ ∃v (u ∈ v ∧ v ∈ x)).

By extensionality this z is unique, so we define a unary operation ⋃ x = this z. Note that ⋃ x is the union of x, i.e., the union of all of the sets which are elements of x. We also define a binary operation x∪y = ⋃{x, y}, the union of x and y.

4. The power set axiom: ∀x ∃z ∀y (y ∈ z ⇔ y ⊆ x).

1Recall that L_{set} is a one-sorted language with only set variables. This fact together with the axiom of extensionality embodies our restriction to pure sets. Later we shall introduce another axiom, the axiom of foundation, which embodies our restriction to well-founded sets.

By extensionality this z is unique, so we define a unary operation P (x) = this z. Note that P (x) is the power set of x,

P (x) = {y | y ⊆ x},

the set of all subsets of x.

5. The comprehension scheme: the universal closure of

∀x ∃z ∀u (u ∈ z ⇔ (u ∈ x ∧ A))

where A is any L_{set}-formula in which z does not occur.

The idea here is that x is a given set, and A expresses a property of elements u ∈ x. The comprehension scheme asserts the existence of a set

z = {u ∈ x | A},

i.e., z is a subset of x consisting of all u ∈ x such that A holds. By extensionality, this z is unique.

Note that the comprehension scheme consists of an infinite set of axioms. It can be shown that ZC is not finitely axiomatizable.

Using comprehension, we define binary operations

(a) x ∩ y = {u ∈ x | u ∈ y}, the intersection of x and y,

(b) x \ y = {u ∈ x | u ∉ y}, the set-theoretic difference of x and y, and

(c) x × y = {w ∈ P (P (x ∪ y)) | ∃u ∃v (u ∈ x ∧ v ∈ y ∧ (u, v) = w)}, the Cartesian product of x and y.

We also define a constant ∅ = {} = x \ x, the empty set.

We define a unary predicate Fcn(f) saying that f is a function, i.e., a set f such that

∀w (w ∈ f ⇒ ∃x ∃y (w = (x, y)))

and

∀x ∀y ∀z (((x, y) ∈ f ∧ (x, z) ∈ f) ⇒ y = z).

Using comprehension, the domain and range of f are defined as unary operations

dom(f) = {x ∈ ⋃ ⋃ f | ∃y ((x, y) ∈ f)}

and

ran(f) = {y ∈ ⋃ ⋃ f | ∃x ((x, y) ∈ f)}.

We also define f(x), the value of f at x ∈ dom(f), to be the unique y such that (x, y) ∈ f.

6. The axiom of infinity: ∃z (∅ ∈ z ∧ ∀x ∀y ((x ∈ z ∧ y ∈ z) ⇒ x ∪ {y} ∈ z)).

Using comprehension, we can prove the existence of a unique smallest set z as above, namely the intersection of all such sets. We define a constant HF = this z. Note that HF is an infinite set. The elements of HF are the hereditarily finite sets, i.e., those pure well-founded sets x such that C(x) is finite. Here

C(x) = x ∪ ⋃ x ∪ ⋃ ⋃ x ∪ ⋯,

i.e., C(x) is the set consisting of all elements of x, elements of elements of x, elements of elements of elements of x, ….

Similarly, we can prove that there exists a unique smallest set w such that ∅ ∈ w ∧ ∀x (x ∈ w ⇒ x ∪ {x} ∈ w). We define a constant ω = this w. Note that ω ⊆ HF. The elements of ω are just the natural numbers, inductively identified with hereditarily finite sets via n = {0, 1, …, n − 1}. Thus ω = ℕ, the set of natural numbers, and we have 0 = ∅ and, for all n, n + 1 = n ∪ {n}. We define a finite sequence to be a function f such that dom(f) ∈ ω. We define an infinite sequence to be a function f such that dom(f) = ω.

A set x is said to be finite if

∃n ∃f (n ∈ ω ∧ Fcn(f) ∧ dom(f) = n ∧ ran(f) = x).

We define |x|, the cardinality of x, to be the least such n. We can prove that, for all n ∈ ω, |n| = n. For m, n ∈ ω we define

m + n = |(m × {0}) ∪ (n × {1})|

and m · n = |m × n|. On this basis, we can prove the essential properties of + and · on ω. Moreover, from the definition of ω it follows that

∀x ((x ⊆ ω ∧ 0 ∈ x ∧ ∀n (n ∈ x ⇒ n ∪ {n} ∈ x)) ⇒ x = ω).

Thus we have a copy of the natural number system.

7. The axiom of choice:

∀f ((Fcn(f) ∧ ∀x (x ∈ dom(f) ⇒ f(x) ≠ ∅)) ⇒ ∃g (Fcn(g) ∧ dom(g) = dom(f) ∧ ∀x (x ∈ dom(f) ⇒ g(x) ∈ f(x)))).

The axiom of choice says that, given an indexed family of nonempty sets, there exists a function which chooses one element from each of the sets. There is a history of controversy surrounding this axiom.

8. The axiom of foundation: ∀x (x ≠ ∅ ⇒ ∃u (u ∈ x ∧ u ∩ x = ∅)).

The axiom of foundation amounts to saying that all sets are well-founded. To see this, note that if there were an infinite descending ∈-chain

⋯ ∈ u_{n+1} ∈ u_{n} ∈ ⋯ ∈ u_{2} ∈ u_{1} ∈ u_{0}

then we would have a counterexample to the axiom of foundation, namely x = {u_{0}, u_{1}, …, u_{n}, u_{n+1}, …}. Conversely, if x were a counterexample to the axiom of foundation, i.e., x ≠ ∅ and ∀u (u ∈ x ⇒ u ∩ x ≠ ∅), then we could use the axiom of choice to obtain an infinite descending ∈-chain u_{1} ∈ x, u_{2} ∈ u_{1} ∩ x, u_{3} ∈ u_{2} ∩ x, ….

Remark 5.6.5 (foundational significance of set theory). The significance of ZC and similar theories is that they can serve as an axiomatic, set-theoretical foundation for virtually all of mathematics. As already noted, within ZC we have the natural number system, ℕ. On this basis, it is possible to follow the usual Dedekind construction of the integers ℤ, the rational numbers ℚ, and the real numbers ℝ. We can also develop the theory of higher mathematical objects such as manifolds, topological spaces, operators on Banach spaces, etc., all within (definitional extensions of) ZC.

Definition 5.6.6 (Zermelo/Fraenkel set theory). ZFC, Zermelo/Fraenkel set theory with the axiom of choice, consists of ZC, Zermelo set theory with the axiom of choice, plus

9. The replacement scheme: universal closure of

(∀u (∃ exactly one v) A) ⇒ ∀x ∃y ∀v (v ∈ y ⇔ ∃u (u ∈ x ∧ A))

where A is any L_{set}-formula in which y does not occur.

The idea here is that to each u is associated exactly one v such that A holds. Under this assumption, we assert that for all sets x there exists a set y consisting of all v associated to some u ∈ x. By extensionality, this y is unique.

Note that the replacement scheme consists of an infinite set of axioms. It can be shown that ZFC is not finitely axiomatizable.

Remark 5.6.7 (practical completeness of set theory). The most obvious model of Zermelo set theory is the set

P^{ω}(HF) = ⋃_{n∈ω} P^{n}(HF) = ⋃_{n∈ℕ} \underbrace{P (P ⋯ (P}_{n}(HF)) ⋯)

consisting of HF plus all subsets of HF plus all subsets of subsets of HF plus …. Thus P^{ω}(HF) is the set of all sets of finite order over HF. The axioms of ZC express evident properties of P^{ω}(HF).

The existence of the set P^{ω}(HF) cannot be proved in Zermelo set theory. However, the existence of P^{ω}(HF) can be proved in Zermelo/Fraenkel set theory, as follows. Let A be a formula which associates to each n ∈ ℕ the set P^{n}(HF). Since ℕ is a set, the replacement scheme for A gives us the set {P^{n}(HF) | n ∈ ℕ}, and then the union axiom gives us ⋃{P^{n}(HF) | n ∈ ℕ} = P^{ω}(HF).

The intended model of Zermelo/Fraenkel set theory is the collection V of all pure, well-founded sets. V is also known as the universe of set theory. It can be shown that V = ⋃_{α} P^{α}(HF), where α ranges over transfinite ordinal numbers. Thus V is the collection of all sets of all transfinite orders over HF.

The axioms of ZFC express evident properties of V. Moreover, it has been found that ZFC is “practically complete” in the sense that all L_{set}-sentences expressing evident properties of V are provable in ZFC. At the same time, there are many interesting L_{set}-sentences, e.g., the Continuum Hypothesis, which are neither evidently true nor evidently false in V according to our current understanding, and which are known to be neither provable nor refutable in ZFC. Thus it appears that ZFC accurately reflects our current understanding of V.

5.7 Interpretability

Definition 5.7.1. Let T_{1} and T_{2} be theories. We say that T_{1} is a subtheory of T_{2} if the language of T_{1} is included in the language of T_{2} and the theorems of T_{1} are included in the theorems of T_{2}.

Definition 5.7.2 (interpretability). Let T_{1} and T_{2} be theories. We say that T_{1} is interpretable in T_{2} if T_{1} is a subtheory of some definitional extension of T_{2}. Intuitively, this means that T_{2} is “at least as strong as” T_{1}, in some abstract sense. We sometimes write T_{1} ≤ T_{2} to mean that T_{1} is interpretable in T_{2}.

Remark 5.7.3. It is straightforward to show that the interpretability relation is transitive. In other words, T_{1} ≤ T_{2} and T_{2} ≤ T_{3} imply T_{1} ≤ T_{3}. Thus we have equivalence classes of theories under mutual interpretability, partially ordered by the interpretability relation.

Examples 5.7.4. First-order arithmetic is interpretable in second-order arithmetic, and second-order arithmetic is interpretable in set theory. More generally, for all n ≥ 1, nth-order arithmetic is interpretable in (n + 1)st-order arithmetic and in set theory. It can be shown that (n+1)st-order arithmetic and set theory are not interpretable in nth order arithmetic. In particular, second-order arithmetic is not interpretable in first-order arithmetic. Results of this kind follow from Gödel’s Second Incompleteness Theorem. We have

Z_{1} < Z_{2} < ⋯ < Z_{n} < Z_{n+1} < ⋯ < Z_{∞} < ZC < ZFC

where T_{1} < T_{2} means that T_{1} is “weaker than” T_{2}, i.e., T_{2} is “stronger than” T_{1}, i.e., T_{1} is interpretable in T_{2} and not vice versa.

Remark 5.7.5 (the Gödel hierarchy). The partial ordering of foundational theories under interpretability is sometimes known as the Gödel hierarchy. This hierarchy is of obvious foundational interest.

Remark 5.7.6. The foundational significance of interpretability is highlighted by the following observations. If T_{1} is interpretable in T_{2}, then:

1. Consistency of T_{2} implies consistency of T_{1}.

2. Essential incompleteness of T_{1} implies essential incompleteness of T_{2}.

3. Effective essential incompleteness of T_{1} implies effective essential incompleteness of T_{2}.

5.8 Beth’s Definability Theorem

In this section we consider implicit definitional extensions of theories. We state and prove Beth’s Definability Theorem, which says that an implicit definitional extension of a theory T is always equivalent to an explicit definitional extension of the same theory, T.

We consider only the case of predicates, but operations can be handled similarly. Let T = (L, S) be a theory, and let P be an n-ary predicate of L.

Definition 5.8.1.

1. We say that T explicitly defines P if there exists an L-formula D not involving P with free variables x_{1}, …, x_{n} such that

T ⊢ ∀x_{1} ⋯ ∀x_{n} (P x_{1} ⋯ x_{n} ⇔ D).

2. We say that T implicitly defines P if, letting P′ be a new n-ary predicate and letting T′ = T [P/P′], we have

T ∪ T′ ⊢ ∀x_{1} ⋯ ∀x_{n} (P x_{1} ⋯ x_{n} ⇔ P′x_{1} ⋯ x_{n}).

Theorem 5.8.2 (Beth’s Definability Theorem). T explicitly defines P if and only if T implicitly defines P.

Proof. Assume first that T explicitly defines P, say

T ⊢ ∀x_{1} ⋯ ∀x_{n} (P x_{1} ⋯ x_{n} ⇔ D).

It follows that

T′ ⊢ ∀x_{1} ⋯ ∀x_{n} (P′x_{1} ⋯ x_{n} ⇔ D).

Hence

T ∪ T′ ⊢ ∀x_{1} ⋯ ∀x_{n} (P x_{1} ⋯ x_{n} ⇔ P′x_{1} ⋯ x_{n}),

i.e., T implicitly defines P.

Conversely, assume that T implicitly defines P, i.e.,

T ∪ T′ ⊢ ∀x_{1} ⋯ ∀x_{n} (P x_{1} ⋯ x_{n} ⇔ P′x_{1} ⋯ x_{n}).

By the Compactness Theorem, there are finitely many axioms A_{1}, …, A_{k} ∈ S such that

(A ∧ A′) ⇒ ∀x_{1} ⋯ ∀x_{n} (P x_{1} ⋯ x_{n} ⇔ P′x_{1} ⋯ x_{n})

is logically valid, where A = A_{1} ∧ ⋯ ∧ A_{k} and A′ = A[P/P′]. Introducing parameters a_{1}, …, a_{n}, we see that

(A ∧ A′) ⇒ (P a_{1} ⋯ a_{n} ⇔ P′a_{1} ⋯ a_{n})  (5.1)

is logically valid. It follows quasitautologically that

(A ∧ P a_{1} ⋯ a_{n}) ⇒ (A′ ⇒ P′a_{1} ⋯ a_{n})  (5.2)

is logically valid. By the Interpolation Theorem 3.5.1, we can find an L-formula D with free variables x_{1}, …, x_{n} such that D[x_{1}/a_{1}, …, x_{n}/a_{n}] is an interpolant for (5.2). Thus

(A ∧ P a_{1} ⋯ a_{n}) ⇒ D[x_{1}/a_{1}, …, x_{n}/a_{n}]  (5.3)

and

D[x_{1}/a_{1}, …, x_{n}/a_{n}] ⇒ (A′ ⇒ P′a_{1} ⋯ a_{n})  (5.4)

are logically valid, and P and P′ do not occur in D. Since (5.4) is logically valid, it follows that

D[x_{1}/a_{1}, …, x_{n}/a_{n}] ⇒ (A ⇒ P a_{1} ⋯ a_{n})  (5.5)

is logically valid. From the logical validity of (5.3) and (5.5), it follows quasitautologically that

A ⇒ (P a_{1} ⋯ a_{n} ⇔ D[x_{1}/a_{1}, …, x_{n}/a_{n}])  (5.6)

is logically valid. Hence

A ⇒ ∀x_{1} ⋯ ∀x_{n} (P x_{1} ⋯ x_{n} ⇔ D)

is logically valid, so

T ⊢ ∀x_{1} ⋯ ∀x_{n} (P x_{1} ⋯ x_{n} ⇔ D).

Thus we see that T explicitly defines P. □

Arithmetization of Predicate Calculus

6.1 Primitive Recursive Arithmetic

Definition 6.1.1. To each natural number n we associate a variable-free PRAterm \underline{n} as follows: \underline{0} = 0, \underline{n + 1} = \underline{S} \underline{n}. Thus

\underline{n} = \underbrace{\underline{S} ⋯ \underline{S}}_{n} 0.

These terms are known as numerals.

Theorem 6.1.2. Let f be a k-ary primitive recursive function. Then for all k-tuples of natural numbers m_{1}, …, m_{k} we have

PRA ⊢ \underline{f} \underline{m_{1}} ⋯ \underline{m_{k}} = \underline{f(m_{1}, …, m_{k})} .

Proof. □

6.2 Interpretability of PRA in Z_{1}

6.3 Gödel Numbers

Let L be a countable language. Assume that to all the sorts σ, predicates P, and operations f of L have been assigned distinct positive integers #(σ), #(P), #(f) respectively. As usual, let V be the set of parameters.

Definition 6.3.1 (Gödel numbers). To each L-V -term t and L-V -formula A we assign a positive integer, the Gödel number of t or of A, denoted #(t) or #(A), respectively.

#(v_{i}^{σ})  = 2 · 3^{#(σ)} · 5^{i}
#(a_{i}^{σ})  = 2^{2} · 3^{#(σ)} · 5^{i}
#(ft_{1} ⋯ t_{n}) = 2^{3} · 3^{#(f)} · p_{2}^{#(t_{1})} ⋯ p_{n+1}^{#(t_{n})} if f is an n-ary operation
#(P t_{1} ⋯ t_{n}) = 2^{4} · 3^{#(P)} · p_{2}^{#(t_{1})} ⋯ p_{n+1}^{#(t_{n})} if P is an n-ary predicate
#(¬ A)  = 2^{5} · 3^{#(A)}
#(A ∧ B)  = 2^{6} · 3^{#(A)} · 5^{#(B)}
#(A ∨ B)  = 2^{7} · 3^{#(A)} · 5^{#(B)}
#(A ⇒ B)  = 2^{8} · 3^{#(A)} · 5^{#(B)}
#(A ⇔ B)  = 2^{9} · 3^{#(A)} · 5^{#(B)}
#(∀v A)  = 2^{10} · 3^{#(v)} · 5^{#(A)}
#(∃v A)  = 2^{11} · 3^{#(v)} · 5^{#(A)}

Definition 6.3.2. The language L is said to be primitive recursive if the following items are primitive recursive.

Sort(x)  ≡ x = #(σ) for some sort σ
Pred(x)  ≡ x = #(P) for some predicate P
Op(x)  ≡ x = #(f) for some operation f
arity(#(P)) = n  if P is an n-ary predicate
arity(#(f)) = n  if f is an n-ary operation
sort(#(P), i) = #(σ_{i})  if 1 ≤ i ≤ n and P is an n-ary predicate of
type (σ_{1}, …, σ_{n})
sort(#(f), i) = #(σ_{i})  if 1 ≤ i ≤ n and sort(#(f)) = #(τ) and f is an n-ary operation
of type (σ_{1}, …, σ_{n}, τ).

Lemma 6.3.3. If L is primitive recursive, then the following are primitive recursive.

Var(x)  ≡ x = #(v) for some variable v
Param(x) ≡ x = #(a) for some parameter a
Term(x)  ≡ x = #(t) for some term t
ClTerm(x) ≡ x = #(t) for some closed term t
AtFml(x) ≡ x = #(A) for some atomic formula A
Fml(x)  ≡ x = #(A) for some formula A
sort(#(t)) = #(σ)  if t is a term of sort σ

Proof. We have

Var(x) ≡ (x)_{0} = 1 ∧ x = 2^{(x)_{0}} · 3^{(x)_{1}} · 5^{(x)_{2}} ∧ Sort((x)_{1})

and

Param(x) ≡ (x)_{0} = 2 ∧ x = 2^{(x)_{0}} · 3^{(x)_{1}} · 5^{(x)_{2}} ∧ Sort((x)_{1}) .

To show that the predicate Term(x) is primitive recursive, we first show that the function sort(x) is primitive recursive, where sort(#(t)) = #(σ) if t is a term of sort σ, sort(x) = 0 otherwise. Put lh(x) = least w < x such that (x)_{w} = 0. We then have

sort(x) = \{ \begin{matrix}(x)_{1} & if Var(x) ∨ Param(x) , \\ sort((x)_{1}, lh(x) · − 1) & if (x)_{0} = 3 ∧ Op((x)_{1}) ∧ (+) , \\ 0 & otherwise , \end{matrix}

where

(+)  arity((x)_{1}) = lh(x) · − 2 ∧ x = ∏_{i=0}^{lh(x) ·_{−}1} p_{i}^{(x)_{i}}
∧ (∀i < lh(x) · − 2) (sort((x)_{i+2}) = sort((x)_{1}, i + 1)) .

Then

Term(x) ≡ sort(x) > 0 .

For closed terms, define clsort(x) like sort(x) replacing Var(x) ∨ Param(x) by Param(x). We then have

ClTerm(x) ≡ clsort(x) > 0 .

For formulas we have

AtFml(x) ≡ ((x)_{0} = 4 ∧ Pred((x)_{1}) ∧ (+))

and Fml(x) ≡ AtFml(x) ∨ ((x)_{0} = 5 ∧ x = 2^{(x)_{0}} · 3^{(x)_{1}} ∧ Fml((x)_{1}))

∨ (6 ≤ (x)_{0} ≤ 9 ∧ x = 2^{(x)_{0}} · 3^{(x)_{1}} · 5^{(x)_{2}} ∧ Fml((x)_{1}) ∧ Fml((x)_{2}))

∨ (10 ≤ (x)_{0} ≤ 11 ∧ x = 2^{(x)_{0}} · 3^{(x)_{1}} · 5^{(x)_{2}} ∧ Var((x)_{1}) ∧ Fml((x)_{2}))

and this completes the proof. □

Lemma 6.3.4 (substitution). There is a primitive recursive function sub(x, y, z) such that for any formula A and any variable v and any closed term t,

sub(#(A), #(v), #(t)) = #(A[v/t]) .

Proof.

sub(x, y, z) = \{ \begin{matrix}z & if x = y, \\ 2^{(x)_{0}} · 3^{(x)_{1}} · ∏_{i=2}^{lh(x) ·_{−}1} p_{i}^{sub((x)_{i},y,z)} & if 3 ≤ (x)_{0} ≤ 4, \\ 2^{(x)_{0}} · 3^{sub((x)_{1},y,z)} & if (x)_{0} = 5, \\ 2^{(x)_{0}} · 3^{sub((x)_{1},y,z)} · 5^{sub((x)_{2},y,z)} & if 6 ≤ (x)_{0} ≤ 9, \\ 2^{(x)_{0}} · 3^{(x)_{1}} · 5^{sub((x)_{2},y,z)} & if 10 ≤ (x)_{0} ≤ 11 ∧ (x)_{1} ≠ y, \\ x & otherwise. \end{matrix}

□

Lemma 6.3.5. If L is primitive recursive, then the predicate

Snt(x) ≡ x = #(A) for some sentence A

is primitive recursive.

Proof. Recall that, by Exercise 2.1.10, a formula A is a sentence if and only if A[v/a] = A for all variables v occurring in A. Note also that if y = #(v_{i}^{σ}) then 2y = #(a_{i}^{σ}). Thus we have

Snt(x) ≡ Fml(x) ∧ (∀y < x) (Var(y) ⇒ x = sub(x, y, 2y)) .
□

Lemma 6.3.6. There is a primitive recursive function num(x) such that

num(n) = #(\underline{n})

for any nonnegative integer n.

Proof. The recursion equations for num(x) are

num(0) = #(\underline{0}) ,
num(x + 1) = 2^{3} · 3^{#(\underline{S})} · 5^{num(x)} .
□

6.4 Undefinability of Truth

In this section, let T be a theory which includes PRA. For example, we could take T to be PRA itself. Or, by Section 6.2, we could take T to be an appropriate definitional extension of Z_{1} or Z_{2} or ZFC.

Lemma 6.4.1 (Self-Reference Lemma). Let L be the language of T. Let A be an L-formula with a free number variable x. Then we can find an L-formula B such that

T ⊢ B ⇔ A[x/\underline{#(B)} ] .

The free variables of B are those of A except for x. In particular, if x is the only free variable of A, then B is an L-sentence.

Proof. Put d(z) = sub(z, #(x), num(z)). Thus d is a 1-ary primitive recursive function such that, if A is any L-formula containing the number variable x as a free variable, then d(#(A)) = #(A[x/\underline{#(A)} ]. Now given A as in the hypothesis of the lemma, let D be the formula A[x/\underline{d} x], and let B be the formula A[x/\underline{d} \underline{#(D)} ], i.e., D[x/\underline{#(D)} ]. Note that d(#(D)) = #(B). It follows by Theorem 6.1.2 that PRA ⊢ \underline{d} \underline{#(D)} = \underline{#(B)}. Since T includes PRA, it follows that T ⊢ \underline{d} \underline{#(D)} = \underline{#(B)}. Hence T ⊢ A[x/\underline{d} \underline{#(D)}] ⇔ A[x/\underline{#(B)} ]. In other words, T ⊢ B ⇔ A[x/\underline{#(B)} ]. This completes the proof. □

Definition 6.4.2. If M is any model of T, let True_{M} be the set of Gödel numbers of sentences that are true in M, i.e.,

True_{M} = {#(B) | B is a sentence and M ⊧ B}.

Definition 6.4.3. An ω-model of T is a model M of T such that the number domain of M is ω = {0, 1, 2, …} and 0_{M} = 0 and S_{M}(n) = n + 1 for all n ∈ ω. More generally, if M is any model of T, we may assume that ω is identified with a subset of the number domain of M in such a way that 0_{M} = 0 and S_{M}(n) = n + 1 for each n ∈ ω. Thus each n ∈ ω is identified with the element of M that is denoted by \underline{n}, i.e., n = v_{M}(\underline{n}).

Theorem 6.4.4 (undefinability of truth). If M is an ω-model of T, then True_{M} is not explicitly definable over M. More generally, if M is any model of T, then the characteristic function of True_{M} is is not included in the characteristic function of any subset of M that is explicitly definable over M.

Proof. Let X be a subset of the number domain of M which is explicitly definable over M. Let A be an L-formula with a free number variable x and no other free variables, such that A explicitly defines X over M. Applying Lemma 6.4.1 to the negation of A, we obtain an L-sentence B such that T ⊢ B ⇔ ¬ A[x/\underline{#(B)} ]. Since M is a model of T, it follows that #(B) ∈ True_{M} if and only if #(B) ∉ X. Hence the characteristic function of True_{M} is not included in the characteristic function of X, q.e.d. □

Corollary 6.4.5. Let M = (ω, +, ·, 0, 1, =) be the standard model of first-order arithmetic, Z_{1}. Then True_{M} is not explicitly definable over M. This^{1} may be paraphrased by saying that arithmetical truth is not arithmetically definable.

Remark 6.4.6. With M = (ω, +, ·, 0, 1, =) as above, it can be shown that True_{M} is implicitly definable over M. (See also Exercise 6.4.7.) Thus the Beth’s Definability Theorem does not hold for definability over this particular model.

Exercise 6.4.7. Let M be an ω-model of Z_{1} or Z_{2} or ZFC. Let Sat_{M} be the satisfaction relation on M. Show that Sat_{M} is implicitly definable over M.

6.5 The Provability Predicate

In this section, let L be a primitive recursive language, and let T be an Ltheory which is primitive recursively axiomatizable. For example, T could be PRA itself, or T could be any of the mathematical or foundational theories discussed in Sections 5.2, 5.5, 5.6.

Definition 6.5.1. Choose a primitive recursive predicate Ax_{T} for the set of Gödel numbers of axioms of T. In terms of Ax_{T} show that various predicates associated with T are primitive recursive. Introduce the provability predicate Pvbl_{T} by definition:

1This result is due to Tarski [5].

Pvbl_{T} (x) ⇔ ∃y Prf_{T} (x, y) .

Note that, for all L-sentences B, Pvbl_{T} (\underline{#(B)}) is true if and only if T ⊢ B.

Lemma 6.5.2 (derivability condition 1). For any L-sentence A, if T ⊢ A then

PRA ⊢ Pvbl_{T} (\underline{#(A)}) .

Proof. Suppose T ⊢ A. Let p be a proof of A in T. Then Prf_{T} (#(A), #(p)) holds. Since Prf_{T} (x, y) is a primitive recursive predicate, it follows by Theorem 6.1.2 that PRA ⊢ Prf_{T} (\underline{#(A)}, \underline{#(p)}). Hence PRA ⊢ Pvbl_{T} (\underline{#(A)}), q.e.d. □

Lemma 6.5.3 (derivability condition 2). For any L-sentence A, we have

PRA ⊢ Pvbl_{T} (\underline{#(A)}) ⇒ Pvbl_{PRA}(\underline{#(Pvbl_{T} (\underline{#(A)}))}) .

Proof. This is just Lemma 6.5.2 formalized in PRA. The details of the formalization are in Section 6.7. □

Lemma 6.5.4 (derivability condition 3). For any L-sentences A and B, we have

PRA ⊢ Pvbl_{T} (\underline{#(A ⇒ B)}) ⇒ (Pvbl_{T} (\underline{#(A)}) ⇒ Pvbl_{T} (\underline{#(B)})) .

Proof. This is a straightforward consequence of the fact that our rules of inference include modus ponens. □

6.6 The Incompleteness Theorems

In this section, let T be a theory which is primitive recursively axiomatizable and includes PRA. For example, T could be PRA itself, or it could be an appropriate definitional extension of Z_{1} or Z_{2} or ZFC. As in Section 6.5, let Pvbl_{T} be a provability predicate for T.

Lemma 6.6.1. Let A(x) be a PRA-formula with one free variable x. Then we can find a PRA-sentence B such that PRA ⊢ B ⇔ A(\underline{#(B)}).

Proof. This is the Self-Reference Lemma 6.4.1 specialized to PRA. □

Lemma 6.6.2. We can find a PRA-sentence S such that

PRA ⊢ S ⇔ ¬ Pvbl_{T} (\underline{#(S)}) .  (6.1)

Note that S is self-referential and says “I am not provable in T.”

Proof. This is an instance of Lemma 6.6.1 with A(x) ≡ ¬ Pvbl_{T} (x). □

Lemma 6.6.3. Let S be as in Lemma 6.6.2. If T is consistent, then T ⊬ S.

Proof. Suppose for a contradiction that T ⊢ S. By Lemma 6.5.2 we have PRA ⊢ Pvbl_{T} (\underline{#(S)}). Hence by (6.1) it follows that PRA ⊢ ¬ S. Since T includes PRA, we have T ⊢ ¬ S. Thus T is inconsistent. □

Theorem 6.6.4 (the First Incompleteness Theorem). If T is consistent, then we can find a sentence S′ in the language of first-order arithmetic such that S′ is true yet S′ is not a theorem of T.

Proof. Let S be a PRA-sentence as in Lemma 6.6.2. By Lemma 6.6.3, T ⊬ S. It follows by (6.1) that S is true. As in Section 6.2, let S′ be the translation of S into the language of first-order arithmetic. Thus S′ is also true. By the results of Section 6.2, PRA ⊢ S ⇔ S′. Hence T ⊢ S ⇔ S′. Hence T ⊬ S′. □

Assume now that the primitive recursive predicate Ax_{T} has been chosen in such a way that PRA ⊢ ∀x (Ax_{PRA}(x) ⇒ Ax_{T} (x)). It follows that PRA ⊢ ∀x (Pvbl_{PRA}(x) ⇒ Pvbl_{T} (x)). In particular we have:

Lemma 6.6.5. For all PRA-sentences A, we have

PRA ⊢ Pvbl_{PRA}(\underline{#(A)}) ⇒ Pvbl_{T} (\underline{#(A)}) .

Definition 6.6.6. Con_{T} is defined to be the sentence ¬ Pvbl_{T} (\underline{#(0 ≠ 0)}). Note that Con_{T} is a PRA-sentence which asserts the consistency of T.

Theorem 6.6.7 (the Second Incompleteness Theorem). If T is consistent, then T ⊬ Con_{T}.

Proof. Let S be as in Lemma 6.6.2. By Theorem 6.6.4 we have T ⊬ S. Therefore, to show T ⊬ Con_{T}, it suffices to show T ⊢ Con_{T} ⇒ S. Since T includes PRA, it suffices to show PRA ⊢ Con_{T} ⇒ S. By (6.1) it suffices to show

PRA ⊢ Con_{T} ⇒ ¬ Pvbl_{T} (\underline{#(S)}) .  (6.2)

But this is just Lemma 6.6.3 formalized in PRA.

Details: We need to prove (6.2). Reasoning in PRA, suppose Pvbl_{T} (\underline{#(S)}). By Lemma 6.5.3 we have Pvbl_{PRA}(\underline{#(Pvbl_{T} (\underline{#(S)}))}). Moreover, from (6.1) and Lemma 6.5.2 we have Pvbl_{PRA}(\underline{#(S ⇔ ¬ Pvbl_{T} (\underline{#(S)}))}). Hence by Lemmas 6.5.2 and 6.5.4 we have Pvbl_{PRA}(\underline{#(¬ S)}). By Lemma 6.6.5 it follows that Pvbl_{T} (\underline{#(¬ S)}). Hence by Lemmas 6.5.2 and 6.5.4 we have Pvbl_{T} (\underline{#(0 ≠ 0)}), i.e., ¬ Con_{T}. This completes the proof. □

Exercise 6.6.8. Show that PRA ⊢ S ⇔ Con_{T}.

Exercise 6.6.9 (Rosser’s Theorem). Show that if T is as in Theorems 6.6.4 and 6.6.7, then T is incomplete.

Hint: Use the Self-Reference Lemma 6.4.1 to obtain a sentence B such that PRA ⊢ B ⇔ A[x/\underline{#(B)}], where A[x/\underline{#(B)}] says that for any proof p of B in T there exists a proof q of ¬ B in T such that #(q) < #(p). Using the assumption that T is consistent, show that T ⊬ B and T ⊬ ¬ B.

Exercise 6.6.10. Give an example of a T as in Theorems 6.6.4 and 6.6.7 such that T ⊢ ¬ Con_{T}.

Solution. We may take T = PRA + ¬ Con_{PRA}, or T = Z_{1} + ¬ Con_{Z_{1}}, etc.

6.7 Proof of Lemma 6.5.3

FIXME Write this section!

Bibliography

[1] Neil D. Jones and Alan L. Selman. Turing machines and the spectra of first-order formulas. Journal of Symbolic Logic, 39:139–150, 1974.

[2] David Marker. Model Theory: An Introduction. Springer, 2002. VIII + 342 pages.

[3] Stephen G. Simpson. Subsystems of Second Order Arithmetic. Perspectives in Mathematical Logic. Springer-Verlag, 1999. XIV + 445 pages.

[4] Raymond M. Smullyan. First-Order Logic. Dover Publications, New York, 1995. XII + 158 pages.

[5] Alfred Tarski. Introduction to Logic and to the Methodology of Deductive Sciences. Oxford University Press, 4th edition, 1994. XXII + 229 pages.

Index

Abelian group, 89 ACF, 93 ACF_{0}, 94 ACF_{p}, 94 Algebra, Fundamental Theorem of, 93 algebraically closed field, 93 antisymmetry, 22 arithmetic

first-order, 103 second-order, 104 nth order, 106

arity, 24, 78, 84 assignment, 6 associativity, 10, 30, 104 atomically closed, 43 atomic formula, 3, 24, 79, 85 automorphism, 98 axiom of choice, 109 axiom of foundation, 109

Beth’s Definability Theorem, 100, 112,

118 binary, 3 block tableau, 61

modified, 66 bound variable, 25

ℂ (complex numbers), 93 Cartesian product, 108 categoricity, 88, 89 characteristic, 93 choice, 109 Church’s Theorem, 52 clause, 11 closed, 15, 40

atomically, 43 cofinite, 76 commutativity, 10, 89, 92 Compactness Theorem, 72 companion, 51, 52 completeness, 19, 43, 51, 58, 64, 66, 81,

85 practical, 103–105, 111

complete theories, 88–92, 94–96, 103 complex numbers, 93 composite number, 77 comprehension, 105, 108 congruence, 71, 72 consequence

logical, 8, 10, 27, 35, 40, 60, 87 quasitautological, 57, 58

conservative extension, 102 consistency, 87 constant, 78

DAG_{0}, 90 Dedekind, 110 definability, 97 definitional extension, 100, 102 degree, 3, 24 dense linear ordering, 91 difference, 108 differential equations, 99 disjunctive normal form, 11 distance, 91 distributivity, 10, 92, 104 divisible group, 90 DLO, 91 dom, 108 domain, 26, 85, 108 dyadic, 20

element, 107 elementary equivalence, 27, 88 elimination of quantifiers, 95 empty set, 108 end node, 20 end points, 91 equality, 82 equivalence relation, 76 e^{x}, 99 explicit definability, 97, 112 exponential function, 97 extensionality, 107

falsity, 27 Fcn, 108 Fibonacci numbers, 78 field, 93 finite, 109 finitely branching, 20 first-order arithmetic, 103 formation sequence, 4 formation tree, 4 formula, 3, 24, 79, 85 foundation, axiom of, 109 foundational theories, 88, 102–111 free variable, 25 function, 79, 85, 108 Fundamental Theorem of Algebra, 93

Gentzen-style proof system, 63 Gödel number, 114 Gödel hierarchy, 111 graph, 22, 70, 91 group, 83

Hilbert-style proof system, 50 Hintikka’s Lemma, 19, 41

identity, 71, 85 identity axioms, 71, 82, 85 identity predicate, 71, 85 immediate extension, 12, 35 immediate predecessor, 20 immediate successor, 20 implicit definability, 98, 112 induction, 103 infinity, 109 integers, 93, 97 intended model, 88, 104–106, 110 interpolation, 66, 69 interpretability, 111 intersection, 108 invariance, 98 irreflexivity, 75 isomorphism, 26, 79

König’s Lemma, 20

L_{1}, 103 L_{2}, 104 language, 3, 24, 78

primitive recursive, 115 LG, 63, 81, 85 LG^{+}, 64 LG′, 66 LG(atomic), 66 LG(symmetric), 67 LH , 56, 81, 85 LH (S), 60 LH′, 59 linear ordering, 91 logical consequence, 8, 10, 27, 35, 40,

60, 87 logical equivalence, 10, 37 logical validity, 8, 27, 35, 37, 64, 67

many-sorted, 84

mathematical theories, 88–96 membership, 45, 104–106 mixed type, 94, 104 modus ponens, 51

ℕ (natural numbers), 97, 104

\underline{n}, 114

n-ary function, 79, 85 n-ary operation, 78, 84 n-ary predicate, 24, 84 n-ary relation, 26, 85 natural numbers, 97, 104 normal satisfiability, 72, 82 normal structure, 71, 82, 86 nth-order arithmetic, 106 numeral, 114

∅ (empty set), 108 one-sorted, 86 open, 15, 18, 40 operation, 78, 84 ordered field, 95 ordered pair, 107 ordering

linear, 91 partial, 22

P (power set), 108 PA, 103 padding, 64 pair

ordered, 107 unordered, 107

pairing, 107 parameter, 31, 85 partial ordering, 22 partition, 76 path, 20 Peano arithmetic, 103 power set, 105–108 practical completeness, 103–105, 111 predecessor, 20 predicate, 24, 84 prenex form, 39 prime numbers, 77 primitive recursive language, 115 product, Cartesian, 108 proof system, 50

Gentzen-style, 63 Hilbert-style, 50

pure set, 107

Q, 103 ℚ (rational numbers), 93 quantifier, 24 quantifier-free, 39 quantifier elimination, 95 quasitautological consequence, 57, 58 quasitautology, 51, 53, 56 quasiuniversal, 43

ℝ (real numbers), 93, 95, 97–99 ran, 108 random graph, 92 range, 108 rational numbers, 93 RCOF, 95 real-closed field, 95 real numbers, 93, 95, 98, 99 reduct, 74, 101 reflexivity, 71 relation, 26, 85 replacement, 110 replacement of bound variables, 38 replete, 18, 40 ring, 83, 92 root, 20

S (successor function), 104 satisfaction, 8, 27, 35 satisfiability, 8, 27, 28, 35, 37 scalar, 94 second-order arithmetic, 104 sentence, 25, 26 sequent, 62 sequent calculus, 63 set theory, 106, 107, 110 signed formula, 12 signed sequent, 67 signed variant, 67 simple type theory, 106 singleton, 107 sin x, 99 sort, 84 soundness, 51 spectrum, 75, 82, 86 strength, 111 structure, 26, 35 sub, 116 subtheory, 111 subtree, 20 successor, 20 successor function, 104 symmetric, 67 symmetry, 71

tableau, 12, 15, 31, 80 Tarski, 95, 118 tautology, 8, 51 term, 78, 84 theories, 87

complete, 88–92, 94–96, 103 foundational, 88, 102–111 mathematical, 88–96 practically complete, 103–105, 111

torsion, 83, 90 transitivity, 71 tree, 20 truth, 27 truth values, 6 type theory, 106

⋃ (union), 107 unary, 3 union, 107 universal closure, 40 universe, 26, 85, 110 unordered pair, 107 unsigned formula, 12 unsigned sequent, 67

valuation, 6, 26, 79 value, 108 variable, 24, 84

bound, 25 free, 25

variable-free, 79 variant, 39, 67 Vaught’s Test, 89 vector space, 94

weakening, 64 well-founded set, 107

ℤ (integers), 93 Z_{1}, 103 Z_{2}, 104 Z_{n}, 106 Z_{∞}, 106 ZC, 107 ZFC, 110 Zermelo, 107 Zermelo/Fraenkel, 110