| |
| |
| 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 | |