From: "Ben Tilly" <btilly@gmail.com>
Date: Sat, 27 May 2006 12:16:12 -0700

``` Sat, 27 May 2006 12:16:12 -0700
On 5/27/06, Taran Rampersad <cnd@knowprose.com> wrote:
> Stephen J. Turnbull wrote:
> >>>>>> "Taran" == Taran Rampersad <cnd@knowprose.com> writes:
> >>>>>>
> >
> >     Taran> I once had to do a mathematical proof that 1+1=2. It wasn't
> >     Taran> as simple as writing 'because it is', it was about 6
> >     Taran> handwritten pages with all sorts of mathematical symbols.
> >
> > Wow, that's really efficient!  It took Russell and Whitehead a couple
> > hundred pages. ;-)
> >
> Peano Axioms. So I cheated. I didn't have to prove them.

Um, you can't prove them.  That's why they are axioms.

BTW now I'm confused that it took so so long.  In the Peano axioms, +
can be recursively defined by the rules:

a + 0 = a
a + s(b) = s(a+b)

In which case:

1 + 1
= s(0) + s(0)
= s(s(0) + 0)
= s(s(0))
= 2

Proving the basic algebraic properties of + is harder, but 1+1=2 is
pretty easy.  In sequence you prove that + is well-defined by single
induction, commutative by a double induction then associative by
triple induction.  After + is properly established, you can define *
and prove the same things about it in the same way.  Then you can
define <, and prove its basic properties, and basic algebraic
relationships with + and *.

All of that might take me 6 pages, but I suspect not.  (Then again I
have more experience than you did when you did that exercise.)

Cheers,
Ben
```