I know that there are a lot of unsolved conjectures, but it could possible for them to be independent of ZFC (see Could it be that Goldbach conjecture is undecidable? for example).
I was wondering if there is some conjecture for which we have proved that either a proof of it or a proof of its negation exists, but we just haven't found that proof yet.
Could such a proof of dependence even exist, or would the only way of proving that a statement is dependent be proving/disproving it?
Best Answer
There are plenty of problems in mathematics which can be done by a finite computation in principle, but for which the computation is too large to actually carry out and we don't know of any shortcut to let us find the answer without (more or less) computing it by brute force. For instance, the value of the Ramsey number $R(5,5)$ is unknown, even though it is known that it must be one of the numbers $43,44,45,46,47,$ or $48$. We know that a proof of which number it actually is exists, since you can in principle find the answer by an exhaustive search of a finite (but very very large) number of cases.
Another example is solving the game of chess. We know that with perfect play, one of the following must be true of chess: White can force a win, Black can force a win, or both players can force a draw. A proof of one of the cases must exist, since you can just examine all possible sequences of moves (there are some technicalities about repeated positions but they don't end up mattering).
In fact, every example must be of this form, in the following sense. Suppose you have a statement $P$ and you know that either a proof of $P$ exists or a proof of $\neg P$ exists (in some fixed formal system). Then there is an algorithm which you can carry out to determine whether $P$ or $\neg P$ is true (assuming your formal system is sound, meaning that it can only prove true statements): one by one, list out all possible proofs in your formal system and check whether they are a proof of $P$ or a proof of $\neg P$. Eventually you will find a proof of one of them, since a proof of one exists. So this is a computation which you know is guaranteed to be finite in length which you know will solve the problem.