- •Contents
- •Preface to the Fifth Edition
- •1 Enumerability
- •1.1 Enumerability
- •1.2 Enumerable Sets
- •Problems
- •2 Diagonalization
- •Problems
- •3 Turing Computability
- •Problems
- •4 Uncomputability
- •4.1 The Halting Problem
- •4.2* The Productivity Function
- •Problems
- •5 Abacus Computability
- •5.1 Abacus Machines
- •5.2 Simulating Abacus Machines by Turing Machines
- •5.3 The Scope of Abacus Computability
- •Problems
- •6 Recursive Functions
- •6.1 Primitive Recursive Functions
- •6.2 Minimization
- •Problems
- •7 Recursive Sets and Relations
- •7.1 Recursive Relations
- •7.2 Semirecursive Relations
- •7.3* Further Examples
- •Problems
- •8.1 Coding Turing Computations
- •8.2 Universal Turing Machines
- •8.3∗ Recursively Enumerable Sets
- •Problems
- •9.1 First-Order Logic
- •9.2 Syntax
- •Problems
- •10.1 Semantics
- •10.2 Metalogical Notions
- •Problems
- •11 The Undecidability of First-Order Logic
- •11.1 Logic and Turing Machines
- •11.2 Logic and Primitive Recursive Functions
- •11.3 Lemma
- •Problems
- •12 Models
- •12.1 The Size and Number of Models
- •12.2 Equivalence Relations
- •Problems
- •13 The Existence of Models
- •13.1 Outline of the Proof
- •13.2 The First Stage of the Proof
- •13.3 The Second Stage of the Proof
- •13.4 The Third Stage of the Proof
- •13.5* Nonenumerable Languages
- •Problems
- •14 Proofs and Completeness
- •14.1 Sequent Calculus
- •14.2 Soundness and Completeness
- •14.3* Other Proof Procedures and Hilbert’s Thesis
- •Problems
- •15 Arithmetization
- •15.1 Arithmetization of Syntax
- •Problems
- •16 Representability of Recursive Functions
- •16.2 Minimal Arithmetic and Representability
- •16.3 Mathematical Induction
- •16.4* Robinson Arithmetic
- •Problems
- •17.1 The Diagonal Lemma and the Limitative Theorems
- •17.2 Undecidable Sentences
- •17.3* Undecidable Sentences without the Diagonal Lemma
- •Problems
- •18 The Unprovability of Consistency
- •Historical Remarks
- •19 Normal Forms
- •19.1 Disjunctive and Prenex Normal Forms
- •19.2 Skolem Normal Form
- •19.3 Herbrand’s Theorem
- •19.4 Eliminating Function Symbols and Identity
- •Problems
- •20 The Craig Interpolation Theorem
- •20.1 Craig’s Theorem and Its Proof
- •20.2 Robinson’s Joint Consistency Theorem
- •20.3 Beth’s Definability Theorem
- •Problems
- •21 Monadic and Dyadic Logic
- •21.1 Solvable and Unsolvable Decision Problems
- •21.2 Monadic Logic
- •21.3 Dyadic Logic
- •Problems
- •22 Second-Order Logic
- •Problems
- •23.2 Arithmetical Definability and Forcing
- •Problems
- •24 Decidability of Arithmetic without Multiplication
- •Problems
- •25 Nonstandard Models
- •25.1 Order in Nonstandard Models
- •25.2 Operations in Nonstandard Models
- •25.3 Nonstandard Models of Analysis
- •Problems
- •26 Ramsey’s Theorem
- •Problems
- •27 Modal Logic and Provability
- •27.1 Modal Logic
- •27.2 The Logic of Provability
- •27.3 The Fixed Point and Normal Form Theorems
- •Problems
- •Annotated Bibliography
- •General Reference Works
- •Textbooks and Monographs
- •By the Authors
- •Index
268 |
THE CRAIG INTERPOLATION THEOREM |
by γ . Let A(A ) be the conjunction of the members of T0 (T0 ). Then (1) is implied by
A & A Let c0, . . . , ck be constants not occurring in T T , and hence not in A, A ,
—α, x0, . . . , xk —, or —α , x0, . . . , xk —. Then
—α, c0, . . . , ck — ↔ —α , c0, . . . , ck —
is a consequence of (1) and therefore of A & A . Here of course by —α, c0, . . . , ck — is meant the result of substituting ci for xi in —α, x0, . . . , xk —for all i, and similarly for —α , c0, . . . , ck —. It follows that
|
(A & A ) → (—α, c0, . . . , ck — ↔ —α , c0, . . . , ck —) |
is valid, and hence that |
|
(4) |
A & —α, c0, . . . , ck — |
implies |
|
(5) |
A → —α , c0, . . . , ck —. |
We now apply the Craig interpolation lemma. It tells us that there is a sentence B(c0, . . . , ck ) implied by (4) and implying (5), such that the nonlogical symbols of B are common to (4) and (5). This means that they can include only the ci , which we have displayed, and the βi . Since (4) implies B(c0, . . . , ck ), A and therefore T implies
—α, c0, . . . , ck — → B(c0, . . . , ck )
and since the ci do not occur in T , this means T implies
(6) |
x0 · · · xk (—α, x0, . . . , xk — → B(x0, . . . , xk )). |
Since B(c0, . . . , ck ) implies (5), A and therefore T implies
B(c0, . . . , ck ) → —α , c0, . . . , ck —
and since the ci do not occur in T , this means T implies
|
x0 · · · xk (B(x0, . . . , xk ) → —α , x0, . . . , xk —). |
Replacing each symbol γ by γ , it follows that T implies |
|
(7) |
x0 · · · xk (B(x0, . . . , xk ) → —α, x0, . . . , xk —). |
But (6) and (7) together imply, and therefore T implies, the explicit definition
x0 · · · xk (—α, x0, . . . , xk — ↔ B(x0, . . . , xk )).
Thus, α is explicitly definable from the βi in T , and Beth’s theorem is proved.
Problems
20.1(Lyndon’s interpolation theorem) Let A and C be sentences without constants or function symbols and in negation-normal form. We say that an occurrence of a predicate in such a sentence is positive if it is not preceded by , and negative
PROBLEMS |
269 |
if it is preceded by . Show that if A implies C, and neither A nor C is valid, then there is another such sentence B such that: (i) A implies B; (ii) B implies C; (iii) any predicate occurs positively in B only if it occurs positively in both A and C, and occurs negatively in B if and only if it occurs negatively in both
Aand C.
20.2Give an example to show that Lyndon’s theorem does not hold if constants are present.
20.3(Kant’s theorem on the indefinability of chirality). For points in the plane, we say y is between x and z if the three points lie on a straight line and y is between x and z on that line. We say w and x and y and z are equidistant if the distance from w to x and the distance from y to z are the same. We say x and y and z form a right-handed triple if no two distances between different pairs of them are the same, and traversing the shortest side, then the middle side, then the longest side of the triangle having them as vertices takes one around the triangle clockwise, as on the right in Figure 20-1.
Figure 20-1. Right and left handed triangles.
Show that right-handedness cannot be defined in terms of betweenness and equidistance. (More formally, consider the language with a three-place predicate P, a four-place predicate Q, and a three-place predicate R; consider the interpretation whose domain is the set of the points in the plane and that assigns betweenness and equidistance and right-handedness as the denotations of P and Q and R; and finally consider the theory T whose theorems are all the sentences of the language that come out true under this interpretation. Show that R is not definable in terms of P and Q in this theory.)