[FOM] no information proofs

[Harvey Friedman]

Regarding proofs that give no explanation.

We of course have an unlimited supply of such by looking at, e.g., the
base 10 expansion of pi.

Consider

A) the first digit of pi is 3.
B) the sixth digit of pi is 9.

(recall pi ~ 3.14159)

This is an interesting arena to test the idea of "explanation of proof".

I would think that for A), one can fine tune a proof that is quite
explanatory. E.g., start with pi being the circumference divided by
the diameter, and do linear (line segment) approximations.
Incidentally, this leads to a little subject about how close to pi can
you get by linear figures of a given complexity. At least in some
form, this subject is embedded in existing subjects, but the possibly
new spin is to relate this to "explanation" or the related
"simplicity", possibly introducing new twists to an existing
subject(s).

For B), it would be hard to imagine anything similar to what we
probably have for A). And of course, this remark should correspond to
a theorem. Maybe that you have to have a pretty complicated linear
figure to get within 10^-5 of pi.

Regarding Richard Heck's example attributed to Putnam that cardinal
preservation in the standard Cohen mode of ZFC + not(CH)  as a proof
without explanation. We now know that cardinal preservation here
follows in an entirely explained beautiful way from c.c.c., and this
is used constantly in modern set theory. So *now* this is entirely
explained. However, we can ask whether Cohen's original proof is an
explanation. That may depend on whether you can actually see that
Cohen is only using what amounts to c.c.c. I haven't looked at Cohen's
original proof, but it would seem likely that this is the case.

In any case, these look like interesting cases, among many other
specific cases, to test and refine and split the idea of "explanation"
in mathematics.

Harvey Friedman