[FOM] Arithmetical soundness of ZFC

[Timothy Y. Chow]

John Steel wrote:
>    Bottom-up evidence would be consequences of ZFC which do not fit
> well with existing number theory. Like the consequences of ZFC + V=L in
> the language of 2nd order arithmetic which do no fit well with
> the basic Analysis of low-level projective sets. E.g. what if
> ZFC refutes the Riemann Hypo.?

This is an interesting suggestion.  If we continue to cling to RH in the 
face of a ZFC-disproof, then presumably the disproof will be ineffective, 
because an effective disproof has a certain assent-compelling quality to 
it.  This suggests that if we are too impatient to wait for a ZFC-disproof 
of RH and want to look for an example *now*, then we should cast around 
for ineffective proofs.

One candidate might be the graph minor theorem.  Suppose we believe that 
ZFC is consistent but not arithmetically sound, and in particular suppose 
we believe that the graph minor theorem is a specific example of a false 
theorem of ZFC.  That means we believe in an infinite sequence (G_i) of 
finite graphs such that no G_i is a minor of G_j.  A priori, I see no 
reason why such a sequence couldn't be rather "nice."  For example, 
perhaps it's recursive, and we can write down explicitly an algorithm A
that accepts all and only the G_i.  It might even be possible to prove
in ZFC that A always halts, and that the language it accepts is infinite; 
we just wouldn't be able to prove in ZFC that A witnesses a counterexample 
to the graph minor theorem.  Is there even any reason that the sizes of 
the G_i have to grow rapidly?  I don't immediately see one.  (Maybe a 
bound can be extracted from the Robertson-Seymour proof?)

So someone convinced of this state of affairs could try to come up with 
a candidate algorithm A that appears to work---that is, A can be used to
generate more and more graphs that appear to satisfy the "no G_i is a 
minor of G_j" property.  The numerical evidence could conceivably be so 
compelling that we would start to doubt the arithmetical soundness of ZFC 
(or whatever minimal system is needed to prove the graph minor theorem).

Proving that A really witnesses a counterexample would be a tall order, of 
course.  Under our assumption that ZFC is consistent, any such proof would 
have to be unformalizable in ZFC.  But given how many FOMers were outraged 
by my proposed "Formalization Thesis" a couple of years ago, there must be 
many people who would not bat an eyelid at such a condition.

As an aside, I don't know whether Nik Weaver considers the proof of the 
graph minor theorem to be predicatively sound.  If not, then a more exotic 
candidate would be needed.

Tim