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

236 Views Asked by At

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?

2

There are 2 best solutions below

3
On BEST ANSWER

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.

0
On

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.