Does the Y combinator contradict the Curry-Howard correspondence?

The Y combinator has the type $(a \rightarrow a) \rightarrow a$. By the Curry-Howard Correspondence, because the type $(a \rightarrow a) \rightarrow a$ is inhabited, it must correspond to a true theorem. However $a \rightarrow a$ is always true, so it appears as if the Y combinator's type corresponds to the theorem $a$, which is not always true. How can this be?

The original Curry-Howard correspondence is an isomorphism between intuitionistic propositional logic and the simply-typed lambda calculus.

There are, of course, other Curry-Howard-like isomorphisms; Phil Wadler famously pointed out that the double-barrelled name "Curry-Howard" predicts other double-barrelled names like "Hindley-Milner" and "Girard-Reynolds". It would be funny if "Martin-Löf" was one of them, but it isn't. But I digress.

The Y combinator does not contradict this, for one key reason: it is not expressible in the simply-typed lambda calculus.

In fact, that was the whole point. Haskell Curry discovered the fixpoint combinator in the untyped lambda calculus, and used it to prove that the untyped lambda calculus is not a sound deduction system.

Interestingly, the type of Y corresponds to a logical paradox which isn't as well-known as it should be, called Curry's paradox. Consider this sentence:

If this sentence is true, then Santa Claus exists.

Suppose the sentence were true. Then, clearly, Santa Claus would exist. But this is precisely what the sentence says, so the sentence is true. Therefore, Santa Claus exists. QED

• Santa Claus doesn't exist?! Oct 31, 2014 at 10:49
• He does, and I just proved it. Nov 1, 2014 at 5:24
• Phew, I was worried for a moment. Nov 2, 2014 at 17:37

The Curry-Howard relates type systems to logical deduction systems. Among other things, it maps:

• programs to proofs
• program evaluation to transformations on proofs
• inhabited types to true propositions
• type systems to logical deduction systems

If the type system admits a Y combinator, then that means that the corresponding logical deduction system is inconsistent — every theorem is true. On the program side, the Y combinator allows any function of type $a \to b$ to be defined, for any $a$ and $b$: $Y (\lambda x. x) \to Y (\lambda x.M)$. The corresponding deduction rule allows any proposition to be derived from any other proposition. Thus the logical system is inconsistent.

The Curry-Howard correspondence is just that: a correspondence. In itself, it doesn't say that certain theorems are true. It says that typability/provability carries from one side to the other.

The Curry-Howard correspondence is useful as a proof tool with many type systems: simply typed lambda calculus, system F, calculus of constructions, etc. All these type systems have the property that the corresponding logic is consistent (if the usual mathematics are consistent). They also have the property of not allowing arbitrary recursion. The Curry-Howard correspondence shows that these two properties are related.

The Curry-Howard still applies to non-terminating typed calculi and inconsistent deduction systems. It's just not particularly useful there.