Mathematical Logic

Stephen G. Simpson
October 7, 2008
Department of Mathematics
The Pennsylvania State University
University Park, State College PA 16802
http://www.math.psu.edu/simpson/

Contents

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¨onig’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 . . . . . . . . . . . . . . . . . . . . . 66
4 Extensions of Predicate Calculus 71
4.1 Predicate Calculus with Identity . . . . . . . . . . . . . . . . . . 71
4.2 The Spectrum Problem . . . . . . . . . . . . . . . . . . . . . . . 75
4.3 Predicate Calculus With Operations . . . . . . . . . . . . . . . . 78
4.4 Predicate Calculus with Identity and Operations . . . . . . . . . 82
4.5 Many-Sorted Predicate Calculus . . . . . . . . . . . . . . . . . . 84
5 Theories, Models, Definability 87
5.1 Theories and Models . . . . . . . . . . . . . . . . . . . . . . . . . 87
5.2 Mathematical Theories . . . . . . . . . . . . . . . . . . . . . . . . 89
5.3 Definability over a Model . . . . . . . . . . . . . . . . . . . . . . 97
5.4 Definitional Extensions of Theories . . . . . . . . . . . . . . . . . 100
5.5 Foundational Theories . . . . . . . . . . . . . . . . . . . . . . . . 103
5.6 Axiomatic Set Theory . . . . . . . . . . . . . . . . . . . . . . . . 106
5.7 Interpretability . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111
5.8 Beth’s Definability Theorem . . . . . . . . . . . . . . . . . . . . . 112
6 Arithmetization of Predicate Calculus 114
6.1 Primitive Recursive Arithmetic . . . . . . . . . . . . . . . . . . . 114
6.2 Interpretability of PRA in Z1 . . . . . . . . . . . . . . . . . . . . 114
6.3 G¨odel Numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114
6.4 Undefinability of Truth . . . . . . . . . . . . . . . . . . . . . . . . 117
6.5 The Provability Predicate . . . . . . . . . . . . . . . . . . . . . . 118
6.6 The Incompleteness Theorems . . . . . . . . . . . . . . . . . . . . 119
6.7 Proof of Lemma 6.5.3 . . . . . . . . . . . . . . . . . . . . . . . . 121