Mathematical Logic

Front Cover
Springer Science & Business Media, Nov 15, 1996 - Mathematics - 291 pages
0 Reviews
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

Common terms and phrases

References to this book

All Book Search results »

About the author (1996)

Prof. Jvrg Flum, Abteilung f]r Mathematische Logik, Albert-Ludwigs-Universitdt Freiburg, Germany, http: //logik.mathematik.uni-freiburg.de/personen/Flum.html Prof. Martin Grohe, Institut f]r Informatik, Humboldt-Universitdt zu Berlin, Germany, http: //www.informatik.hu-berlin.de/~grohe/ The authors are very well qualified to write this book. In addition to their strong backgrounds in complexity, algorithms, etc., they have contributed a number of specific key results in parameterized complexity (e.g., http: //epubs.siam.org/sam-bin/dbq/article/42720). Jvrg Flum has coauthored two other Springer monographs: (i) "Mathematical Logic," Undergraduate Texts in Mathematics, 0-387-94258-0, 3rd printing since 1994, over 4000 copies sold, Heinz-Dieter Ebbinghaus, Jvrg Flum, Wolfgang Thomas, http: //www.springer.com/0-387-94258-0. (ii) "Finite Model Theory," Springer Monographs in Mathematics (was in series Perspectives in Mathematical Logic), printed in soft- and hardback, 1995, 2nd ed. in 1999, 2nd corr. print in 2006, Heinz-Dieter Ebbinghaus, Jvrg Flum, 3-540-28787-6, http: //www.springer.com/3-540-28787-6. In addition, Jvrg Flum coauthored the following LNM title: Vol. 769, "Topological Model Theory, 1980, 3-540-09732-5, Jvrg Flum, Martin Ziegler. And he coedited the following LNCS title: Vol. 1683, CSL 1999 conf. proc., Jvrg Flum, Mario Rodriguez-Artalejo, 1999, 3-540-66536-6. Prof. Martin Grohe has authored over 50 articles for refereed theoretical computer science journals and conference proceedings (http: //www.informatik.uni-trier.de/~ley/db/indices/a-tree/g/Grohe: Martin.html) in the areas of logic, complexity, algorithms, etc.

Prof. Dr. Heinz-Dieter Ebbinghaus und Prof. Dr. JArg Flum forschen und lehren am Institut fA1/4r Mathematik der UniversitAt Freiburg, Prof. Dr. Wolfgang Thomas ist Inhaber des Lehrstuhls fA1/4r Informatik 7 (Logik und Theorie diskreter Systeme) der RWTH Aachen.

Bibliographic information