Assume our universe is finite in any sense (the information amount was some $10^{120}$ bits, if I remember correct) and deal with the following, slightly (and intendedly) preposterous, scenario:
-
- The wonderful Theorem T says that all semi-Gaussian gnampfs are reducible.
-
- A proof of T will bring love, peace and harmony to humankind.
-
- Alas, the shortest proof of T takes $10^{120}+1$ bits...
Is there a principal objection against such a dire possibility? I see at least two:
- A. "Shortest proof" implies that human math is totally equivalent to symbol juggling. (In the latter case proofs indeed could be ordered by information complexity.)
- B. Assume we prove the lemma L "All semi-reducible gnampfs are Gaussian" first and this takes only $1/2*10^{120}+1$ bits. Every mathematician on Earth looks at the proof and agrees it is true. We then erase selfsame bits and, using L, need only another $1/2*10^{120}$ bits to prove T, and recycle the bits. (Still, lightspeed and duration of the universe in principle block this weaseling out too. But did we really prove T?)
Do you know references to works dealing with doing math in a finite universe? (Any hardcore Platonist surely will assure that such ponderings are nonsense...)