[Math] Reference request for type theory

reference-requesttype-theory

I am interested in learning the theory of types, especially in how they can provide a foundation to mathematics different to sets and how they can avoid self-referential paradoxes by stipulating that a collection of objects of type n has type n+1. As for my background knowledge, I only know a little of propositional and predicate logic and Zermelo-Fraenkel set theory.

Best Answer

I would suggest you look at Martin-Löf's work, such as the following reprint of his earlier unpublished manuscript (from 1972?):

Per Martin-L: An Intuitionistic Theory of Types. In: Twenty-Five Years of Constructive Type Theory Proceedings of a Congress held in Venice, October 1995. Editors: Giovanni Sambin and Jan M. Smith. Oxford University Press, 1998.

I belive a fairly good approximation of this paper is available online. If you are looking for other online references, have a look at this lecture by Martin-Löf.

This should give you some idea for type theory as foundation of mathematics.

Related Solutions

[Math] A Learning Roadmap request: From high-school to mid-undergraduate studies

I'm not a big fan of full roadmaps and reading lists. Exploring mathematics is something that can be totally different depending on where and who you are. Any serious roadmap needs to be flexible and take account of the course: reading maths is a skill (one you seem well on your way to learning btw! but still...), initially you may find actual teaching easier to grasp- and your reading should work along side that. So here's my attempt at a flexible roadmap:

1) Buy some very carefully chosen books and read them cover to cover: There's a lot of baffling books out there- even some that look really UG friendly can have you weeping by page 5 in your first year- and you only want 4-5 to start with (any more will just be too expensive and you won't get round to reading all of them- top up via the library). My recommendations are: 'Naive set theory- Halmos', 'Finite dimensional vector spaces- Halmos', 'Principles of mathematical analysis- Rudin' and 'Proofs from the book- Aigner and Ziegler'.

[These, ostensibly, cover the exact same material as the book you have decided to buy- but to develop quickly I urge you to buy more mathematical texts like these: Halmos' and Rudin's writing styles are very clear but technical (in a way that the book you are interested in will not be), and will make you a better mathematician faster than any book that tries to 'bridge the gap' ever would. I also seconded Owen's call for proofs from the book: it is simultaneously inspiring and useful as a way of seeing 'advanced' topics in action- it's something you'll keep coming back to, right up to your third year!]

2) Do all of the excercises: Or as much as you can bear to- even if it looks like it's beneath you (if you're half decent- a lot of first year will!) you will be surprised as to how much it helps with your mathematical development (and the crucial high mark you'll need for a good PhD placement). This applies to classes and your 4-5 text books.

3) Ask your tutor about doing some modules from the year above: If you've read all of those textbooks and done all of the excercises, you will be ready. Get some advice from your tutor about what would be best and roll with it (most unis won't make you take the exam, so if you don't feel comfortable you're fine). Taking something like metric spaces or group theory in your first year will put you top of the pile.

4) Keep doing all of these things: Immerse yourself in maths- keep on MO, meet likeminded people and no matter how slow the course seems to be moving, no matter the allure of apathy: keep at it. Advice for later books would be pointless now, but there will be people who can give it to you there and then (use maths forums if you want). Oh, and never rule out an area- you never know where intrigue will come from...

Best of luck, Tom

[Math] Surreal Numbers as Inductive Type

Heh, I just ran across this old question again and realized that I now know an answer: it's in section 11.6 of the HoTT Book. It's written out there as a higher inductive-inductive type; in other language it says roughly that $\mathbf{No}$ is the initial object among classes $X$ equipped with the following.

Two binary relations $<$ and $\le$.
For any two sub-sets $L,R\subseteq X$ such that $x^L<x^R$ for all $x^L\in L$ and $x^R\in R$, a specified element $x\in X$, written $\{x^L\mid x^R\}$.
If $x,y\in X$ satisfy $x\le y$ and $y\le x$, then $x=y$.
Given $x = \{x^L\mid x^R\}$ and $y = \{y^L\mid y^R\}$, if every $x^L<y$ and every $x<y^R$, then $x\le y$.
Given $x = \{x^L\mid x^R\}$ and $y = \{y^L\mid y^R\}$, if some $x\le y^L$, then $x<y$.
Given $x = \{x^L\mid x^R\}$ and $y = \{y^L\mid y^R\}$, if some $x^R\le y$, then $x<y$.

The first innovation is that in place of the single order relation of a ZF-structure, we specify the strict and non-strict order relations as separate data. The second is that we include in the above list of axioms a way to make two surreal numbers equal; categorically this means we consider not initial algebras for an endofunctor, but initial algebras for a presented monad (type-theoretically it corresponds to using higher inductive types rather than ordinary inductive types).

Best Answer

Related Solutions

[Math] A Learning Roadmap request: From high-school to mid-undergraduate studies

[Math] Surreal Numbers as Inductive Type

Related Question