FOM: Length of proofs; Parikh; Sazonov

[Martin Davis]

At 09:54 PM 9/15/98 +0200, peccatte at club-internet.fr wrote:
>Following is a short note published in AMM by Joel Spencer:
>Short theorems with long proofs
>American Mathematical Monthly, 1983, vol. 90, 365-366
>
>--- begin of quote ---
...........................................................
>(a) Short interesting statements are decidable.
>(b) Short interesting theorems have short proofs.

......................................................................

> The possible falsity of (b) is only seeping into our mathematical
>counsciousness.
>--- end of quote ---
>
There has been some discussion on fom of the relevance of G"odel
incompleteness to ordinary mathematical practice. But I don't recall
anything on the relevance of G"odel "speedup": going to stronger systems
will not only increase the set of provable statements, but there will also
be statements provable in both systems whose proof is shortened
"arbitrarily" (i.e. by any given recursive function, the statement depending
on the given function) by going to the stronger system.

Maybe we can hope that large cardinals will not only yield proofs of
previously open questions but will also help in obtaining short neat proofs
where only clumsy unwieldy ones were previously available.

Martin