3
$\begingroup$

There are several problems which have been shown to be unprovable in ZFC. Has there ever been a case of the opposite? That is, has it ever been proven for some statement $\varphi$ that $\text{ZFC} \models \varphi$ or $\text{ZFC} \models \neg \varphi$, without actually proving which one is true? If not, would it make sense for a proof like this to exist or is it unlikely that something like this will ever happen?

edit: As mentioned by the two answers I was not clear enough what I am looking for. I meant a statement for which it was not clear at first whether it is unprovable but then it was shown that a proof or disproof exists, without immediately finding it. The particular statement which causes me to think about this is P=NP.

$\endgroup$
3
  • $\begingroup$ Doesn't this follow for all unproven sentences from the completeness theorem for first order logic together with the law of excluded middle? $\endgroup$ – Nikolaj-K Jan 16 '15 at 9:57
  • 1
    $\begingroup$ @NikolajK: No it doesn't. I think you're confusing completeness of the logic (which is true) with the particular theory ZFC being complete (which it isn't). $\endgroup$ – hmakholm left over Monica Jan 16 '15 at 10:07
  • 2
    $\begingroup$ @NikolajK: $\varphi\lor\neg\varphi$ will of course be true in all models, but it may be that there are some models of the theory where $\varphi$ is true and other models where $\neg\varphi$ is true. In that case neither $\varphi$ nor $\neg\varphi$ can be provable from the theory. $\endgroup$ – hmakholm left over Monica Jan 16 '15 at 11:54
4
$\begingroup$

This question is not well-formulated as it stands. I will give you a trivial example of such a formula: $$402439 \times 284665 = 114560397935.$$ It is clear for general reasons, that ZFC either proves this true or proves it false. However, I feel it is safe to say that it is not currently known which of these cases holds.

You will of course - quite reasonably - object that there exists an algorithm that determines which case holds.

However, more generally, this will always be the case in your situation. The algorithm to determine which of $\varphi$ and $\lnot \varphi$ is provable is simply to start systematically writing down all possible proofs in ZFC. Eventually, one of the two formulas $\varphi$ or $\lnot \varphi$ will come up, and at that point you'll have your answer.

Now it is true that there is a gulf, in terms of computation time, between the two examples I've presented. But what do you make of this?

(1) The game of chess is winnable for White.

Nobody knows a proof of this (or its negation), but it is clear that with enough computation time, we could get the answer. Would you put this in the category of questions about simple arithmetic, or the category of more difficult questions?

My point has been to illustrate that, given a particular $\varphi$, a meaningful answer to your question will generally involve reference to the computation time it would take to answer which of $\varphi$ or $\lnot \varphi$ is provable.

Edit. To respond to the last part of the question, Goldbach's weak conjecture, that every odd integer greater than or equal to $7$ is the sum of three primes, was proved in 2013 by Helfgott. In 1937, Vinogradov had proved this true for all odd integers greater than some constant $C$, and around 1947, an explicit, but enormous, value for $C$ was found. So between 1947 and 2013, it was clear that the weak conjecture was either provable or disprovable, but it wasn't known which one.

$\endgroup$
5
  • $\begingroup$ You are right and I should have specified my question. Do you know any examples where the (dis)provability was not clear at first but has then been shown? $\endgroup$ – Andreas T Jan 16 '15 at 10:33
  • $\begingroup$ 1.e4 e5 2.Qh5 Nc6 3.Bc4 Nf6 4.Qxf7# is a win for white, so that the game is winnable for white at all doesn't seem too hard to prove :-) $\endgroup$ – RemcoGerlich Jan 16 '15 at 12:19
  • $\begingroup$ Regarding your edited section: This seems odd to me. How would the existance of one constant imply that there is a proof or disproof? I would expect that this is intuition and expectation rather than an actual proof, similar to the situation if you show some property for all numbers up to a million and expect that it is probably true for every natural, but you did not actually prove it. $\endgroup$ – Andreas T Jan 16 '15 at 16:01
  • $\begingroup$ @RemcoGerlich: What that word usually means is that no matter how Black plays, there's a way for White to win. $\endgroup$ – hmakholm left over Monica Jan 16 '15 at 16:02
  • $\begingroup$ @AndreasT: The conjecture has the property that checking it for any given number is a simple matter of computation. Thus, if it is false, then there is a counterexample and so it is provably false. And after Vinogradov it was known that the conjecture is true for all numbers above $C$, so if it is true, it would have a proof that consists of Vinogradov's proof plus a checking that all number below $C$ has the property. The difference from your analogy is that you have a general proof that all numbers greater than a million has the property. $\endgroup$ – hmakholm left over Monica Jan 16 '15 at 16:05
10
$\begingroup$

It is easy to see that ZFC either proves or disproves $$ \sin\left(10^{10^{100}}\right) > 0 $$ but we have no idea whether one or the other is the case.

This may seem like cheating, in that finding out whether it is provable or not is just a matter of computing a googol digits of $\pi$ and reducing. However all examples will have more or less this property. As soon as we know that either $\varphi$ or $\neg\varphi$ is provable, we can in principle find out which is the case in finite time, just by enumerating all proofs from ZFC until we hit one that concludes either $\varphi$ or $\neg\varphi$.

$\endgroup$
10
  • $\begingroup$ You are right and I should have specified my question. Do you know any examples where the (dis)provability was not clear at first but has then been shown? $\endgroup$ – Andreas T Jan 16 '15 at 10:33
  • $\begingroup$ @AndreasT: I'm sure we could concoct one, using a function that it took some time to show is computable. But that's just cheating to the second order. So what you really want might be a sentence that contains no obvious parameters -- but that's a hard concept to make rigorous. $\endgroup$ – hmakholm left over Monica Jan 16 '15 at 10:41
  • $\begingroup$ "cheating to the second order" -- I wonder whether, perhaps via imposter syndrome, all mathematics is cheating to some finite order ;-) $\endgroup$ – Steve Jessop Jan 16 '15 at 10:46
  • 1
    $\begingroup$ @SteveJessop: In most other sciences perhaps -- but in mathematics we really ought to be capable of transfinite cheating at least for recursive-ordinal orders. $\endgroup$ – hmakholm left over Monica Jan 16 '15 at 11:03
  • $\begingroup$ Sorry for the off, but I have idea: $sin{10^{10}}$ is yet calculable (numerically), and then using $sin{2x}$ and $sin{x+y}$ multiple times also the final result could be calculated, I think. $\endgroup$ – peterh - Reinstate Monica Jan 16 '15 at 12:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.