Is there any conjecture that we know is provable/disprovable but we haven't found a proof of yet?

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?

• Wouldn't proving that a proof exists constitute a proof? – Shaun May 9 '17 at 18:45
• @Shaun: Yes, but I'm taking about a proof that either a proof of the conjecture exists or a proof that the conjecture is false exists (a proof that it is not independent). – Abc May 9 '17 at 18:48
• Ah, I see. Sorry. – Shaun May 9 '17 at 18:49
• Tarski came up with an axiomatization of Euclidean geometry which is decidable. Thus, any conjecture in Euclidean geometry is of this form, subject to the constraint that it is expressible in Tarski's system. – John Coleman May 10 '17 at 1:49
• The following paper proves that if Dickson's conjecture (a generalization of the twin prime's conjecture) is true then there exists an extension of Presburger arithmetic which is still decidable but is strong enough to express a variation of Goldbach's conjecture (namely that all even numbers can be expressed as the sum or difference of 2 primes): arxiv.org/pdf/1601.07099.pdf . – John Coleman May 12 '17 at 18:33

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.

• Right, you need to pick an enumeration that doesn't miss any proofs. – Eric Wofsey May 10 '17 at 2:04
• @gardenhead It's the same issue as e.g. trying to list all the rational numbers. If I start counting 1,2,3, ... I'll never get to 1/2. – Carmeister May 10 '17 at 3:15
• @gardenhead But we can enumerate all possible proofs by considering a proof written in ascii, look at the binary representation, concatenate all of the bytes together, and we get a natural number written in binary. Then to enumerate them, just count up from 1. Most of those numbers wont be valid proofs, but the enumeration will catch all that are. – Shufflepants May 10 '17 at 14:25
• "Finite" is one of those things that powerful complete proof systems struggle with; the Godel sentence being consistent both true and false is a symptom. So you could have a proof in your formal system that either the proof for P or the proof for not P exists, yet the algorithm to find it would actually run forever. (and assuming the proof for P exists, and the proof for not P exists, are both consistent with your axiom system!) – Yakk May 10 '17 at 14:46
• @gardenhead, countable doesn't necessarily imply that a computer can wrangle it. If you have a system and say something along the lines of "every python program that halts is an axiom" then there may be countably many axioms but a computer still can't check a proof. – Mark S. May 10 '17 at 19:34

Eric Wofsey's answer is certainly more comprehensive, but I thought I'd provide an example where the assurance that there's a proof of $P$ or $\neg P$ that's not of the form "there's a straightforward, if tedious, algorithm to check things" as there is in the case of Ramsey Theory or who wins a game like Chess.

The question is that of the "kissing number" for dimension 5 (or anything higher except 8 or 24). In 1d, two intervals of the same length can touch a third without overlapping. In 2d, 6 circles of a given radius can touch a 7th. We don't know the highest number of 5d spheres of a fixed radius that can all touch the same one, but the answer is between 40 and 44, inclusive. Since we're dealing with real numbers, I'd argue there's no obvious algorithm like with Ramsey Theory: we can't just test all of the possible centers of spheres.

However, because this kind of question can be translated into a simple statement about real numbers (think about using dot products to deal with the angles, for instance), it only depends on what things are true in any "real-closed field" (a field that acts like the real numbers for many algebraic purposes).

The thing is, the theory of real-closed fields is complete and decidable! Everything you can phrase in the language of real-closed fields can in theory be proven true or false with an algorithm, and they're even relatively efficient.

This example is not my own, and is discussed in a number of places, including these slides on "Formal Methods in Analysis" by Jeremy Avigad.

• What do you mean by 6 circles can touch a 7th without overlapping? Do they have the same radius or something? – NSZ May 10 '17 at 15:45
• @NSZ, sorry about the confusion. Yes, everything should have the same radius. The Wikipedia page I linked for the kissing number problem has more precise descriptions, as well as some pictures. – Mark S. May 10 '17 at 15:50
• Your answer and the other one by Eric Wofsey give a sentence that is parametrized by a natural number, such that we know it is provable for some parameter from a finite set, but for which we don't actually have a proof yet. I'm curious to know if there is a similar example where we know the explicit sentence. By the way, according to this RCF quantifier elimination is doubly-exponential, so is that what you mean by "relatively efficient"? =) – user21820 May 10 '17 at 16:30
• @user21820, a sentence stating something like "the kissing number for dimension 5 at least 41" would be something we have yet to prove or disprove. As far as "relatively efficient" goes, I'm far from an expert, but it appears the "$\exists xy$ rephrasing on the wikipedia page for the problem can use a pspace algorithm for existential statements (see this for one source), but maybe the conversion to that form adds so much complexity that it's not worth it. – Mark S. May 10 '17 at 16:57
• Yes I should have been more precise; is there a sentence of this sort where it is known to be provable (not just decidable) but we haven't found an explicit proof yet? As for the algorithm for this particular problem, I'm also not an expert so I'm not claiming anything about its efficiency. =) – user21820 May 10 '17 at 18:04

Could such a proof of dependence even exist, or would the only way of proving that a statement is dependent be proving/disproving it?

I'd like to address this specific question. It is not true in general that a existence of a proof of $P$ implies that $P$ itself is true. Neither is it true that existence of proof of provability of $P$ implies the provability of $P$. By Lob's theorem, each of these fails for some sentence $P$, if your foundational system is strong enough (ZFC set theory is certainly more than enough). To be 100% precise:

Take any formal system $S$ that satisfies the Hilbert-Bernays provability conditions, where $\def\box{\square}$"$\box_S P$" denotes the uniform arithmetical sentence representing "$S$ proves $P$", and we just write "$\box P$" if it is in the context of "$S \vdash \cdots$". Then the external form of Lob's theorem (L* in the linked post) asserts that if $S \vdash \box P \to P$ then $S \vdash P$. If $S$ is consistent, then $S \nvdash \bot$ and hence $S \nvdash \box \bot \to \bot$. Read in English, this shows that $S$ does not always prove that provability implies truth, even for individual sentences one at a time.

More can be said. If $S \vdash \box \box P \to \box P$ then by (L*) again we get $S \vdash \box P$. If $S$ is $Σ_1$-sound then $S \nvdash \box \bot$, so $S \nvdash \box \box P \to \box P$ does not hold when $P = \bot$. In English, S does not even prove that existence of proof of provability implies provability.

Strangely, it could even be possible (but no logician believes so) that ZFC is consistent but proves ¬Con(ZFC), which literally means that ZFC proves the existence of a proof of contradiction over ZFC even though there is no such proof...

More specifically, (in very weak meta-systems) we can easily prove that if ZFC is consistent then ZFC' = ZFC+¬Con(ZFC) is also consistent but yet ZFC' proves ¬Con(ZFC'). Of course, anyone who believes that ZFC is consistent ought to reject ZFC' because it denies its own consistency. But the problem is that we cannot ever figure out whether ZFC itself is already like ZFC' in being consistent but $Σ_1$-unsound, unless we actually find something like a concrete proof over ZFC of ¬Con(ZFC). But we actually hope that ZFC is $Σ_1$-sound, in which case we can never establish it non-circularly.

Now to explicitly answer the question interpreted externally, it is possible that $S \vdash \box P \lor \box \neg P$ and yet $S \nvdash P$ and $S \nvdash \neg P$, so 'proof of dependence' is not necessarily a reliable indicator of actual dependence! Here is one general explicit construction:

Take any $Σ_1$-sound formal system $S$ that satisfies the Hilbert-Bernays provability conditions. Let $S' = S + \box_S \box_S \bot$. Then we have:

• $S' \vdash \box_{S'} \box_S \bot \lor \box_{S'} \neg \box_S \bot$, since $S' \vdash \box_S P \to \box_{S'} P$ for any sentence $P$ over $S$.

• $S' \nvdash \box_S \bot$, otherwise $S \vdash \box_S \box_S \bot \to \box_S \bot$, and hence $S \vdash \box_S \bot$ by (L*), contradicting the $Σ_1$-soundness of $S$.

• $S' \nvdash \neg \box_S \bot$, otherwise $S \vdash \box_S \box_S \bot \to \neg \box_S \bot$, but $S \vdash \neg \box_S \box_S \bot \to \neg \box_S \bot$ by (D3), and hence $S \vdash \neg \box_S \bot$, contradicting Godel's incompleteness theorem.

• I'm not sure how you're applying Löb's theorem in your first statement. If your formal statement is $\omega$-consistent (which, as you mention, is a stronger statement than simply consistency) then proving that a proof exists implies that, in fact, a proof "actually" exists, which implies truth of the statement if your system is sound. Löb's theorem says that assuming the existence of a proof does not help much in the proof finding process. – cody May 10 '17 at 20:30
• @cody: I slipped a bit; although my first statement was correct when interpreted as "in general $S$ does not prove ( $\box \box P \to P$ )", and can be proven, it was not what I had in mind. I have also expanded my post to give the technical details. – user21820 May 11 '17 at 15:58
• Your first paragraph seems to use "true" in a confusing way. Presumably each instance of "true" really means "a consequence of S", and not truth in some unspecified model (or even a philosophical sense), since all the following statements are qualified $S \vdash$ or $S \nvdash$ or "$S$ does not prove"? In the context of a model of $S$, if $S$ can prove a proof of $P$ exists, then it is true a proof exists, which means $S$ can prove $P$, and therefore $P$ is true. – aschepler Aug 14 '18 at 11:12
• @aschepler: My first paragraph is using "true" within the meta-system. In general, statements in mathematical logic are asserted in the meta-system unless otherwise stated. And the last sentence of your comment is wrong because it is possible as explained in my post that $S$ is consistent but proves ( $S \vdash P$ ) even though $S \nvdash P$. This is a basic result obtainable from Godel's argument, and in my post I even gave an example in my last paragraph. – user21820 Aug 14 '18 at 11:38
• @user21820 Not sure I entirely get this still. So does that mean $S$ would not be sound, since it can prove the false statement $S \vdash P$? Don't we usually talk about theories that are consistent and sound (but often not complete) unless otherwise noted? – aschepler Aug 14 '18 at 23:35