4
$\begingroup$

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$ ?

  • 0
    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?2011-08-01
  • 0
    @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.2011-08-01
  • 0
    Possible duplicate: [Is there a statement whose undecidability is undecidable?](http://math.stackexchange.com/questions/17212/is-there-a-statement-whose-undecidability-is-undecidable)2011-08-01
  • 0
    @Zhen: I disagree. It is not a duplicate. This question refers to *high-order* statements, and not statements which are first order and their undecidability is undecidable (so to speak, high-order decidability).2011-08-01
  • 0
    @Asaf: But the question that the OP *actually* asked is essentially a paraphrase of the title of the other question: ‘Are there any conjectures/statements of which we can prove that we cannot prove whether it is decidable or not?’ The OP didn't say anything about higher-order logic!2011-08-01
  • 0
    @Zhen: true, the first subquestion is a duplicate. The second one isn't though, so I will change the main question in such a way that it adresses the second subquestion as well.2011-08-01
  • 1
    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.2011-08-01
  • 0
    Under the new title, and in my opinion, this really has nothing to do with metamathematics.2011-08-01
  • 1
    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.2011-08-02
  • 1
    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".2012-11-10

0 Answers 0