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.
