The questions I'm going to ask are non formal because they concern decidability of decidability, and I couldn't find any references on that after some quick searches. I hope that this thread is still "formal enough" to be productive.

So, let us suppose that we're working with an ambient logic that is classical (we believe in LEM and induction principle), and that we were able to define some formal theory in our natural language that is strong enough to have undecidable statements.

Let $A$ be any proposition of this formal theory, and call $Dec(A)$ the proposition "there exists a proof of $A$ or there exists a proof of $\neg A$". $Dec(A)$ is true iff $A$ is decidable, $Dec(A)$ being false iff $A$ is undecidable.

Notice that because of LEM, $Dec(A) = Dec(\neg A)$.

What can we say about $Dec(Dec(A))$ ? (here begins the non formal stuff, supposing we have at our disposal some stratified ``infinite order logic'' that can speak about its own propositions and proofs (say, level $n$ propositions can speak about level $m \leq n$ propositions and proofs)).

If $Dec(A)$ is right, then there either exists a proof of $A$ or a proof of $\neg A$ that we can write down as a finite string of symbols. Thus, by finding such a proof, we proved that it is possible to find a proof of $A$ or that it is possible to find a proof of $\neg A$, hence $Dec(Dec(A))$ is true. By obvious induction, $Dec^n(A)$ true implies $Dec^{n+1}(A)$ true.

This leads us to the following definition of $n$-undecidability: A proposition $A$ is said to be $n$-undecidable iff there exists some positive integer $n$ such that for all $m \leq n$, $Dec^m(A)$ is false and $Dec^{n+1}(A)$ is true.

We can also define the notion of $\infty$-undecidability: We call $\infty$-undecidable, any proposition $A$ such that for all $n$, $Dec^n(A)$ is false.

Question: can we prove that an $\infty$-undecidable proposition exists ? Let $B$ = there exists an $\infty$-undecidable proposition. What can we say about $Dec(B)$ ?

If $Dec(B)$ is true, then we can either find a proof of $B$ or a proof of $\neg B$. Finding a proof of $B$ means to find a statement $C$ and to prove that for all $n$, $Dec^n(C)$ is false. This implies that $Dec^{n+1}(C)$ is true, and hence contradiction. If we can find a proof of $\neg B$, that is, a proof that there exists no $\infty$-undecidable statement, this means that for all statements $C$ we can find an $n$ such that $Dec^n(C)$ is true, and in particular, for $C = B$. Thus there exists an $n$ such that $Dec^n(B)$ is true and it therefore becomes decidable to know if it is decidable ... that there exists an $\infty$-undecidable proposition.

If $Dec(B)$ is false, what can we say about $Dec^n(B)$ for all $B$ ? It appears that there must exist some $m$ such that $Dec^m(B)$ is true too, or we would have found a proof that there exists an infinitely undecidable statement, and hence contradiction.

Any comment, recommandations, references about this stuff?

PS: it really looks like that one needs to have a theory that is able to speak about its own lower level propositions and proofs, say, an infinite order stratified language.

  • 6
    $\begingroup$ It seems to me that your question and the discussion would benefit from a greater level of precision in provability logic (e.g. see csc.villanova.edu/~japaridz/Text/prov.pdf), since the assertion Dec(A) is $\square A\vee\square\neg A$, and Dec(Dec(A)) is $\square(\square A\vee\square\neg A)\vee\square\neg(\square A\vee\square\neg A)$, and so on. Thus, your question is really about modal reasoning in the provability logic of your formal system. Which validities come out true will depend on iterated consistency assumptions in the background theory. $\endgroup$ Oct 28, 2014 at 1:41
  • 1
    $\begingroup$ For example, if $F$ is the formal system for your proofs, and we have F+Con(F) in our background, then the second case of Dec(Dec(A)) cannot occur, since we can have no proof in F that $\neg\text{Dec}(A)$, as this provably implies Con(F), which would violate the second incompleteness theorem under our assumption of Con(F). So in this case Dec(Dec(A)) amounts to "there is a proof of Dec(A)". $\endgroup$ Oct 28, 2014 at 2:12
  • $\begingroup$ But meanwhile, with $F+\neg\text{Con}(F)$ in the background, then all $\text{Dec}(A)$ come out true, and so also $\text{Dec}(\text{Dec}(A))$ and so on, trivializing the hierarchy. $\endgroup$ Oct 28, 2014 at 3:13
  • $\begingroup$ Does this imply that if you recursively choose as a background $F_n = F_{n-1} + Con(F_{n-1})$ you can instantly see that $B$ is true, where $B$ is ``there exists an $\infty$-undecidable proposition'' (and thus Dec(B) is true, even though you can't contruct any such $B$ explicitely) ? This would rejoin the comment of Fedya. PS : I wasn't aware of the fact that a proof of $\neg Dec(A)$ implies $Con(F)$, which is clearly a strong result there. $\endgroup$
    – sure
    Oct 28, 2014 at 12:58
  • $\begingroup$ Regarding your final remark, you haven't said it correctly. It isn't that "a proof of $\neg\text{Dec}(A)$" implies $\text{Con}(F)$, but rather just $\neg\text{Dec} (A)$ itself implies $\text{Con}(F)$. This is obvious, since if a statement is independent, then not everything is provable, and so the theory must be consistent. And regarding your first statement, yes, I would think you care most about the background in which those iterated consistency assumptions hold. Without that, your hierarchy will trivialize at some $n$. $\endgroup$ Oct 28, 2014 at 13:04

2 Answers 2


$\newcommand\Con{\text{Con}} \newcommand\Dec{\text{Dec}}$

Let $F$ be the formal system in which the proofs are to be carried out, when it comes to your formal assertions of the form $\Dec(\varphi)$. So we assume that $F$ is described by some computable axiomatization. For example, perhaps $F$ is simply the usual first-order PA axioms. Let me assume that $F$ is true in the standard model $\mathbb{N}$, which is probably a case that you care most about. (But actually, I believe it is sufficient in this argument to assume iterated consistency assertions about $F$.)

Let $A=\Con(F)$. I claim that this statement is $\infty$-undecidable with respect to $F$.

To see this, argue as follows. By the incompleteness theorem, since $\Con(F)$ is true, we know that $F$ does not prove $A$, and since $F$ and $A$ are both true, it also follows that $F$ does not prove $\neg A$. So $\neg\Dec(A)$ is true (that is, in the standard model $\mathbb{N}$). But $F$ by itself cannot prove $\neg\Dec(A)$, since $F$ proves $\neg\Dec(X)\to \Con(F)$, as an inconsistent theory has no undecidable statements, and so if it did it would violate the incompleteness theorem. Note also that $F$ cannot prove $\Dec(A)$ either, since $\neg\Dec(A)$ is true. Thus, $\neg\Dec(\Dec(A))$ is true. But $F$ cannot prove this, since then again it would prove $\Con(F)$, violating incompleteness, and it also cannot prove $\Dec(\Dec(A))$, since $\neg\Dec(\Dec(A))$ is true. So $\neg\Dec(\Dec(\Dec(A)))$ is true. And so on.

For the general step, if $\Dec^n(A)$ is false, then $F$ cannot prove this, since then it would prove $\Con(F)$, contrary to the incompleteness theorem, and it cannot prove $\Dec^n(A)$ either since it was false and $F$ is true, and so $\Dec^{n+1}(A)$ is false.

This reasoning shows that $\Dec^n(A)$ will be false for every $n$, and so $A=\Con(F)$ is $\infty$-undecidable, assuming that $F$ is true in the standard model.

It seems likely to me that the content of what it was about "true in the standard model" that the argument used should be covered by the assumption merely that $\Con^n(F)$ holds for all $n$. But I shall leave this to the proof-theoretic experts, who I hope will shed light on things.

Update. More generally, I claim the following.

Theorem. Assume that the formal system $F$ is true in the standard model of arithmetic $\mathbb{N}$. Then $\Dec(B)$ and $\Dec(\Dec(B))$ are equivalent for any statement $B$. So $\Dec(B)$ is equivalent to $\Dec^n(B)$ for any particular $n$ with respect to any such true formal system $F$.

Proof. Note that I am not claiming that this equivalence is provable in $F$, only that it is true in the standard model. You had already noted that $\Dec(B)$ implies $\Dec(\Dec(B))$. So assume $\Dec(\Dec(B))$ is true. Thus, it is true in $\mathbb{N}$ that either there is a proof in $F$ of $\Dec(B)$ or a proof of $\neg\Dec(B)$. It cannot be the latter, because then $F$ would prove its own consistency, as we have noted, contrary to the incompleteness theorem. Thus, it must be true in the standard model that "there is a proof of $\Dec(B)$." In this case, there really is a (standard) proof of $\Dec(B)$, and so $\Dec(B)$ is true. QED

Thus, once you have an undecidable statement, it is $\infty$-undecidable, with respect to any such system $F$ that is true in the standard model.

  • $\begingroup$ I think you want to leave out the $F+{}$ from the last paragraph, otherwise you are just reasserting that $F$ is true in the standard model in different words. $\endgroup$ Oct 28, 2014 at 15:27
  • $\begingroup$ Thanks, fixed! Do you agree with that point? I find it confusing to argue in those iterated consistency theories, without knowing that they are true in the standard model. $\endgroup$ Oct 28, 2014 at 15:33
  • $\begingroup$ Yes, it should be correct. I find it more clear if expressed in provability logic, as you suggested above: it is easy to show by induction on $n$ that $\mathrm{Dec}^n(A)$ is provably equivalent to $\Box^{n+1}\bot$ (well, apart from $n=0$). $\endgroup$ Oct 28, 2014 at 15:39
  • $\begingroup$ Actually, one does not even have to prove it :) $\mathrm{Dec}^n(A)$ is in any case expressed by a variable-free formula of provability logic, and being a positive combination of boxed formulas, it implies its own boxed version. Every such formula is equivalent over $\mathrm{GL}$ either to some $\Box^m\bot$, or to $\top$, but the latter is impossible if the original argument works for sound theories. $\endgroup$ Oct 28, 2014 at 15:47
  • 1
    $\begingroup$ That's a beautiful proof $\endgroup$
    – sure
    Oct 28, 2014 at 17:07

This answer is from the point of view of algorithmic decidability; I'm not sure how much of it carries over to other logical systems. So let's suppose our statements are strings in a finite alphabet and "$P$ is a proof of $A$" is a computable operation. I'm also supposing that if $Dec(A)$ holds, then there is indeed a proof of $A$ or $\neg A$; as @Joel David Hamkins points out, this is nontrivial.

Suppose that for every $A$ there is an $n$ such that $Dec^n(A)$ holds. Then we can have a machine that, for a given $A$, runs through every possible proof and checks whether it is a proof of $Dec^n(A)$ or a proof of $\neg Dec^n(A)$. Eventually, if we don't find a proof of $A$ or $\neg A$, we find a proof of $\neg Dec^n(A)$ for some $n \geq 1$: this is the lowest $n$ such that $Dec^{n+1}(A)$ holds, and we know for sure that $A$ is undecidable. So if an $\infty$-undecidable statement doesn't exist, the whole hierarchy collapses. Moreover, if the system is sufficiently powerful, this would give a solution to the halting problem. So a sufficiently powerful theory with these assumptions has to have $\infty$-undecidable statements (though I'm not sure if every theory which has undecidable statements is this powerful.)

Of course, this doesn't give us a particular $C$ which is $\infty$-undecidable.

  • $\begingroup$ Thanks for this answer. This doesn't give us any particular $C$ which is $\infty$-undecidable, and there's even no way to construct such as far as I understand. $\endgroup$
    – sure
    Oct 28, 2014 at 12:47
  • $\begingroup$ Your statement "a sufficiently powerful theory has to have $\infty$-undecidable statements" is not correct, since if $F$ is sufficiently powerful and consistent, then $F+\neg\text{Con}(F)$ is even more powerful, but has no $\infty$-undecidable statements, since this theory thinks that everything is provable in it, and so it has $\text{Dec}(A)$ for every $A$, even though it is actually consistent by the incompleteness theorem. $\endgroup$ Oct 28, 2014 at 13:16
  • $\begingroup$ Ah, so my claim only works for theories in which $Dec(A)$ being true actually implies that there is a proof of $A$ or $\neg A$. $\endgroup$
    – Fedya
    Oct 28, 2014 at 13:30
  • $\begingroup$ I don't follow your remark, because Dec (A) asserts exactly that A is provable or not A is provable. Perhaps your answer would be more clear with a greater distinction between your meta theoretic consistency assumptions and the theory to which Dec is referring. $\endgroup$ Oct 28, 2014 at 14:13

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.