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.



Decidability of decidability
$\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.


