# Book:Peter B. Andrews/An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof

## Peter B. Andrews: *An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof*

Published $1986$, **Academic Press**

- ISBN 978-0120585366.

### Subject Matter

- Mathematical Logic
- Type Theory

### Contents

*Preface***Introduction***Chapter 1***Propositional Calculus**- 10. Formation Rules for $\mathscr P$
- 10A. Supplement on Induction
- 11. The Axiomatic Structure of $\mathscr P$
- 12. Semantics, Consistency, and Completeness of $\mathscr P$
- 13. Independence
- 14. Propositional Connectives
- 15. Compactness
- 16. Ground Resolution

*Chapter 2***First-Order Logic**- 20. Formation Rules for the System $\mathscr F$
- 21. The Axiomatic Structure of $\mathscr F$
- 22. Prenex Normal Form
- 23. Semantics of $\mathscr F$
- 24. Independence
- 25. Abstract Consistency and Completeness
- 25A. Supplement: Simplified Completeness Proof
- 26. Equality

*Chapter 3***Provability and Refutability**- 30. Natural Deduction
- 31. Gentzen's Theorem
- 32. Semantic Tableaux
- 33. Skolemization
- 34. Refutations of Universal Sentences
- 35. Herbrand's Theorem
- 36. Unification

*Chapter 4***Further Topics in First-Order Logic**- 40. Duality
- 41. Craig's Interpolation Theorem
- 42. Beth's Definability Theorem

*Chapter 5***Type Theory**- 50. Introduction
- 51. The Primitive Basis of $\mathcal Q_0$
- 52. Elementary Logic in $\mathcal Q_0$
- 53. Equality and Descriptions
- 54. Semantics of $\mathcal Q_0$
- 55. Completeness of $\mathcal Q_0$

*Chapter 6***Formalized Number Theory**- 60. Cardinal Numbers and the Axiom of Infinity
- 61. Peano's Postulates
- 62. Order
- 63. Minimization
- 64. Recursive Functions
- 65. Primitive Recursive Functions and Relations

*Chapter 7***Incompleteness and Undecidability**- 70. Gödel Numbering
- 71. Gödel's Incompleteness Theorems
- 72. Essential Incompleteness
- 73. Undecidability and Undefinability
- 74. Epilogue

*Appendix***Summary of Theorems***Bibliography**Index*