# Is there a statement whose undecidability is undecidable?

We know there are statements that are undecidable/independent of ZFC. Can there be a statement S, such that (ZFC $\not\vdash$ S and ZFC $\not\vdash$ ~S) is undecidable?

-
Can you define exactly what you mean by "$\mathrm{ZFC} \vdash S$ is undecidable"? It's meaningless to say that ask whether "$\mathrm{ZFC} \vdash S$" is independent, because you haven't asked what it's independent of. –  Zhen Lin Jan 12 '11 at 15:22
Con(T) => (T $\not\vdash$ (Con(T) => T $\not\vdash$ S $\land$ T $\not\vdash$ ~S) $\land$ T $\not\vdash$ (Con(T) $\land$ (T $\vdash$ S $\lor$ T $\vdash$ ~S))) –  Zirui Wang Jan 14 '11 at 4:28
T $\not\vdash$ (Con(T) $\land$ (T $\vdash$ S $\lor$ T $\vdash$ ~S)) is always true because T $\not\vdash$ Con(T). –  Zirui Wang Jan 14 '11 at 4:46
Version 2: Con(T) => (Con(T + (Con(T) => (Con(T + S) $\land$ Con(T + ~S)))) $\land$ Con(T + (Con(T) $\land$ (~Con(T + S) $\lor$ ~Con(T + ~S))))) –  Zirui Wang Jan 14 '11 at 5:18

At least one version of this question has a nearly-trivial answer; if you want to know if there's some statement G such that ZFC (or your PA-compatible logic system of choice) doesn't prove G, ZFC doesn't prove ~G, and we can't prove that ZFC doesn't prove G or not G, then any undecideable statement works!

Specifically, it's impossible for ZFC to prove that it can't prove something, because such a statement is tantamount to the consistency of ZFC; if ZFC were inconsistent then it could prove everything, so proving that there's something that can't be proved is equivalent to proving the consistency of ZFC, and of course this is forbidden by the second incompleteness theorem.

-
Of course, this is all assuming that ZFC is actually consistent... (-: –  Arturo Magidin Jan 12 '11 at 19:36

(Zhen: Independence is with respect to ZFC.)

Given any sentence S, either (1) ZFC proves S, in which case it is a theorem of ZFC that ZFC proves S, or (2) ZFC does not prove S. In this case, ZFC is consistent, and ZFC does not know that it does not prove S (or else it would know that it is consistent, and therefore it wouldn't be, but then it would prove S). So, in this case ZFC does not prove that it does not prove S, and does not prove that it proves S. It follows easily that "ZFC proves S" is independent of ZFC, for any S for which ZFC does not prove S.

To ask whether the statement "ZFC proves S" or a variant of this such as (+): "ZFC does not prove S and does not prove not-S" is decidable, on the other hand, is silly, unless you are using the term in a strange fashion. For any S there is a Turing machine M with no input that outputs the truth value of the statement (+). You do not ask for the decidability of a single statement, but of a family of statements, say with S as a parameter. You probably need to clarify what you mean.

The only sensible way of understanding what you are asking is to take the set whose sole element is a sentence formalizing the statement (+), and asking whether that set is decidable, but of course it is as any finite set (of natural numbers) is trivially decidable. Perhaps more interesting is whether, calling the (formalization of the) statement in quotes $(+)_S$, the set $A=${$S\mid(+)_S$} is decidable.

Now: Suppose first that ZFC is inconsistent. Then ZFC proves anything, so all the statements $(+)_S$ are false. Hence, the set $A$ is obviously decidable. Suppose now that ZFC is consistent. Let S be undecidable. Then if a machine solves $A$, it would tell us, upon inputting S, that S is independent. Since the set of independent (of ZFC) statements is independent, we are done: $A$ is undecidable.

Perhaps you want to know whether ZFC proves that A is decidable, or if it proves that A is undecidable. Note that if ZFC proves that A is undecidable, then the argument above (formalized within ZFC) tells us that ZFC knows that ZFC is consistent. In this case, ZFC is inconsistent, and it proves anything.

Suppose, then, that ZFC proves that A is decidable. This is possible if ZFC is inconsistent. So, suppose that ZFC is consistent. Then the argument above tells us that ZFC proves that ZFC is inconsistent.

This is not expected to be the case, as it tells us that ZFC is wrong about arithmetic statements. If ZFC is a "true" theory, meaning, if the arithmetic consequences of ZFC are true about the natural numbers, then ZFC cannot prove that A is decidable, and "A is decidable" is independent. Of course, if ZFC is not a true theory, I do not think it is too interesting whether it proves something or other about A.

We can further complicate things by considering models of ZFC, and checking whether the model thinks that ZFC proves that A is decidable, or not, or any of the posisble variants suggested above. We can in fact, assuming mild consistency requirements on ZFC, check that there are models of ZFC that disagree on whether ZFC proves that A is decidable, proves that it is undecidable, or does not prove either.

-
Andres: you're talking about the formal concept of 'decidability of membership in a set', whereas I suspect the poster is using an informal concept of decidability, i.e. 'P is decidable' is being used as a shortcut for 'the axioms of my theory can either prove P or prove ~P'... –  Steven Stadnicki Jan 12 '11 at 19:55
Andres, great answer. I'm wondering now, if we say that "ZFC proves S" is independent, can we force it and thus force S, or when we force S it's enough to force "ZFC proves S"? What about S which is inconsistent with ZFC, if ZFC cannot prove it, then "ZFC proves S" is independent, can we force that statement? –  Asaf Karagila Jan 12 '11 at 19:58
@Steven: Yes, I figured. This is why I first address the issue of independence from the theory, to make sure I cover both options. (After all, understanding "decidability" in the usual computability-theoretic sense gives us a more interesting question, after a fashion.) –  Andres Caicedo Jan 12 '11 at 19:58
@Asaf: Hi! No, unfortunately we cannot with forcing change the truth value of arithmetic statements (by Shoenfield's absoluteness theorem). If by forcing we obtain a model where ZFC proves blah, then in fact ZFC proved blah in the ground model. Of course, it may be that we manage to prove that "ZFC proves blah" by forcing it. I do not think I know of any actual instances of this, though. For arithmetic statements (not just consistency statements or somesuch), independence from ZFC is usually better handled by the techniques developed by Harvey Friedman. –  Andres Caicedo Jan 12 '11 at 20:02
Oh yeah, for a minute I forgot we are talking about arithmetic statements and not general statements. ;-) –  Asaf Karagila Jan 12 '11 at 20:09

This answer is a response to Simon's answer. It's trivial to show that any statement that's 2-undecidable is 3-undecidable. For instance take any statement S, then

(1)Suppose S is decidable, then its undecidability is decidable.

(2)Suppose the undecidability of S is undecidable, then from (1), S is undecidable.

(3)Suppose the undecidability of S is undecidable but the undecidability of its undecidability is decidable, then it can be shown that the undecidability of S is undecidable, and from (2), this means it can be shown that S is undecidable. Thus the undecidability of S is decidable which contradicts the assumption that the undecidability of S is undecidable.

Thus for any statement S, if its undecidability is undecidable, necessairily the undecidability of it's undecidability is undecidable.

It can also be shown that if S is 3-undecidable, then it's 4-undecidable as follows.

Let T be the statement S is undecidable. Now suppose S is 3-undecidable, then T is 2-undecidable so T is 3-undecidable so S is 4-undecidable.

-

I've wondered about this before. Call a statement whose undecidability is undecidable 2-undecidable. If such statements exist, one is naturally led to consider whether there exist statements such that the 2-undecidability of the statement is undecidable. Call this 3-undecidability. Do there exist $\omega$-undecidable statements?