29
$\begingroup$

Does anyone know any good references that describe type theoretical foundations of mathematics? I've read some books e.g. Winskel's The Formal Semantics of Programming Languages and Pierce's Types and Programming Languages. However, these don't address foundational issues, since they are geared towards practical programming language semantics and don't assume any knowledge of logic.

What troubles me is that almost any definition of mathematics has a set as part of the definition, so any foundation would somehow have to address sets and elements that we use in order to concretely compute (unless I'm completely missing the point). Is there any rigorous book that starts by giving a precise definition of what a type is and how it can be used to describe foundations? Every book I've read so far has failed to even give a precise definition of a type.

$\endgroup$
8
  • 7
    $\begingroup$ i think this new project on homotopy type theory might be of interest to you homotopytypetheory.org $\endgroup$
    – citedcorpse
    Commented Jun 28, 2013 at 9:11
  • $\begingroup$ @exitingcorpse: I know of that project and they recently published an open source book. I haven't looked at it, since I'm not sure whether it answers my question. $\endgroup$
    – Edvard Fagerholm
    Commented Jun 28, 2013 at 9:13
  • 3
    $\begingroup$ One of my friends from the masters switched to computer science for his Ph.D., and I recall talking to him once and he said that he's been reading on type theory for something and that the got the feeling that a lot of the people there didn't know what they really talk about (in comparison to, say, classical analysis, where the definitions are very concrete and clear). I'm sure that that's not 100% true on the actual people, but that impression did stick with me. He also made the same claim on the theoretical foundations of CS being shaky and people are not sure what they want to do, or how. $\endgroup$
    – Asaf Karagila ♦
    Commented Jun 28, 2013 at 9:15
  • 2
    $\begingroup$ As far as I can tell, the homotopy type theory effort precisely and completely answers your question. Perhaps you should look at it before deciding it is not suitable. $\endgroup$
    – András Salamon
    Commented Jun 29, 2013 at 14:19
  • 2
    $\begingroup$ @AsafKaragila, that doesn't surprise me at all. For example, I'm often struck by the way that many (not all) authors of type-theoretic literature claim that the meaning of an expression is given by its introduction and elimination rules. NO! As any logician will tell you, syntax and semantics are very, very different beasts. (I'm not claiming that every type-theorists makes this mistake, only that it seems prevalent in that field.) $\endgroup$
    – goblin GONE
    Commented Feb 2, 2014 at 3:12

1 Answer 1

Reset to default
7
$\begingroup$

As much as I can confirm that (the introduction and the type theory chapter of) the homotopy type theory book is well written, I have the impression that there are shorter texts focusing more directly on (the history of) type theory as foundations. The Stanford Encyclopedia of Philosophy (SEP) is an excellent place where one can find such shorter texts. A good place to start might be the section on typed theories in Randall Holmes' SEP entry on Alternative Axiomatic Set Theories. A more complete picture including $\lambda$-calculus can be found in Thierry Coquand's SEP entry on Type Theory. The latest revision of that entry even contains a section on univalent foundations (homotopy type theory).

I have to admit that the SEP articles are quite broad and contain many historical and philosophical references. For some more mathematically minded people, a more focused account like William Farmer's The Seven Virtues of Simple Type Theory might be better suited as an introduction to type theories (as foundation). One problem with type theory as a foundation is that there are so many different (non-equiconsistent) type theories. For set theory, this problem can be avoided by using ZF (or NBG) as the "canonical" set theory. Saunders Mac Lane (1986) tried to address this problem by advocating "bounded Zermelo set theory" as a foundation for mathematics:

Some weaker subsystems of ZFC are used. Zermelo set theory, the system Z described above, is still studied. The further restriction of the axiom of separation to formulas in which all quantifiers are bounded in sets ($\Delta_0$ separation) yields "bounded Zermelo set theory" or "Mac Lane set theory", so called because it has been advocated as a foundation for mathematics by Saunders Mac Lane (1986). It is interesting to observe that Mac Lane set theory is precisely equivalent in consistency strength and expressive power to TST with the Axiom of Infinity. Z is strictly stronger than Mac Lane set theory; the former theory proves the consistency of the latter. See Mathias (2001) for an extensive discussion.

In an answer to another question, I tried to explain how TST is related to other type theories, and how it derives its consistency strength from non-circular impredicative quantification.

$\endgroup$
2
  • $\begingroup$ Thanks for this comment. I'll look into the references once I have time. $\endgroup$
    – Edvard Fagerholm
    Commented Oct 28, 2014 at 0:17
  • 1
    $\begingroup$ The Seven Virtues paper is outstanding, the best exposition I've seen yet of simple type theory as a mathematical foundation. Thanks! $\endgroup$
    – Adam Dingle
    Commented Jun 21, 2017 at 13:31

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .