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?
$\begingroup$
$\endgroup$
5
-
4$\begingroup$ 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. $\endgroup$– Zhen LinJan 12, 2011 at 15:22
-
$\begingroup$ 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))) $\endgroup$– Zirui WangJan 14, 2011 at 4:28
-
$\begingroup$ T $\not\vdash$ (Con(T) $\land$ (T $\vdash$ S $\lor$ T $\vdash$ ~S)) is always true because T $\not\vdash$ Con(T). $\endgroup$– Zirui WangJan 14, 2011 at 4:46
-
$\begingroup$ 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))))) $\endgroup$– Zirui WangJan 14, 2011 at 5:18
-
$\begingroup$ @ZhenLin: It seems obvious to me that he means independent of ZFC. What am I missing here? $\endgroup$– ZazMar 11, 2022 at 4:07
Add a comment
|
5 Answers
$\begingroup$
$\endgroup$
2
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.
answered Jan 12, 2011 at 19:14
-
13$\begingroup$ Of course, this is all assuming that ZFC is actually consistent... (-: $\endgroup$ Jan 12, 2011 at 19:36
-
$\begingroup$ @Arturo Magidin. Of course, this is all assuming that math works. $\endgroup$ Aug 18, 2021 at 4:28
$\begingroup$
$\endgroup$
8
(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.
answered Jan 12, 2011 at 19:50
-
1$\begingroup$ 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'... $\endgroup$ Jan 12, 2011 at 19:55
-
$\begingroup$ 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? $\endgroup$– Asaf Karagila ♦Jan 12, 2011 at 19:58
-
$\begingroup$ @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.) $\endgroup$ Jan 12, 2011 at 19:58
-
$\begingroup$ @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. $\endgroup$ Jan 12, 2011 at 20:02
-
1$\begingroup$ Oh! I forgot that an inconsistent theory proves all statements, of course. $\endgroup$– ZazMar 10, 2022 at 19:27
$\begingroup$
$\endgroup$
1
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.
-
1$\begingroup$ I've attempted to restate this proof in more detail (and in a symbolism that I think is easier to wrap one's head around than the prose here) in this answer. $\endgroup$ Feb 22, 2018 at 19:27
$\begingroup$
$\endgroup$
2
Yes.
If every statement was decidable, that would imply that every statement could be proven true or false, which contradicts Gödel's first incompleteness theorem.
If every statement's decidability was decidable, that would imply that every statement could be proven true, false, or undecidable. We could then define a method of classifying all statements as true or false: Enumerate all statements: When one is proven undecidable, add an axiom saying it is false. This is known as a Hilbert program and again was proven impossible by Gödel's first incompleteness theorem.
And so on for $n$-undecidable statements.
Proof of second sentence
Let $d(S)$ denote "we can prove S is decidable".
If we prove S, then we know that S is decidable. If we disprove S, then we know that S is decidable. I.e.:
$$ S \implies d(S), \ \ \ \neg S \implies d(S) $$
In the same fashion: If we prove $d(S)$, then we know that $d(S)$ is decidable. If we disprove $d(S)$, then we know that $d(S)$ is decidable.
$$ \ \ \ d(S) \implies \ \ d(d(S)), \ \ \ \ \ \neg d(S) \implies \ \ \ d(d(S)) $$
The line above implies (by modus tollens on each) that:
$$ \neg d(S) \impliedby \neg d(d(S)), \ \ \neg\neg d(S) \impliedby \neg d(d(S)) $$
So we conclude that if the decidability of S is itself undecidable, then: we can't prove S is decidable and we can't prove S is undecidable.
-
2$\begingroup$ "We could then define a new axiom that states that all undecidable statements are false." That doesn't actually work: such a system would be inconsistent, since if $P$ is undecidable then so is $\neg P$. A bit more work is required. $\endgroup$ Mar 11, 2022 at 2:16
-
1$\begingroup$ @NoahSchweber: Agh! Yes. I changed it to enumerate over statements. $\endgroup$– ZazMar 11, 2022 at 4:00
$\begingroup$
$\endgroup$
Yes. This is true for any first order statement by Church's theorem, not just statements with respect to ZFC. First order logic is semidecidable, in that every first order statement that can be proven has a sound, complete proof calculus; Valid statements will always be decidable, and can always be proven, though this may take quite a bit of computation.
Satisfiability is undecidable in general however. If a statement is satisfiable, sometimes it can be shown to be satisfiable with finite models, or forcing. If the statement itself and it's negation is demonstrably satisfiable, then you've just proved the statement isn't a universally valid statement. However, one of the result's of Church's theorem proves that there's no algorithm that you can rely on to terminate trying to check for satisfiability of an arbitrary first order statement, because otherwise it would solve the Entscheidungsproblem.
