Introduction XIII
Notation XVI
1 Propositional Logic 1
1.1 Boolean Functions and Formulas . . . . . . . . . . . . . . . . . . . . 2
1.2 Semantic Equivalence and Normal Forms . . . . . . . . . . . . . . . . 9
1.3 Tautologies and Logical Consequence . . . . . . . . . . . . . . . . . . 14
1.4 A Complete Calculus for . . . . . . . . . . . . . . . . . . . . . . . . 18
1.5 Applications of the Compactness Theorem . . . . . . . . . . . . . . . 25
1.6 Hilbert Calculi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2 Predicate Logic 33
2.1 Mathematical Structures . . . . . . . . . . . . . . . . . . . . . . . . . 34
2.2 Syntax of Elementary Languages . . . . . . . . . . . . . . . . . . . . 43
2.3 Semantics of Elementary Languages . . . . . . . . . . . . . . . . . . . 49
2.4 General Validity and Logical Equivalence . . . . . . . . . . . . . . . . 58
2.5 Logical Consequence and Theories . . . . . . . . . . . . . . . . . . . . 62
2.6 Explicit Definitions—Expanding Languages . . . . . . . . . . . . . . 67
3 G¨odel’s Completeness Theorem 71
3.1 A Calculus of Natural Deduction . . . . . . . . . . . . . . . . . . . . 72
3.2 The Completeness Proof . . . . . . . . . . . . . . . . . . . . . . . . . 76
3.3 First Applications—Nonstandard Models . . . . . . . . . . . . . . . . 81
3.4 ZFC and Skolem’s Paradox . . . . . . . . . . . . . . . . . . . . . . . . 87
3.5 Enumerability and Decidability . . . . . . . . . . . . . . . . . . . . . 92
3.6 Complete Hilbert Calculi . . . . . . . . . . . . . . . . . . . . . . . . . 95
3.7 First-Order Fragments and Extensions . . . . . . . . . . . . . . . . . 99
IX
X Contents
4 The Foundations of Logic Programming 105
4.1 Term Models and Horn Formulas . . . . . . . . . . . . . . . . . . . . 106
4.2 Propositional Resolution . . . . . . . . . . . . . . . . . . . . . . . . . 112
4.3 Unification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119
4.4 Logic Programming . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122
4.5 Proof of the Main Theorem . . . . . . . . . . . . . . . . . . . . . . . 129
5 Elements of Model Theory 131
5.1 Elementary Extensions . . . . . . . . . . . . . . . . . . . . . . . . . . 132
5.2 Complete and κ-Categorical Theories . . . . . . . . . . . . . . . . . . 137
5.3 Ehrenfeucht’s game . . . . . . . . . . . . . . . . . . . . . . . . . . . . 142
5.4 Embedding and Characterization Theorems . . . . . . . . . . . . . . 145
5.5 Model Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . 151
5.6 Quantifier Elimination . . . . . . . . . . . . . . . . . . . . . . . . . . 157
5.7 Reduced Products and Ultraproducts . . . . . . . . . . . . . . . . . . 163
6 Incompleteness and Undecidability 167
6.1 Recursive and Primitive Recursive Functions . . . . . . . . . . . . . . 169
6.2 Arithmetization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 176
6.3 Representability of Arithmetical Predicates . . . . . . . . . . . . . . . 182
6.4 The Representability Theorem . . . . . . . . . . . . . . . . . . . . . . 189
6.5 The Theorems of G¨odel, Tarski, Church . . . . . . . . . . . . . . . . 194
6.6 Transfer by Interpretation . . . . . . . . . . . . . . . . . . . . . . . . 200
6.7 The Arithmetical Hierarchy . . . . . . . . . . . . . . . . . . . . . . . 205
7 On the Theory of Self-Reference 209
7.1 The Derivability Conditions . . . . . . . . . . . . . . . . . . . . . . . 210
7.2 The Theorems of G¨odel and L¨ob. . . . . . . . . . . . . . . . . . . . . 217
7.3 The Provability Logic G . . . . . . . . . . . . . . . . . . . . . . . . . 221
7.4 The Modal Treatment of Self-Reference . . . . . . . . . . . . . . . . . 223
7.5 A Bimodal Provability Logic for PA . . . . . . . . . . . . . . . . . . . 226
7.6 Modal Operators in ZFC . . . . . . . . . . . . . . . . . . . . . . . . . 228
Hints to the Exercises 231
Literature 241
Contents XI
Index of Terms and Names 247
Index of Symbols 255