## Mathematical LogicWhat 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 |

277 | |

280 | |

283 | |

### Common terms and phrases

Algebra algorithm alphabet applied arbitrary assignment axiom system binary relation Chapter clauses Compactness Theorem consistent set countable decidable define definition derivable disjunction dom(p domain elementarily equivalent elementary elements enumerable equality-free example Exercise finite subset first-order language first-order logic first-order sentence following holds formal function symbol given Godel H-derivation hence Herbrand structure Horn sentences induction hypothesis infinite logical system logically equivalent Lowenheim-Skolem Theorem mathematical n-ary natural numbers nonempty notion obtain ordered field partial isomorphism prenex normal form procedure proof propositional logic propositional variables prove quantifier quantifier-free R-decidable R-enumerable real numbers rules S-formula S-sentence S-structures 21 S-terms satisfiable second-order second-order logic sequent calculus set of formulas set of sentences set theory strings Suppose symbol set syntactic interpretation system of axioms unary relation symbol uncountable universal Horn formulas

### References to this book

Handbook of Formal Languages: Beyond words Grzegorz Rozenberg,Arto Salomaa No preview available - 1997 |