An Introduction to Mathematical Logic and Type TheoryIn case you are considering to adopt this book for courses with over 50 students, please contact ties.nijssen@springer.com for more information.
The last three chapters of the book provide an introduction to type theory (higher-order logic). It is shown how various mathematical concepts can be formalized in this very expressive formal language. This expressive notation facilitates proofs of the classical incompleteness and undecidability theorems which are very elegant and easy to understand. The discussion of semantics makes clear the important distinction between standard and nonstandard models which is so important in understanding puzzling phenomena such as the incompleteness theorems and Skolem's Paradox about countable models of set theory. Some of the numerous exercises require giving formal proofs. A computer program called ETPS which is available from the web facilitates doing and checking such exercises. Audience: This volume will be of interest to mathematicians, computer scientists, and philosophers in universities, as well as to computer scientists in industry who wish to use higher-order logic for hardware and software specification and verification. |
Contents
Introduction | 1 |
Propositional Calculus | 5 |
10A Supplement on Induction | 17 |
11 The Axiomatic Structure of 𝓟 | 21 |
12 Semantics Consistency and Completeness of 𝓟 | 32 |
13 Independence | 42 |
14 Propositional Connectives | 44 |
15 Compactness | 64 |
41 Craigs Interpolation Theorem | 196 |
42 Beths Definability Theorem | 199 |
Type Theory | 201 |
51 The Primitive Basis of 𝓠₀ | 210 |
53 Equality and Descriptions | 232 |
54 Semantics of 𝓠₀ | 238 |
55 Completeness of 𝓠₀ | 248 |
Formalized Number Theory | 257 |
16 Ground Resolution | 67 |
FirstOrder Logic | 73 |
21 The Axiomatic Structure of 𝓕 | 84 |
22 Prenex Normal Form | 110 |
23 Semantics of 𝓕 | 114 |
24 Independence | 123 |
25 Abstract Consistency and Completeness | 125 |
Simplified Completeness Proof | 139 |
26 Equality | 142 |
Provability and Refutability | 151 |
31 Gentzens Theorem | 156 |
32 Semantic Tableaux | 160 |
33 Skolemization | 166 |
34 Refutations of Universal Sentences | 171 |
35 Herbrands Theorem | 176 |
36 Unification | 183 |
Further Topics in FirstOrder Logic | 189 |
61 Peanos Postulates | 261 |
62 Order | 269 |
63 Minimization | 276 |
64 Recursive Functions | 281 |
65 Primitive Recursive Functions and Relations | 289 |
Incompleteness and Undecidability | 301 |
70 Godel Numbering | 303 |
71 Godels Incompleteness Theorems | 312 |
72 Essential Incompleteness | 323 |
73 Undecidability and Undefinability | 332 |
74 Epilogue | 338 |
Supplementary Exercises | 339 |
Summary of Theorems | 345 |
371 | |
381 | |
383 | |
Other editions - View all
An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof Peter B. Andrews No preview available - 2002 |