# Mathematical proofs implemented purely by Lambda Calculus

I've seen often stated that Lambda Calculus can be used for mathematical proofing but I haven't yet seen any example how it is actually used for the task.

Is there a simple example, lambda abstraction or application that can be shown to be a valid mathematical proof? For example what does it take to make a Church numeral successor function regarded as a mathematical proof?

• Lambda calculus is mostly there for other things. For example, I used it, like, two weeks ago in my lecture, to show the difference between the evaluation orders that leads to laziness vs. strictness and call-by-name vs. call-by-value. – Oleg Lobachev Dec 15 '17 at 20:54
• LC as a symbolic manipulation method is interesting to compare with mathematical equation manipulation method, thus as a candidate for a universal mathematical language. But seemingly as an untyped form, it is not so useful... That bites a bit of the halo of being simple and universal after all. – MarkokraM Dec 15 '17 at 21:11

So, the trick is that the untyped lambda calculus is not very useful as a mathematical proof, since it has non-halting terms.

Lambda Calculus as a proof system is most useful with types, particularly in terms of the Curry-Howard Isomorphism. Phillip Wadler has a great article outlining this.

The basic idea is that lambda abstraction corresponds to the way that you prove an implication. To write a function of type $A \to B$, you assume you have a value of type $A$, and use it to construct a return value of type $B$. This is exactly how you prove $A \implies B$: assume that $A$ holds, then use this to prove $B$.

Not every lambda term corresponds to a mathematical proof in the sense we're used to, although each term can be regarded as a proof that its type is inhabited. In particular, to prove anything really useful, you need dependent types, where types are allowed to be indexed by values.

For Church-Numerals, their typed version if $\forall a \ldotp a \to (a \to a) \to a$, which, when interpreted as a proposition, is really boring. It's saying that if something holds, and it implies itself, then that something still holds.