# Mathematical Logic

Springer Science & Business Media, Nov 15, 1996 - Mathematics - 291 pages
What is a mathematical proof? How can proofs be justified? Are there limitations to provability? To what extent can machines carry out mathe matical proofs? Only in this century has there been success in obtaining substantial and satisfactory answers. The present book contains a systematic discussion of these results. The investigations are centered around first-order logic. Our first goal is Godel's completeness theorem, which shows that the con sequence relation coincides with formal provability: By means of a calcu lus consisting of simple formal inference rules, one can obtain all conse quences of a given axiom system (and in particular, imitate all mathemat ical proofs). A short digression into model theory will help us to analyze the expres sive power of the first-order language, and it will turn out that there are certain deficiencies. For example, the first-order language does not allow the formulation of an adequate axiom system for arithmetic or analysis. On the other hand, this difficulty can be overcome--even in the framework of first-order logic-by developing mathematics in set-theoretic terms. We explain the prerequisites from set theory necessary for this purpose and then treat the subtle relation between logic and set theory in a thorough manner.

### What people are saying -Write a review

We haven't found any reviews in the usual places.

### Contents

 Introduction 3 1 An Example from Group Theory 4 2 An Example from the Theory of Equivalence Relations 5 3 A Preliminary Analysis 6 4 Preview 8 Syntax of FirstOrder Languages 11 2 The Alphabet of a FirstOrder Language 13 3 Terms and Formulas in FirstOrder Languages 15
 4 Set Theory as a Basis for Mathematics 110 Syntactic Interpretations and Normal Forms 115 2 Syntactic Interpretations 118 3 Extensions by Definitions 125 4 Normal Forms 128 PART B 135 Extensions of FirstOrder Logic 137 1 SecondOrder Logic 138

 4 Induction in the Calculus of Terms and in the Calculus of Formulas 19 5 Free Variables and Sentences 24 Semantics of FirstOrder Languages 27 1 Structures and Interpretations 28 2 Standardization of Connectives 31 3 The Satisfaction Relation 32 4 The Consequence Relation 33 5 Two Lemmas on the Satisfaction Relation 40 6 Some Simple Formalizations 44 7 Some Remarks on Formalizability 48 8 Substitution 52 A Sequent Calculus 59 1 Sequent Rules 60 2 Structural Rules and Connective Rules 62 3 Derivable Connective Rules 63 4 Quantifier and Equality Rules 66 5 Further Derivable Rules and Sequents 68 6 Summary and Example 69 7 Consistency 72 The Completeness Theorem 75 2 Satisfiability of Consistent Sets of Formulas the Countable Case 79 3 Satisfiability of Consistent Sets of Formulas the General Case 82 4 The Completeness Theorem 85 The LöwenheimSkolem Theorem and the Compactness Theorem 87 2 The Compactness Theorem 88 3 Elementary Classes 91 4 Elementarily Equivalent Structures 94 The Scope of FirstOrder Logic 99 2 Mathematics Within the Framework of FirstOrder Logic 103 3 The ZermeloFraenkel Axioms for Set Theory 107
 2 The System ℒw₁w 142 3 The System ℒQ 148 Limitations of the Formal Method 151 1 Decidability and Enumerability 152 2 Register Machines 157 3 The Halting Problem for Register Machines 163 4 The Undecidability of FirstOrder Logic 167 5 Trahtenbrots Theorem and the Incompleteness of SecondOrder Logic 170 6 Theories and Decidability 173 7 SelfReferential Statements and Gödels Incompleteness Theorems 181 Free Models and Logic Programming 189 2 Free Models and Universal Horn Formulas 193 3 Herbrand Structures 198 4 Propositional Logic 200 5 Propositional Resolution 207 6 FirstOrder Resolution without Unification 218 7 Logic Programming 226 An Algebraic Characterization of Elementary Equivalence 243 1 Finite and Partial Isomorphisms 244 2 Fraïssés Theorem 249 3 Proof of Fraïssés Theorem 251 p Ehrenfeucht Games 258 Lindströms Theorems 261 2 Compact Regular Logical Systems 264 3 Lindströms First Theorem 266 4 Lindströms Second Theorem 272 References 277 Symbol Index 280 Subject Index 283 Copyright