Naive Computational Type Theory

"Naive Computational Type Theory" by RobertConstable?

Available from http://www.nuprl.org/documents/constable/NaiveTypeTheoryPreface.html

---

This book's title deliberately alludes to PaulHalmos?' classic SkinnyBook "NaiveSetTheory"; Naive Set Theory is called "naive" because it takes a simple intuitive approach (typically based on the Peano axioms) that ignores issues that lead to e.g. Russell's Paradox (e.g. the set of all sets which do not contain themselves, which turns out to be as paradoxical as other classics such as "this sentence is false"). There are many more sophisticated approaches to set theory which are paradox-free (such as ZFC, Zermelo-Frankel SetTheory with the axiom of choice), but which are more technical and less intuitive in their approach. Since Naive Set Theory is ultimately inconsistent, the Law of the Excluded Middle may not always be used to establish a theorem by contradiction; in some cases it does, in others it simply points to the inconsistency of the axioms. It nonetheless is widely considered a more suitable first introduction to set theory than systems such as ZFC.

Historically, "types" and "The Theory of Types" in mathematics primarily arose in the context of building consistent systems (avoiding Russell's paradox).

---

Table of contents:

1. Types And Equality
2. Subtypes And Set Types
3. Pairs
4. Union And Intersection
5. Functions And Relations
6. Universes, Powers And Openness
7. Families
8. Lists And Numbers
9. Logic And The Peano Axioms
10. Structures, Records And Classes
11. The Axiom Of Choice
12. Computational Complexity

---

CategoryBook CategoryOnlineBook CategoryLanguageTyping CategoryTypeTheory