Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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?

share|improve this question
4  
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
add comment

4 Answers 4

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.

share|improve this answer
4  
Of course, this is all assuming that ZFC is actually consistent... (-: –  Arturo Magidin Jan 12 '11 at 19:36
add comment

(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.

share|improve this answer
    
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
add comment

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.

share|improve this answer
add comment

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?

Could you elaborate on your answer a little Qiaochu?

share|improve this answer
2  
The decidability Dec(S) of a statement S in ZFC is not a statement in ZFC; it's a statement in whatever metatheory you're using to study ZFC. So when you ask about its decidability, that question is a function of the metatheory. It doesn't have a notion of decidability in isolation, so the notions you've just defined are not well-defined. –  Qiaochu Yuan Jan 12 '11 at 15:26
    
Great, thanks for the clarification. I guess a little knowledge is a dangerous thing :) –  Simon Jan 12 '11 at 16:31
2  
@Qiaochu: This is not correct, I'm afraid. There is a straightforward (and standard) way of writing Dec(S) as a statement in the language of set theory. –  Andres Caicedo Jan 12 '11 at 17:09
    
@Andres: If you have time I would appreciate an answer clarifying this question. I was under the impression that any such statement would be a statement about models of ZFC internal to a model of ZFC and that this was different from a statement about models of ZFC. –  Qiaochu Yuan Jan 12 '11 at 17:42
2  
@Qiaochu: Any statement about provability within a recursive theory or decidability of provability from a recursive theory can be formalized as an arithmetic statement, so any theory that can interpret a bit of number theory (say, PA; certainly ZFC does this) can express this statement in its language. Now, of course, a different issue is whether what the theory has to say about the statement is true or not. (I wrote a brief answer to the question, hopefully you won't find it too brief.) –  Andres Caicedo Jan 12 '11 at 19:53
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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