Could there be an undecidable statement $S$ in ${\sf ZFC}$ of which one will never be able to prove its undecidability for principal reasons (ie we will never know that $S$ is undecidable)?

If this is a silly question, I apologise; feel free to vote to close. I'll remove it quickly.


One can never prove in ZFC itself that a given statement is independent of ZFC, because the assertion "$S$ is independent of ZFC" implies Con(ZFC), since every statement is settled by an inconsistent theory.

Thus, if a statement $S$ is independent of ZFC, then there is a model of ZFC inside of which $S$ is not independent of ZFC, since this is the situation inside any model of ZFC+$\neg$Con(ZFC).

For any given computably axiomatizable consistent theory $T$ extending ZFC, there are statements that are independent of $T$ and hence of ZFC, whose ZFC independence cannot be proved in $T$. Namely, the Rosser sentence $\rho$ for $T$. If $T$ is consistent, then $\rho$ is independent of $T$ and hence also of ZFC. But one cannot prove the assertion "$\rho$ is independent of ZFC" in the theory $T$, because in a model of T+$\neg$Con(T), there are proofs both of $\rho$ and of $\neg\rho$ in $T$, and depending on which proof has a smaller Gödel code, the model will have either $\rho$ or $\neg\rho$ being true, in a way that even a very weak theory can verify. So $\rho$ will not be independent of ZFC in that model of $T$.

Conclusion: no matter how much you strengthen ZFC, if you do so consistently, there will be ZFC independent statements whose ZFC-independence you cannot establish in your theory.

  • 2
    $\begingroup$ This is so meta... but I think the question was actually about "if ZFC is consistent then S is independent" being independent, since this is precisely how the independence statements are proven. $\endgroup$ – Wojowu Nov 23 '16 at 22:10
  • 1
    $\begingroup$ My remarks also apply to that statement, which is provably true from a weak theory in any model of ZFC+$\neg$Con(ZFC), as the hypothesis will be false and provably so. $\endgroup$ – Joel David Hamkins Nov 23 '16 at 23:37
  • 1
    $\begingroup$ And see also my update, which adds a conclusion for consistent strengthenings of ZFC, including the case of ZFC+Con(ZFC). $\endgroup$ – Joel David Hamkins Nov 23 '16 at 23:42
  • $\begingroup$ Would the same result hold if one formulated $ZFC$ in a paraconsistent meta-theory like $HF_{\infty}$ (Hyper-Frege +_" There is an infinite well-founded set"_? $\endgroup$ – Thomas Benjamin Nov 24 '16 at 23:48
  • 1
    $\begingroup$ My answer also applies to KM and its strengthenings, including the one you mention, by essentially the same argument. There seems to be no way around that phenomenon. $\endgroup$ – Joel David Hamkins Nov 25 '16 at 0:34

Here is a general statement:

If $X$ is the set of $\Pi_1$ statements of arithmetic (i.e., statements $P$ of the form $\forall n\in\mathbb{N}\,(Q(n))$ where $Q$ is arithmetic with bounded quantifiers), there exists no Turing machine $U$ which, given an element $P$ of $X$, (1) always halts, (2) returns "yes" if $P$ is a theorem of Peano arithmetic, and (3) returns "no" if $\neg P$ is a theorem of Peano arithmetic (or equivalently, if $\neg P$ is true, because a $\Sigma_1$ arithemetical statement like $\exists n\in\mathbb{N}\,(\neg Q(n))$, if true, is trivially provable).

(In other words, there is no program $U$ to decide which $\Pi_1$ statements of arithmetic are theorems and which are false, even if the program is allowed to answer whatever it wants — but it must still terminate — for a statement which is true but unprovable in Peano arithmetic.)

To see why this is, consider two Turing machines $T_1$ and $T_2$ which enumerate sets $S_1$ and $S_2$ which are disjoint (and provably so in Peano arithmetic) and recursively inseparable. Then for an integer $n$, the statement "$T_2$ never generates $n$" is $\Pi_1$. Now if we had a machine $U$ as above, we could run it on this statement, if it answers "no" then by (1) and (2) we know $n\not S_1$ (because if $T_1$ generates $n$ then Peano proves that $T_2$ does not), and if it answers "yes" then by (1) and (3) we know $n\not S_2$; so we are able to recursively separate $S_1$ and $S_2$, a contradiction.

Now what does this have to do with your question? We can construct a machine which, given a $\Pi_1$ arithmetical statement $P$, searches in parallel for: (A) a counterexample to $P$, (B) a proof of $P$ in ZFC, (C) a proof of "$P$ does not follow from Peano arithmetic" in ZFC and (D) a proof of "$P$ is consistent with Peano arithmetic" in ZFC"; if it finds (A) first, it stops and answers "no", if it finds (B) first, it stops and answers "yes", if it finds (C) first, it stops and answers "no", and if it finds (D) first, it stops and answers "yes". Assuming ZFC is arithmetically sound, this machine will answer "yes" for every theorem of Peano arithmetic (because the (B) search will terminate but (A) and (C) cannot), and "no" if $P$ is false (because the (A) search will terminate but (B) and (D) cannot). By the statement above, there must be $P$ for which it does not terminate, i.e., none of the three searches finds anything: this is a $\Pi_1$ arithmetical statement which (A) is true, (B) is not provable in ZFC, (C) for which ZFC cannot prove that it is not provable, nor even that it is not provable in Peano arithmetic and (D) for which ZFC also cannot prove that it is not refutable, nor even that it is not refutable in Peano arithmetic. So this is meta-undecidable in quite a strong sense; and it is clear, by adding further searches to the machine, that one can make this even stronger.

Furthermore, this can all be made completely explicit (by choosing effectively inseparable sets $S_1$ and $S_2$).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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