One example in logic is the proof that $A \Longrightarrow A$ in a "Hilbert-style" deduction system, where our only inference rule is Modus Ponens and we have the two axiom schemata

• K: $\beta \Longrightarrow (\alpha \Longrightarrow \beta)$
• S: $(\alpha \Longrightarrow (\beta \Longrightarrow \gamma)) \Longrightarrow ((\alpha \Longrightarrow \beta) \Longrightarrow (\alpha \Longrightarrow \gamma))$

What gibberish are these? Well, it turns out those are precisely what you need to prove the Deduction Theorem for these systems — that if $\alpha \vdash \beta$ (using $\alpha$ as hypothesis, one can prove $\beta$) then $\vdash \alpha \Longrightarrow \beta$ (with no hypotheses, one can prove $\alpha \Longrightarrow \beta$) — by providing an algorithm that transforms any proof of $\alpha \vdash \beta$ into a (three times as long) proof of $\vdash \alpha \Longrightarrow \beta$. The idea is that for any step $\gamma$ in the original proof, you have a step $\alpha \Longrightarrow \gamma$ in the transformed proof, and then you have a bunch of extra steps to make it all fit together. Axiom scheme S is precisely what you need in order to do a modus ponens $\beta \Longrightarrow \gamma, \beta \vdash \gamma$ when there is a $\alpha \Longrightarrow$ prefix on everything. Axiom scheme K lets you put that $\alpha \Longrightarrow$ prefix on things that are theorems anyway, to import them into the hypothetical realm. However, that part is just definitions / an axiom system, not the mysterious theorem.

To complete the proof transformation required for the Deduction Theorem, you do however also need to prove that $\vdash \alpha \Longrightarrow \alpha$, since this is what you get as the transformation of the step where your proof uses the hypothesis for the first time. Frege had this as a separate axiom ($\alpha \Longrightarrow \alpha$ is a tautology, as he did for K and S, rather than prove it from earlier theorems as he did for everything else (in the implicational fragment of propositional calculus).">at least sort of), but it turns out it can be proved from schemata K and S alone, in just five steps:

1. $(A \Longrightarrow ((A \Longrightarrow A) \Longrightarrow A)) \Longrightarrow ((A \Longrightarrow (A \Longrightarrow A)) \Longrightarrow (A \Longrightarrow A))$
   • instance of axiom scheme S, with $\alpha = \gamma = A$ and $\beta = A \Longrightarrow A$
2. $A \Longrightarrow ((A \Longrightarrow A) \Longrightarrow A)$
   • instance of axiom scheme K, with $\alpha = A \Longrightarrow A$ and $\beta = A$
3. $(A \Longrightarrow (A \Longrightarrow A)) \Longrightarrow (A \Longrightarrow A)$
   • from 1 and 2 by modus ponens
4. $A \Longrightarrow (A \Longrightarrow A)$
   • instance of axiom scheme K, with $\alpha = \beta = A$
5. $A \Longrightarrow A$
   • from 3 and 4 by modus ponens

Checking that this is a proof is trivial. Explaining how it works… is a different matter entirely.

Enter the Curry–Howard correspondence

The names K and S are not from formalised logic, but from the combinatory calculus: these are the standard names for the two higher order functions satisfying the identities

• $K(x)(y) = x$
• $S(f)(g)(x) = f(x)(g(x))$

TeXheads may prefer to think of those as the TeX macros that would be defined as

\def\K#1#2{#1}                % A.k.a. \@firstoftwo
\def\S#1#2#3{#1{#3}{#2{#3}}}  % Not a common utility, but should be

The fun thing about those two is that they generate the whole combinatory calculus — any lambda-term whatsoever can be mechanically translated to a composition of $K$ and $S$. In particular the identity function $I(x)=x$ can be so expressed, in the sense that

• $S(K)(K)(x) = K(x)(K(x)) = x$ for all $x$, hence $I = S(K)(K)$.

Now the untyped combinatory calculus, like the untyped lambda calculus, is too powerful for many purposes (it lets you do anything), so a major activity in these parts of logic and foundations of computer science is to tame it by stamping types on everything. The basic system is the simply-typed theory, where you have some set of atomic types and the ability to make function types; $f : \alpha \to \beta$ means $f$ is a function that takes an argument of type $\alpha$ and returns an argument of type $\beta$. To get functions of several variables, you use currying, so instead of some $f : \alpha \times \beta \to \gamma$ you have $f : \alpha \to (\beta \to \gamma)$. For example the $K$ combinator has type $\alpha \to (\beta \to \alpha)$ since its result has the same type ($\alpha$, say) as the first argument whereas its second argument can have any type ($\beta$).

Similarly analysing the defining identity $S(f)(g)(x) = f(x)(g(x))$ of $S$, we may arbitrarily let $x : \alpha$ (we pick the name $\alpha$ for the type of $x$). Then $f$ and $g$ must both have some $\alpha \to$ type, as they both take $x$ as their first argument. $f(x)$ take $g(x)$ as its argument, but the type of $g(x)$ is not constrained, so let's call that $\beta$, making $g : \alpha\to\beta$. The type of $f(x)(g(x))$ is likewise not constrained, so let's call that $\gamma$. Then we get

• $f : \alpha \to (\beta \to \gamma)$
• $S : (\alpha \to (\beta \to \gamma)) \to ((\alpha\to\beta) \to (\alpha\to\gamma))$

Simply typed terms are too restrictive for proper programming — you can only write trivial programs — so there is an entire industry of designing more complicated type systems for doing more (though still less than the untyped calculus can) while still keeping the functions tame; at least this gives the theorists something to do. However we will only need to consider the $S(K)(K)$ expression for the identity, which is perfectly possible to type with simple types, provided one observes that we can't use the same types for the two $K$s (they will be two different instances of the same untyped combinator). If we take $A$ to be the concrete type of some $x$ that our $S(K)(K)$ should apply to, then the second $K$ must fit the pattern for a $g$ argument of $S$ and have a type of the form $A \to (B \to A)$ for some (so far not constrained) type $B$. The first $K$ must take $x$ as its first argument and $g(x) : B \to A$ as its second, so the first $K$ rather has type $A \to ((B \to A) \to A)$. This means $\alpha = \gamma = A$ and $\beta = B \to A$ in the typing of $S$, so our typed identity of type $A \to A$ is in fact

• $S_{(A \to ((B \to A) \to A)) \to ((A \to (B \to A)) \to (A \to A))} ( K_{A \to ((B \to A) \to A)} )( K_{A \to (B \to A)} )$

where the indices show the exact type instance of the three combinators that is at hand.

As it turns out, that combinatory term also serves as a blueprint for the above proof that $A \Longrightarrow A$, because the instances of the axiom schemes K and S have exactly the same structure as the possible types of the combinators $K$ and $S$, if one substitutes the implication arrow $\Longrightarrow$ for the function type arrow $\to$ (and for simplicity replaces $B$s by $A$s as well). Modus ponens has the same structure as the type inference "if $x$ has type $\beta$ and $f$ has type $\beta \to \gamma$, then $f(x)$ has type $\gamma$". This is (an elementary instance of) the Curry–Howard correspondence.

Opinions vary as to whether this is is a Deep Insight into the way logic really works, or just a funny coincidence. People can get ideological about it. For me, the only way I can reproduce that 5 step proof is to derive it by assigning types in $S(K)(K)$.