*I have moved this question here from MSE, because I did not receive any answers as of yet over there.*


I know that there are statements that are neither provable nor disprovable within some set of axioms, and I also know that such statements are called undecidable. Please allow me to call these statements to be undecidable to the first order. These statements belong to $U\_1$.


I was wondering if there is some kind of generalization of this concept. 



> 
> Question 1. Are there any conjectures/statements of which we can prove that we cannot prove whether it is decidable or not? Related: how would such a proof look like?
> 
> 
> 


Such a statement/conjecture would be undecidable to the second order, or belong to $U\_2$. 
Generalizing even further 
(Question 2):



> 
> What about statements that are in $U\_\infty$ ?
> 
> 
> 



Questions regarding "second and higher-order-undecidability"
Let $T$ be a fixed theory (recursively axiomatized, extending $I\Delta\_0+\mathrm{EXP}$, sound). I read your first question as:



> 
> Q1: Is there a sentence $A$ such that $T$ proves that “$T$ does not prove ‘$T$ proves $A$ or $T$ proves $\neg A$’ and $T$ does not prove ‘$T$ does not prove $A$ and $T$ does not prove $\neg A$’”?
> 
> 
> 


The answer is no, by Gödel’s theorem: if $T$ does not prove some formula, then in particular $T$ is consistent, hence a positive answer would imply that $T$ proves its own consistency. In light of this argument, we can make the question more sensible by putting enough consistency of $T$ in the assumptions:



> 
> Q1’: Is there a sentence $A$ such that $T$ proves that “If $T$ + ‘$T$ is consistent’ is consistent, then $T$ does not prove ‘$T$ proves $A$ or $T$ proves $\neg A$’ and $T$ does not prove ‘if $T$ is consistent, then $T$ does not prove $A$ and $T$ does not prove $\neg A$’”?
> 
> 
> 


The answer is yes, and the convenient way to solve this and similar question is to use [provability logic](http://en.wikipedia.org/wiki/Provability_logic).


The basic provability logic works with the language of propositional modal logic: we have propositional variables $p\_0$, $p\_1$, $p\_2$, ..., Boolean connectives such as $\land$, $\lor$ and $\neg$ (including the constants $\bot$ and $\top$ for falsity and truth), and the unary modal connective $\Box$. We also define $\Diamond A=\neg\Box\neg A$. An arithmetical interpretation of this language is an assignment $\*$ of an arithmetical sentence $p^\*$ to every propositional variable $p$, which is extended to all modal formulas by making it commute with Boolean connectives, and putting $(\Box A)^\*=\Pr\_T(\ulcorner A^\*\urcorner)$, where $\Pr\_T$ is the formalized provability predicate for $T$. That is, we read $\Box A$ as “$A$ is provable in $T$”, and $\Diamond A$ as “$A$ is consistent with $T$”. In particular, $\Diamond\top$ translates to “$T$ is consistent”.


$\DeclareMathOperator\prl{PRL}$
Then, the provability logic of $T$ with respect to a metatheory $S$, denoted $\prl\_S(T)$, is the set of all modal formulas $A$ such that $S\vdash A^\*$ for every arithmetical interpretation $\*$. The two most important special cases are the ordinary provability logic of $T$, which is $\prl(T):=\prl\_T(T)$, and the true provability logic of $T$, which is $\prl^+(T):=\prl\_{\mathrm{Th}(\mathbb N)}(T)$ (here, $\mathrm{Th}(\mathbb N)$ is the true arithmetic, i.e., the set of all arithmetical sentences true in the standard model).


The modal logics $\prl\_S(T)$ have been completely characterized for all sufficiently strong theories $T,S$. In particular, under our assumptions, $\prl(T)$ is the so-called Gödel–Löb logic GL, and $\prl^+(T)$ is Solovay’s logic S. Both logics are decidable, and they have transparent Kripke semantics.


Now, a moment’s reflection shows that Q1’ is equivalent to:



> 
> Q1’’: the formula $B:=\neg\Box[\Diamond\Diamond\top\to\neg\Box(\Box p\lor\Box\neg p)\land\neg\Box(\Diamond\top\to\neg\Box p\land\neg\Box\neg p)]$ is not in $\prl^+(T)$.
> 
> 
> 


One can easily produce a Kripke model of S where $B$ fails, hence the answer is indeed positive. One can solve all sorts of similar questions about unprovability like this, by expressing it in provability logic and then finding a suitable Kripke model. You can learn more about provability logic from references given in the Wikipedia article.


