Mathematical LogicSpringer Science & Business Media, 15.11.1996 - 291 Seiten 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. |
Inhalt
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 | |
Andere Ausgaben - Alle anzeigen
Häufige Begriffe und Wortgruppen
a₁ applied arbitrary assignment axiom system binary relation Chapter Compactness Theorem consistent set countable decidable define definition derivable dom(p domain elementarily equivalent elementary elements enumerable equality-free example Exercise finite subset first-order language first-order logic following holds formal function symbol Gödel H-derivation hence Herbrand structure Horn sentences induction hypothesis infinite isomorphism K₁ and K2 logical system logically equivalent Löwenheim-Skolem Theorem mathematical natural numbers nonempty notion obtain 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-sentences S-structure S-terms satisfiable second-order second-order logic sequent calculus set of formulas set of sentences set theory strings structure Suppose symbol set system of axioms t₁ t₂ Th(N unary relation symbol uncountable universal Horn formulas v₁ valid
Verweise auf dieses Buch
Handbook of Formal Languages: Beyond words, Band 3 Grzegorz Rozenberg Keine Leseprobe verfügbar - 1997 |