Is it possible to nonconstructively prove that a statement can be proven or disproven within a formal system?

Question

I've heard of many examples of statements that have been proven to be independent of a formal system, meaning that they can't be proven within that formal system (for example, the Continuum Hypothesis is independent of ZFC). I've also heard of examples of proofs showing that certain proof techniques are not powerful enough to prove certain results, such as the result that proofs that relativize cannot resolve P versus NP.

This Stack Overflow question (which might be soon closed or migrated) asks whether we know whether it's possible to resolve P versus NP or not. That got me thinking of whether there are any examples of conjectures where we know that the conjecture can either be proven or disproven within some formal system, but where we don't actually know whether the conjecture is true or not. In other words, are there any conjectures where we can nonconstructively argue that the conjecture is either provable or disprovable, but where we don't know which of these is the case?

I apologize if this is a silly question - I don't have much background in proof theory or model theory.

Thanks!

Answer 1

Many. Such questions amount to some finite computation, since you can just search for a proof and simultaneously disproof until you find (enumerate all proofs and check if its a proof or disproof). So just pick one which requires a large computation such as; Is there an odd number of pairs of twin primes below 10^999999999999999 ? This is provable, just count them.

I cant prove there isnt some shortcut to this, but there are some statements where you can prove that the proof or disproof is longer then n for any n you choose, see here: https://en.wikipedia.org/wiki/G%C3%B6del%27s_speed-up_theorem

Answer 2

It's sometimes possible to show existence of proof of a statement in ZF by showing that the statement is true in ZFC, and arguing using absoluteness.

An example would be answer to this question, in which Andreas Blass argues as follows: for any model of ZF, Monsky's theorem holds in an inner model satisfying axiom of choice, and this statement is "simple enough" (involves only finitely many reals) to apply absoluteness, so it held in original model as well. So every model of ZF satisfies Monsky's theorem, hency by Godel's completeness theorem, ZF proves Monsky's theorem.

Note that this argument does not provide us a proof in ZF of Monsky's theorem, it only provides a proof in ZF that there is a proof in ZF on this theorem.

Edit: Actually, I have realized that I haven't answered exactly the question you asked (I thought you are asking for proof of existence of proof without providing one). I think the above proof technique might be applicable for your actual question, so I'll leave the answer here for now.