# Is there such a thing as “second-order-undecidability”? And what about higher order Undecidability statements?

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, or belong to $U_1$.

I was wondering if there is some kind of generalization of this concept. Are there any conjectures/statements of which we can prove that we cannot prove whether it is decidable or not? Such a statement would be undecidable to the second order, or belong to $U_2$. Generalizing even further:

What about statements that are in $U_\infty$ ?

-
I have added [higher-order-logic], I am not too sure about [meta-math] tag. @Max, why do you think this has anything to do with metamathematics? – Asaf Karagila Aug 1 '11 at 15:08
@Asaf: err I guess I thought this because I don't really know what metamathematics is, yet. I just suspected it. Feel free to edit the tags. – Max Muller Aug 1 '11 at 15:09
By contradiction, $U_{n+1}\subseteq U_n$. Presumably at each $U_n$ one must step back to an even higher-order formal system. Ugh. @Zhen: OP's question is only a (half-)duplicate at $n=2$, and it is not specific to ZFC. – anon Aug 1 '11 at 15:28
The usual distinction that's relevant to this question is between object language and metalanguage. The statements Max refers to as neither provable nor disprovable, and the axioms from which they're independent, are stated in one language, the object language. The proof they're undecidable is carried out in the metalanguage, in which we talk about the object language, its axioms and theorems. Max seems to be asking about introducing another metalanguage, in which we talk about the first. This would require formalizing the first metalanguage. I don't know if that's been tried. – MikeC Aug 2 '11 at 5:01
I don't think this question is about higher-order logic in the usual sense. The OP unfortunately uses the word "order" in the context "undecidable to second order" to mean something quite different from its meaning in "second-order logic". – Andreas Blass Nov 10 '12 at 15:02