# Axiom of Choice-esque argument to show that a proof of a statement exists without actually giving a proof

What if the set of all well-formed statements in ZFC formed a kind of pseudo-category where a morphism f between objects A, B represented a formal proof that A implied B? What if that category could be interpreted as a strange topological space, and was proved to be a disjoint union of special path connected subspaces?

The connected subspaces are not ordinary, in that many paths from a given statement to another are not reversible. Then someone shows that since two statements (e.g. Riemann Hypothesis and some other proven conjecture) are in the same connected subspace, there exits a morphism (that is, a correct formal proof) of the Riemann Hypothesis.

No one is any closer to proving RH, but there is some axiom-of-choice-esque argument that a proof exists.

Would everyone accept that the Riemann Hypothesis is true? Is such an approach, to show proofs exist without giving an actual proof, viable?

-
formal proof of implication in what theory? $\sf ZFC$? It seems that "showing that RH and provable statement X are in the same connected component" is exactly as saying "statement X implies RH", which means that we have found a proof for RH. –  Asaf Karagila May 9 '13 at 20:50
Any such category or topological space must be connected: everything proves $\top$, and $\bot$ proves everything. –  Zhen Lin May 9 '13 at 20:57
Yes, you have a pre-order, and the category defined by that pre-order, and the pre-order has a maximum and minimum element, as noted above, so is connected. –  Thomas Andrews May 9 '13 at 21:09

The structure you are talking about is the Lindenbaum algebra of ZFC. It is indeed the case that, if $R$ is the Riemann hypothesis, and you could show that $R \leq \top$ in that algebra (following the convention where $\top$ is the least element and corresponds to theorems provable in ZFC), then $R$ is provable in ZFC.

Most mathematicians, however, are only interested in the question whether $R$ is true, not whether it is provable in ZFC. So if you showed it was provable in ZFC, even if you somehow avoided demonstrating a ZFC-proof, that would still be sufficient justification for accepting $R$, because provability-in-ZFC is sufficient for establishing the truth of a result in mainstream math.

As a similar example, the original proof for Fermat's Last Theorem used lemmas from algebraic geometry that were not proved in ZFC, although it was widely suspected that the proof could be simplified. Colin McLarty, a logician, has recently announced that sufficient versions of these lemmas are provable in ZFC, so in principle there is a ZFC-proof of FLT, but nobody has every written one in full. Nevertheless the original published proof of the solution, which uses techniques beyond ZFC, is completely accepted by number theorists.

-
Hm, I'm ignorant but just curious. I've always heard that ZFC is a very strong theory in which all of conventional mathematics can easily be formulated (all basic structures like the real numbers can be defined and have the usually assumed properties); most results require much less than the full power of ZFC. Results that cannot be proved in ZFC (like the Continuum Hypothesis) are considered more "might be assumed true" than "ought to be true". Now you are saying Wiles used things beyond ZFC, what? Or are you saying he used meta-arguments (like for Gödels incompletness results)? –  Marc van Leeuwen Jun 26 '13 at 12:58
In its original form, Wiles' proof used methods from algebraic geometry that rely on assumptions (Grothendieck universes) that are slightly stronger than ZFC. However, at the same time, it was believed that this was just a simplifying device, and that the same arguments could be modified by an expert to only use special cases of the algebraic geometry lemmas which are provable in ZFC. I see now that Colin McLarty has recently announced that FLT is provable in ZFC. He had been working on this for some time. –  Carl Mummert Jun 26 '13 at 13:07
Nice to know that, thanks a lot! –  Marc van Leeuwen Jun 26 '13 at 13:19

You might be interested in Noson Yanofsky's paper. On page 17 of this paper he discusses the work of R. Parikh paper Existence and feasibility in arithmetic that appeared in the Journal of Symbolic Logic: volume 36, pp. 494-508 in 1971. I have not read the latter paper but Yanofsky's paper is easy to read.

In Yanofsky's paper he discusses statements with very long proofs but with short proofs that the statements are provable.

-