Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

There are many classic textbooks in set and category theory (as possible foundations of mathematics), among many others Jech's, Kunen's, and Awodey's.

Are there comparable classic textbooks in type theory, introducing and motivating their matter in a generally agreed upon manner from the ground up and covering the whole field, essentially?

If not so: why?

share|improve this question
    
Girard's Proofs and Types is quite well-regarded, I think. But one needs some background in ordinary first-order logic to understand it. –  Zhen Lin Feb 25 '12 at 0:24
    
Why would you insist on [set-theory] here? –  Asaf Karagila Feb 25 '12 at 0:26
    
@Asaf: Because I know set theory as one way of foundation and do believe type theory to be an alternative way of foundation. The one road is clear to me (by lots of agreed upon material), the other one not so clear. –  Hans Stricker Feb 25 '12 at 0:30
    
@Zhen Lin: There is lot of set theoretic material to be understood without a lot of background. Why is such material so hard to find in type theory? (No agreed upon ontology, no agreed upon terminology, no agreed upon symbology, ...?) –  Hans Stricker Feb 25 '12 at 0:33
1  
A very clear exposition on basic level with connections to programming languages is Pierce's Types and Programming Languages; there is also a sequel Advanced Topics in Types and Programming Languages. –  sdcvvc Feb 25 '12 at 2:17

2 Answers 2

Although not as comprehensive a textbook as, say, Jech's classic book on set theory, Jean-Yves Girard's Proofs and Types is an excellent starting point for reading about type theory. It's freely available from translator Paul Taylor's website as a PDF. Girard does assume some knowledge of the lambda calculus; if you need to learn this too, I recommend Hindley and Seldin's Lambda-Calculus and Combinators: An Introduction.

As others have mentioned, Martin-Löf's Intuitionistic Type Theory would then be a good next step.

A different approach would be to read Benjamin Pierce's wonderful textbook, Types and Programming Languages. This is oriented towards the practical aspects of understanding types in the context of writing programming languages, rather than purely its mathematical characteristics or foundational promise, but nonetheless it's a very clear and well-written book, with numerous exercises.

The bibliography provided by the Stanford Encyclopedia of Philosophy entry on type theory is quite extensive, and might provide alternative avenues for your research.

share|improve this answer
    
Nice! +1....... –  Tim Feb 25 '12 at 15:13

There are two main settings in which I see type theory as a foundational system.

The first is intuitionistic type theory, particularly the system developed by Martin-Löf. The book Intuitionistic Type Theory (1980) seems to be floating around the internet.

The other setting is second-order (and higher-order) arithmetic. Two main books on this are Foundations without foundationalism by Stewart Shapiro (1991) and Subsystems of second order arithmetic by Stephen Simpson (1999). A decent amount of constructive mathematics, for example the material in Constructive Analysis by Bishop and Bridges (1985), can also be formalized directly in constructive higher-order arithmetic, however the taste of many constructivists is to avoid doing this.

share|improve this answer
    
+1 Nice! (1) What is " a foundational system"? Is it a special kind of formal system? (2) What are relations and differences between set theory, logic, type theory and lambda calculus? I have never been able to understand their purposes even after reading Wiki. (3) Wiki says type theory serves as an alternative to Naive set theory. So I wonder if type theory is a kind of axiom set theory, just like ZFC is a kind of axiom set theory? –  Tim Feb 25 '12 at 13:31
    
(4) what relations and differences are between intuitionistic type theory and the second setting? Is the intuitioistic one based on first order logic, while the other on second or higher order logic? –  Tim Feb 25 '12 at 13:37
    
(5) Wiki says lambda calculus is a formal system in mathematics logic, so I think it is a kind of logic different from the first, second or higher order logic, and therefore typed lambda calclulus is a kind of type theory different from intuitionistic type theory and the other one you mentioned? –  Tim Feb 25 '12 at 16:14

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.