| |
| |
Preface | |
| |
| |
| |
Background | |
| |
| |
| |
Overview of Mathematical Logic | |
| |
| |
| |
Induction | |
| |
| |
| |
Formal Systems | |
| |
| |
| |
Set Theory, Functions, and Relations | |
| |
| |
| |
Countable and Uncountable Sets | |
| |
| |
| |
Axiom Systems | |
| |
| |
| |
Decidability and Computability | |
| |
| |
| |
Recursive Functions and Recursive Relations | |
| |
| |
| |
Language and Semantics of Propositional Logic | |
| |
| |
| |
Language of Propositional Logic | |
| |
| |
| |
Tautological Consequence | |
| |
| |
| |
Adequate Sets of Connectives | |
| |
| |
| |
Propositional Logic | |
| |
| |
| |
The Formal System P | |
| |
| |
| |
Soundness Theorem | |
| |
| |
| |
Deduction Theorem | |
| |
| |
| |
Model Existence Theorem and Adequacy Theorem | |
| |
| |
| |
Hilbert-Style Proof Systems for Propositional Logic | |
| |
| |
| |
Gentzen-Style Proof Systems for Propositional Logic | |
| |
| |
| |
First-Order Languages | |
| |
| |
| |
A Language for Arithmetic | |
| |
| |
| |
First-Order Languages, Interpretations, and Models | |
| |
| |
| |
Tarski's Definition of Truth | |
| |
| |
| |
Agreement Theorem and Substitution for Free Variables | |
| |
| |
| |
First-Order Logic | |
| |
| |
| |
The Formal System FO<sub>L</sub> | |
| |
| |
| |
Soundness Theorem | |
| |
| |
| |
The Deduction Theorem and the Equality Theorem | |
| |
| |
| |
The Model Existence Theorem | |
| |
| |
| |
G�del's Completeness Theorems; Decidability and Listability | |
| |
| |
| |
Replacement Theorem and Prenex Form | |
| |
| |
| |
Mathematics and Logic | |
| |
| |
| |
First-Order Theories and Hilbert's Program | |
| |
| |
| |
The L�wenheim-Skolem Theorem and the Compactness Theorem | |
| |
| |
| |
Decidable Theories | |
| |
| |
| |
Zermelo-Frankel Set Theory | |
| |
| |
| |
Incompleteness, Undecidability, and Indefinability | |
| |
| |
| |
Overview of the Theorems of Godel, Church, and Tarski | |
| |
| |
| |
Coding and Expressibility | |
| |
| |
| |
Recursive Relation → Expressible Relation | |
| |
| |
| |
Godel's Incompleteness Theorems | |
| |
| |
| |
Church's Theorem | |
| |
| |
| |
Definability and Tarski's Theorem | |
| |
| |
| |
Recursive Functions | |
| |
| |
| |
Recursive Functions | |
| |
| |
| |
Recursive Relations | |
| |
| |
| |
Recursive Coding Functions | |
| |
| |
| |
Primitive Recursion | |
| |
| |
| |
RE Relations | |
| |
| |
| |
THM<sub>r</sub> Is Not Recursive and TR Is Not Definable | |
| |
| |
| |
THM<sub>r</sub> Is RE | |
| |
| |
| |
Computability Theory | |
| |
| |
| |
Register Machines and RM-Computable Functions | |
| |
| |
| |
Recursive → RM-Computable | |
| |
| |
| |
Kleene Computation Relation T<sub>n</sub> | |
| |
| |
| |
Partial Recursive Functions | |
| |
| |
| |
Parameter Theorem and Recursion Theorem | |
| |
| |
| |
Semi-Thue Systems and Word Problems | |
| |
| |
| |
Hilbert's Tenth Problem | |
| |
| |
| |
Overview of Hilbert's Tenth Problem | |
| |
| |
| |
Diophantine Relations and Functions | |
| |
| |
| |
RE Relation → Diophantine Relation (Assuming Bounded ∀-Rule | |
| |
| |
| |
The Exponential Function Is Diophantine | |
| |
| |
| |
Bounded ∀-Rule | |
| |
| |
| |
Applications of the Main Theorem | |
| |
| |
Appendix: Number Theory | |
| |
| |
References and Recommended Readings | |
| |
| |
Index | |