# Why was there a need for Martin-Löf to create intuitionistic type theory?

I've been reading up on Intuitionistic Type Theory (ITT) and it does make sense. But what I'm struggling to understand is "why" was it created in the first place?

Intuitionistic Logic (IL) and Simply-typed $\lambda$-calculus (STLC) and type theory in general predates the very existence of Martin-Löf himself! It seems that one can do everything in STLC that is doable in ITT (I may be wrong, but at least it feels that way).

So what was "novel" about ITT and how exactly did (or does) it advance the theory of computation? From what I understand, he introduced the notion of "dependent types", but it seems they were already there in STLC, in a way. Was his ITT an attempt at abstraction to understand the underlying principles of STLC and IL together? But didn't STLC already held do that? So, just why was ITT created in the first place? What is/was the point?

Here's an excerpt from Wikipedia: But I still don't get the reason behind its creation that didn't already exist before.

Martin-Löf's first draft article on type theory dates back to 1971. This impredicative theory generalized Girard's System F. However, this system turned out to be inconsistent due to Girard's paradox which was discovered by Girard when studying System U, an inconsistent extension of System F. This experience led Per Martin-Löf to develop the philosophical foundations of type theory, his meaning explanation, a form of proof-theoretic semantics, which justifies predicative type theory as presented in his 1984 Bibliopolis book...

It seems from the excerpt that the reason was to develop the "philosophical foundations of type theory" - I thought this foundation already existed (or maybe I assumed it did). Was this the main reason then?

• If I remember correctly the reason he did so was a bit philosophical (a constructive foundation of mathematics) and not just technical, but it has been sometime since I have attended his lectures and I don't have my notes from them with me to look up. A good place to look up to grasp a better understanding of Martin-Lof's work and its comparison to other theories is Beeson's "Foundations of Constructive Mathematics". It has a chapter devoted to that. – Kaveh Mar 2 '15 at 5:55
• ps: you might want to edit the title to match what you are asking in the body, right now the title seems to ask what was the novelty in Martin-Lof's theory, while the body seems to be asking why he did it. – Kaveh Mar 2 '15 at 6:02

Very briefly: the simply-typed $\lambda$-calculus does not have dependent types. Dependent types were proposed by de Bruijn and Howard who wanted to extend the Curry-Howard correspondence from propositional to first-order logic. The key contribution of Martin-Löf's is a novel analysis of equality. There are two main ways of giving Curry-Howard style account of equality.