Return to Answer

$\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$.

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.

$\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.

$\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.

$\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$.

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.

$\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 $F+\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.

$\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.