6

Just a curiosity:

Is there an assertion of which a proof (formalizable, say, in ZFC) is not known but a proof that it's not undecidable (in ZFC) is known?

Edit: after the comments, I think the actual question was

Is there an ("interesting") assertion of which neither a proof (formalizable, say, in ZFC) of it or its negation is known but a proof that it's not undecidable (in ZFC) is known?

GH from MO
  • 98,751
Qfwfq
  • 22,715
  • 3
    Well, $0 = 1$ will do... There is no known proof that is formalizable in ZFC, but it is known that $ZFC \vdash \lnot(0 = 1)$, regardless of whether ZFC is consistent or not. (Since quid might scold me again for being unclear: I'm writing this because what you wrote is probably not what you meant...) – François G. Dorais Sep 08 '11 at 22:20
  • 6
    See David Speyer's answer here http://mathoverflow.net/questions/62144/are-the-millennium-prize-problems-all-decidable – Gjergji Zaimi Sep 08 '11 at 22:21
  • @GZaimi: thank you for the link, it's exactly in the spirit of what I (think I) was asking. The example given by D.Spyer clearly answers my question. If anybody knows other examples, answers are welcome. – Qfwfq Sep 08 '11 at 22:46
  • 4
    Any decidable but (so far) infeasible open problem. Such as: what is the 5th Ramsey number? (http://en.wikipedia.org/wiki/Ramsey_number) – Daniel Mehkeri Sep 08 '11 at 22:49
  • 3
    A simple way to put your question: "Is there an assertion in ZFC which is known to be decidable but has not been decided yet." The answer is YES, see the link in Gjergji Zaimi's comment. – GH from MO Sep 08 '11 at 22:49
  • Since it is established that any computationally infeasible problem will do, how about tweaking the question to ask about problems that are decidable, yet not obviously so? – Gjergji Zaimi Sep 08 '11 at 23:03
  • I see. Thanks to the various comments I notice that an answer to my question doesn't involve anything particularly "deep", but it's just a matter of cooking up a computationally challenging "problem". – Qfwfq Sep 08 '11 at 23:03
  • 3
    In fact deciding any decidable assertion is nothing more than a computationally challenging problem: one simply needs to generate all possible proofs in ZFC and find the one which decides the assertion. – GH from MO Sep 08 '11 at 23:11
  • 1
    Reposting a link mentioned in a previous comment so that it appears in the "Linked" questions list: Are the Millennium Prize Problems all decidable? [closed] – The Amplitwist Jan 24 '24 at 18:04

3 Answers3

13

If it's known that some statement $S$ is decidable in ZFC, then you can just run a computer program that enumerates all ZFC-proofs and stops when it finds a proof of $S$ or a proof of $\neg S$. By hypothesis, this algorithm is guaranteed to terminate. Therefore, the only possible obstacle separating decidable statements from decided ones is computational complexity.

In other words, the only possible instances of what you're looking for are statements that have already been proved up to a finite computation. Until they were actually proved, the Kepler Conjecture and Catalan's Conjecture were perhaps the most interesting examples of this type. I can't think of other examples of comparable interest offhand, but maybe others can.

Timothy Chow
  • 78,129
  • 4
    The odd Goldbach problem is only known for $n<10^{18}$ or $n>e^{3100}$, according to http://en.wikipedia.org/wiki/Goldbach%27s_weak_conjecture. – Kevin Ventullo Sep 09 '11 at 05:02
  • 4
    Another one which was of comparable interest until it was settled: Is there a simple group of order 808017424794512875886459904961710757005754368000000000 ? Clearly checkable by finite computation! – David E Speyer Sep 09 '11 at 13:48
  • @Timothy: Your response elaborates on my earlier comment above. – GH from MO Sep 09 '11 at 14:45
  • @GH: Sorry, I didn't see your comment until after I posted. (By the way, I had already made essentially the same comment in response to David Speyer's answer here: http://mathoverflow.net/questions/62144/are-the-millennium-prize-problems-all-decidable ) – Timothy Chow Sep 09 '11 at 20:21
  • @Timothy: That's all right, in fact it is always good to give more detail! – GH from MO Sep 14 '11 at 21:45
  • 1
    @KevinVentullo : A couple of years after you originally posted your comment, Helfgott announced a proof of Goldbach's weak conjecture. The proof seems to have been generally accepted, so that's another potential example that has "bitten the dust." – Timothy Chow Dec 12 '16 at 15:32
11

It shouldn't be hard to find a large number $N$ such that no one knows a proof that $N$ is prime and no one knows a proof that $N$ is not prime. Yet the question of the primality of $N$ can't be undecidable - there is a simple (if impractical) algorithm for deciding it.

Gerry Myerson
  • 39,024
  • 4
    How about a handsome tower of 2's plus 1? – GH from MO Sep 08 '11 at 22:55
  • Is $2^{43112621}-1$ prime? – Gerald Edgar Sep 09 '11 at 00:08
  • @Gerald: Hmm. I may be misinterpreting it, but my reading of http://www.mersenne.org/report_exponent/?exp_lo=43112600&exp_hi=43112699&B1=Get+status is that its Lucas–Lehmer residue, independently confirmed by two people (with another failed attempt), is nonzero, therefore the number is composite, even though no explicit factor is known. – Emil Jeřábek Sep 09 '11 at 10:58
  • 1
    @GHfromMO For that sort, we can make it even worse if instead of primality we ask whether the number has an even or odd number of distinct prime factors, and if we add a small amount to it to make sure that there isn't any hidden pattern involving numbers very close to powers of 2, then we could ask if 2^2^2^2^2^2^2 +35 has an even or odd number of distinct prime factors. This is decidable. But there also is likely not enough computational power in the observable universe to answer this essentially simple arithmetic question. – JoshuaZ Jan 25 '24 at 03:06
7

There's tons of assertions like that in finite combinatorics. For example the Ramsey numbers R(5,5) and R(6,6) can be "straightforwardly" (i.e. given impractically large computing resources) found by direct enumeration. It's known that $43\le R(5,5) \le 49$ and $102\le R(6,6)\le 165$. But Wikipedia's article on Ramsey theory quotes Joel Spencer:

Erdős asks us to imagine an alien force, vastly more powerful than us, landing on Earth and demanding the value of R(5, 5) or they will destroy our planet. In that case, he claims, we should marshal all our computers and all our mathematicians and attempt to find the value. But suppose, instead, that they ask for R(6, 6). In that case, he believes, we should attempt to destroy the aliens.

The article Graham's number has another interesting example.

The Amplitwist
  • 1,446
none
  • 71