An Introduction to Mathematical Logic and Type Theory

Front Cover
Springer Science & Business Media, Jul 31, 2002 - Computers - 390 pages

In case you are considering to adopt this book for courses with over 50 students, please contact ties.nijssen@springer.com for more information.


This introduction to mathematical logic starts with propositional calculus and first-order logic. Topics covered include syntax, semantics, soundness, completeness, independence, normal forms, vertical paths through negation normal formulas, compactness, Smullyan's Unifying Principle, natural deduction, cut-elimination, semantic tableaux, Skolemization, Herbrand's Theorem, unification, duality, interpolation, and definability.

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
Bibliography
371
List of Figures
381
Index
383
Copyright

Other editions - View all

Common terms and phrases

Popular passages

Page 371 - Andrews. A Reduction of the Axioms for the Theory of Propositional Types. Fundamenta Mathematicae, 52:345-350, 1963.
Page 379 - A proof of cut-elimination theorem in simple type theory. Journal of the Mathematical Society of Japan, vol.
Page 371 - A Transfinite Type Theory with Type Variables (Studies in Logic and the Foundations of Mathematics, North-Holland Publishing Co., Amsterdam: 1965). ' Logic, Semantics, Metamathematics, pp. 271-272. ' See especially Truth and Denotation, Chapters IV and V. 7 See Events, Reference, and Logical Form, 'On Some Prepositional Relations...