[FOM] RE: FOM ``Superincompleteness'' ... Well, almost

[Matt Insall]

[Eisworth]
What about the question "Will mathematics always need more axioms?"  Will
there come a time when mathematicians agree on the truth of enough axioms so
that we can really say "all non-metamathematical statements are decided by
our axioms", or is there some super-incompleteness phenomenon that says "no
matter how we choose to formalize our axioms and the definition of
'non-metamathematical', there will always be a non-metamathematical
statement not decided by our axioms"?


[Friedman]
CONJECTURE. sin(2^2^2^2^2^2^2^2) > 0 cannot be proved or refuted in
ZFC even with large cardinal axioms, without using at least 2^2^100
symbols, even if abbreviations are allowed.

CONJECTURE. "The number of primes less than 2^2^2^2^2^2^2^2 is even"
cannot be proved or refuted in ZFC even with large cardinal axioms,
without using at least 2^2^100 symbols, even if abbreviations are
allowed.

Note that both of these statements can be proved or refuted in ZFC.


[Insall]
In answer to Todd Eisworth, I proffer the following, based upon
the assumption that there is a positive resolution to either of
the above conjectures of Harvey Friedman.  Imagine that we now
choose some extension S of ZFC by some non-large cardinal axiom,
so that in S, we can prove that sin(2^2^2^2^2^2^2^2) > 0 in less
than 2^2^100 steps, or we can prove that the number of primes less
than 2^2^2^2^2^2^2^2 is even, again, in less than 2^2^100 steps.
Then we will have ``decided'' a nonmeta-mathematical statement
by adding an axiom, and the statement we will have ``decided''
would be, under my hypothesis that one of Friedman's conjectures
holds, a statement that we could not have ``decided'' otherwise.
Then, presumably, we can extend Friedman's conjectures to include
ever-longer strings of exponentiated twos, so that no matter how
strong we make our axiom system by adding more axioms, we can
always find a statement like the Friedman conjectures, and prove it
(by similar techniques to those used in proving the original Friedman
conjectures), yielding a sort of independence result for a nonmeta-
mathematical statement of the forms discussed in the Friedman conjectures.
Below is an observation related to this that I just realized must
be true.  Its proof is trivial.  Its consequence is that if either
of Friedman's conjectures is ever proved, then we shall immediately
have a proof of the ``practical consistency'' of ZFC.

Observation:  Suppose that one of Friedman's conjectures holds.
Then there is no proof in less than 2^2^100 steps of a contradiction
from ZFC.

Of course, by ``practical consistency'', I mean that we will then be
justified in making the following assumption:

``No person or machine will prove that ZFC is inconsistent.''

Of course, some of us make such an assumption already, based upon
intuition and empirical evidence.  (In fact, some of us assume that
ZFC is consistent, rather than just ``practically consistent''.)

Now, let me suggest a more formal version of some of my above discussion
of Friedman's conjectures.  For this purpose, let a_0 = 2^2^2^2^2^2^2^2,
and for each n, let a_{n+1} = 2^a_n.  Let S_0 denote ZFC, and for each n,
let S_{n+1} be ZFC+``sin(a_n)>0''.  Let P_0 be the statement of Friedman's
first conjecture above:

``sin(a_0) > 0 cannot be proved or refuted in S_0 even with large cardinal
axioms, without using at least 2^2^100 symbols, even if abbreviations are
allowed''

and, more generally, for each n, let P_n denote the statement

``sin(a_n) > 0 cannot be proved or refuted in S_n even with large cardinal
axioms, without using at least 2^2^100 symbols, even if abbreviations are
allowed''.

Then I expect that something like the following can be shown:

CONJECTURE:  Suppose that P_0 holds.  Then for each n, there is
m > n such that P_m holds.

I think that in a practical sense, this is fairly similar to what Todd
Eisworth
is looking for as ``Superincompleteness''.  Well, almost.