[FOM] Checkers is a draw

[John McCarthy]

Timothy Chow quotes Neelakantan Krishnaswami as saying in part

> To understand why this sort of rule is necessary, consider the example
> of showing that 170 * 40 = 6800. No one will do this proof by
> appealing to Peano's axioms, because it would be thousands of lines
> long. Instead we will /calculate/ that 170 * 40 gives 6800, and then
> appeal to reflexivity, which is a one-line proof plus some
> computation.

I agree that reflexivity and appealing to the computer is the best way
to go.  However, a proof from Peano's axioms expressed in first order
logic that 170 * 40 = 6800 need not be thousands of lines provided
some definitions and theorems expressing the grade school way of doing
the calculation are provided.  If this is done, the size of the proof
of a particular multiplication will be a small multiple of the size of
the calculation

170
 40
_______
 000
680
_______
6800

As far as I can see, calculations can always be replaced by proofs at
the cost of a small multiple of size plus and additive constant for
definitions and theorems.  However, I do not see any advantage in
avoiding reflection principles.