FOM: Length of proofs; Parikh; Sazonov

[Patrick Peccatte]

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 ---
Long proofs are an anathema to mathematicians. Part of mathematics'
uniqueness is the verifiability of an argument. This is being called
into question with the existence of proofs of inordinate length. A folk
theorem, surely known in the 1930's, is particularly germane today. A
recent note in which F.H. Norwood ("Long proofs", This Monthly, 89
(1982), 110-112) appears unaware of this result provided the motivation
for these remarks. We give three variants, with increasing formality.

(i) There exist short theorems with long proofs.
(ii) There exist theorems T whose shortest proofs have length at least
(10^100)(2^2^n) where n is the length of T.
(iii) For all recursive function F there exist theorems T whose shortest
proofs have length at least F(n) where n is the length of T.

There remains a hidden variable: the formal system in which theorems are
proven. The folk theorem applies to any formal system for which there is
no decision procedure for theoremhood. This includes Peano Arithmetic,
Zermelo-Fraenkel set theory, or any formalization of "Generally Accepted
Mathematics". It does not apply to limited systems such as the first
order theory of Finite Fields.
Suppose (iii) were false for a specific F and every theorem of length n
had a proof of length at most F(n). This would give a simple decision
procedure for statements S. Let n be the length of S and examine all
texts of length at most F(n). The statement S is a theorem if and only
if one of these texts is a proof of S. As no such decidability procedure
exists, (iii) is proved.
Version (i), even allowing for informality, is somewhat misleading.
Since the integer n which exists by the folk theorem may itself be very
large, it may be the case that there are long theorems with very, very
long proofs.
Einstein's dogma, "God does not play dice with the universe" may be
translated from physics to mathematics in (at least) two ways:

(a) Short interesting statements are decidable.
(b) Short interesting theorems have short proofs.

Fifty years after Gödel, many mathematicians view (a) as false. (The
Axiom of Choice and the Continuum Hypothesis are short, interesting, and
known to be undecidable, but let us restrict ourselves to statements
expressible in Peano Arithmetic.) "Are there an infinite number of
primes of the form (2^p) - 1 ?" may well be undecidable. The advent of
computer proofs has focused attention on (b). A decade ago no
counterexamples to (b) were known. Now there are two. The Four-Color
theorem is the first. The cataloging of Finite Simple Groups (in 5000
pages) is the second - or rather, a second class. Short interesting
theorems such as "Every 6-transitive subgroup of S_n is (n -
2)-transitive" now have proofs of 5000 + epsilon pages. In both cases
shorter proofs are being sought and may eventually be found. Or perhaps
not. The possible falsity of (b) is only seeping into our mathematical
counsciousness.
--- end of quote ---

Comments are welcome, specially on these subjects:
- other formulations of the Spencer's folk theorem?
- is exists any argument different than 4CT or FSG classification (other
long proofs, philosophical or heuristical arguments, others) against
(b)? Or supporting (b).
- is it possible to imagine statements like:
(c) long theorems could have short proofs.
(d) long theorems are uninteresting (i.e. theorems are short theorems).
---
fom member digest:
Name: Patrick Peccatte
Position: Software engineer and philosopher
Institution: Independent private company and Paris 7 University
Research interest: History and philosophy of sciences and mathematics
(specially quasi-empiricism, experimental mathematics, ontology)
More information: http://peccatte.rever.fr (in French)