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.

Things to do with 11...

Some folks may recognise these 2 problems/tasks/puzzles as they are lifted quite unashamedly from the excellent Thinking Mathematically by John Mason. They both relate to 11 and its multiples.

Working with these problems myself and with others has served to highlight:

(i) an awareness (or lack) of our number system and how it is built up but also,
(ii) a need to function generally whilst working with specifics i.e. proving that all multiples of 11 demonstrate a certain property.

The first of the problems looks at 4 digit palindromes and the fact that they are all divisible by 11, can you show this? An example of a palindrome would be

racecar, hannah, I

What would a numeric palindrome look like?

The second of the problems asks why the test for divisibility by 11 works...for those who aren't sure this is as follows:

Add up the even digits, add up the odd digits, find the difference.
If the difference is divisible by 11 so is the original number

e.g. 174757
odd digits --> 1 + 4 + 5 = 10
even digits --> 7 + 7 + 7 = 21
Difference is 11 so our number should be divisible by 11

The question remains why does this work? Can you show this in general?