The Proof is in the P(udding)ierce's Lemma

Hey there I just unearthed an old proof that I liked from my degree. I figured some folk may appreciate it so here it is.

If you don't appreciate it then please enjoy the cartoon above that I borrowed from here.

Pierce's Lemma

Show that: ¦-- (((a->b)->a)->a) (=: c)

Pf: So rewrite the lemma as ¦-- c
By one of the "famous" theorems of prop. calc. we have

¦-- ((a->c)->((¬a->c)->c))

So Suff. To Prove (i)¦--(a->c) & (ii)¦--(¬a->c)

(i) by applying DT twice it is STP that

{a, ((a->b)->a)} ¦-- a

a one line pf so done

(ii) by applying DT twice it is STP that

{¬a, ((a->b)->a)} ¦-- a

One of the theorems says: ¦-- (¬a->(a->b))
So we have that {¬a, ((a->b)->a)} ¦-- ¬a
{¬a, ((a->b)->a)} ¦-- (¬a->(a->b))
so by MP: {¬a, ((a->b)->a)} ¦-- (a->b)
{¬a, ((a->b)->a)} ¦-- ((a->b)->a)
so by MP: {¬a, ((a->b)->a)} ¦-- a

So we've proved (i) and (ii) and so by the tautology we have Peirce's Lemma.