This textbook introduces first-order logic and its role in the foundations of mathematics by examining fundamental questions. What is a mathematical proof? How can mathematical proofs be justified? Are there limitations to provability? To what extent can machines carry out mathematical proofs? In answering these questions, this textbook explores the capabilities and limitations of algorithms and proof methods in mathematics and computer science.
The chapters are carefully organized, featuring complete proofs and numerous examples throughout. Beginning with motivating examples, the book goes on to present the syntax and semantics of first-order logic. After providing a sequent calculus for this logic, a Henkin-type proof of the completeness theorem is given. These introductory chapters prepare the reader for the advanced topics that follow, such as Gödel's Incompleteness Theorems, Trakhtenbrot's undecidability theorem, Lindström's theorems on the maximality of first-order logic, and results linking logic with automata theory. This new edition features many modernizations, as well as two additional important results: The decidability of Presburger arithmetic, and the decidability of the weak monadic theory of the successor function.
Mathematical Logic is ideal for students beginning their studies in logic and the foundations of mathematics. Although the primary audience for this textbook will be graduate students or advanced undergraduates in mathematics or computer science, in fact the book has few formal prerequisites. It demands of the reader only mathematical maturity and experience with basic abstract structures, such as those encountered in discrete mathematics or algebra.
Author(s): Heinz-Dieter Ebbinghaus, Jörg Flum, Wolfgang Thomas
Series: Graduate Texts in Mathematics
Edition: 3
Publisher: Springer Nature Switzerland
Year: 2021
Language: English
Pages: 304
Tags: First-Order Logic, Computability, Logic Programming
Preface
Contents
Part A
Chapter I Introduction
I.1 An Example from Group Theory
I.2 An Example from the Theory of Equivalence Relations
I.3 A Preliminary Analysis
I.4 Preview
Chapter II Syntax of First-Order Languages
II.1 Alphabets
II.2 The Alphabet of a First-Order Language
II.3 Terms and Formulas in First-Order Languages
II.4 Induction in the Calculi of Terms and of Formulas
II.5 Free Variables and Sentences
Chapter III Semantics of First-Order Languages
III.1 Structures and Interpretations
III.2 Standardization of Connectives
III.3 The Satisfaction Relation
III.4 The Consequence Relation
III.5 Two Lemmas on the Satisfaction Relation
III.6 Some Simple Formalizations
III.7 Some Remarks on Formalizability
III.8 Substitution
Chapter IV A Sequent Calculus
IV.1 Sequent Rules
IV.2 Structural Rules and Connective Rules
IV.3 Derivable Connective Rules
IV.4 Quantifier and Equality Rules
IV.5 Further Derivable Rules
IV.6 Summary and Example
IV.7 Consistency
Chapter V The Completeness Theorem
V.1 Henkin’s Theorem
V.2 Satisfiability of Consistent Sets of Formulas (the Countable Case)
V.3 Satisfiability of Consistent Sets of Formulas (the General Case)
V.4 The Completeness Theorem
Chapter VI The Löwenheim–Skolem Theorem and the Compactness Theorem
VI.1 The Löwenheim–Skolem Theorem
VI.2 The Compactness Theorem
VI.3 Elementary Classes
VI.4 Elementarily Equivalent Structures
Chapter VII The Scope of First-Order Logic
VII.1 The Notion of Formal Proof
VII.2 Mathematics Within the Framework of First-Order Logic
VII.3 The Zermelo–Fraenkel Axioms for Set Theory
VII.4 Set Theory as a Basis for Mathematics
Chapter VIII Syntactic Interpretations and Normal Forms
VIII.1 Term-Reduced Formulas and Relational Symbol Sets
VIII.2 Syntactic Interpretations
VIII.3 Extensions by Definitions
VIII.4 Normal Forms
Part B
Chapter IX Extensions of First-Order Logic
IX.1 Second-Order Logic
IX.2 The System Lω_1ω
IX.3 The System L_Q
Chapter X Computability and Its Limitations
X.1 Decidability and Enumerability
X.2 Register Machines
X.3 The Halting Problem for Register Machines
X.4 The Undecidability of First-Order Logic
X.5 Trakhtenbrot’s Theorem and the Incompleteness of Second-Order Logic
X.6 Theories and Decidability
X.7 Self-Referential Statements and Gödel’s Incompleteness Theorems
X.8 Decidability of Presburger Arithmetic
X.9 Decidability of Weak Monadic Successor Arithmetic
Chapter XI Free Models and Logic Programming
XI.1 Herbrand’s Theorem
XI.2 Free Models and Universal Horn Formulas
XI.3 Herbrand Structures
XI.4 Propositional Logic
XI.5 Propositional Resolution
XI.6 First-Order Resolution (without Unification)
XI.7 Logic Programming
Chapter XII An Algebraic Characterization of Elementary Equivalence
XII.1 Finite and Partial Isomorphisms
XII.2 Fraïssé’s Theorem
XII.3 Proof of Fraïssé’s Theorem
XII.4 Ehrenfeucht Games
Chapter XIII Lindström’s Theorems
XIII.1 Logical Systems
XIII.2 Compact Regular Logical Systems
XIII.3 Lindström’s First Theorem
XIII.4 Lindström’s Second Theorem
References
List of Symbols
Subject Index
