Welcome to MathOverflow

Question

3

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?

edited Sep 8 2011 at 22:58

GH
15.7k●1●34●57

asked Sep 8 2011 at 22:10

Qfwfq
8,640●35●86

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 8 2011 at 22:20

5

See David Speyer's answer here mathoverflow.net/questions/62144/… – Gjergji Zaimi Sep 8 2011 at 22:21

3

Any decidable but (so far) infeasible open problem. Such as: what is the 5th Ramsey number? (en.wikipedia.org/wiki/Ramsey_number) – Daniel Mehkeri Sep 8 2011 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 Sep 8 2011 at 22:49

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 Sep 8 2011 at 23:11

show 4 more comments

Timothy Chow · Accepted Answer · 2011-09-09 00:25:42Z UTC

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.

Gerry Myerson · Answer 2 · 2011-09-08 22:50:59Z UTC

6

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.

answered Sep 8 2011 at 22:50

Gerry Myerson
15.8k●1●47●87

3

How about a handsome tower of 2's plus 1? – GH Sep 8 2011 at 22:55

Is $2^{43112621}-1$ prime? – Gerald Edgar Sep 9 2011 at 0:08

@Gerald: Hmm. I may be misinterpreting it, but my reading of mersenne.org/report_exponent/… 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 9 2011 at 10:58

none · Answer 3 · 2011-09-13 08:02:51Z UTC

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.

Is there an “undecided” assertion of which a proof that it’s not undecidable is known?

Remember to vote up questions/answers you find interesting or helpful (requires 15 reputation points)

3 Answers

You can accept an answer to one of your own questions by clicking the check mark next to it. This awards 15 reputation points to the person who answered and 2 reputation points to you.