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

  • $\begingroup$ Of course, the statements "set theory is consistent" and "it is consistent that set theory is consistent" and so on I think are examples, if axiomatized correctly. But you're probably interested in more hands-on statements. I am under the impression that some of the large-cardinal axioms fall into this boat (essentially by implying consistency of consistency, or something like that). But I am not an expert, so don't put much weight in this comment. $\endgroup$ Aug 1, 2011 at 20:20
  • $\begingroup$ I suggest more care in the wording. Just because a statement is not provable from an axiom system does not mean it is undecidable in a recursion theoretic sense. I recommend "undecidable from the given axiom system". You can then (with the right selection of theories) put your concept of generalized undecidability on a more formal (and thus workable) footing. Gerhard" "Ask Me About System Design" Paseman, 2011.08.01 $\endgroup$ Aug 1, 2011 at 20:46
  • 1
    $\begingroup$ (Throughout, I assume the axiom system is consistent.) My impression of the answer was different than what the other two comments seem to offer. If you limit yourself to working in a fixed axiomatic setting, then I thought there is no such thing as a proof there is no proof of undecidability or not. Why? Because such a proof would have to show there is no proof of the original statement, and thus would show the statement is undecidable. $\endgroup$ Aug 1, 2011 at 21:04
  • 1
    $\begingroup$ Related question: cstheory.stackexchange.com/questions/116/… $\endgroup$ Aug 1, 2011 at 21:25
  • 1
    $\begingroup$ I think the proper terminology would be independent. A statement is independent from a set of axioms if it cannot be proved or disproved from the axioms. $\endgroup$ Aug 1, 2011 at 21:28

2 Answers 2


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.

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.


In questions like these, I think it is important to say right off the bat: Theorems are only undecidable in a given axiom system. For all we know, all meaningful mathematical questions, including all questions about the halting/nonhalting of any computer program, are settled from a strong enough axiom of higher infinity. It's just that you need stronger axioms for stronger theorems, and you can't use a fixed computer program to list all the the axioms.

Anyway, given some consistent axiomatic system, like ZF, consider the Godel statement, which is constructed as follows:

Write computer program GODEL to do the following:

  1. print its own code into a variable R

  2. deduce all consequences of ZF, looking for the theorem "R does not halt"

  3. if it finds this theorem, halt.

A little reflection shows that GODEL halts if and only if ZF proves "GODEL does not halt". That is, if you call the sentence "GODEL does not halt" by the name G, then G is true if only if ZF does not prove G.

This sentence is unprovable in ZF, so it is order 0.

But it is also order 1: ZF can't prove that it is unprovable, because of the fact that it is a pi-1-0 statement, it is a statement about the non-halting of a computer programs. If program P halts, then ZF proves that this program halts (and ZF can also prove this fact about itself).

A little reflection shows that G is also of order 2, and order 3, of any order really, because the whole point of the Godel sentence is that ZF can't prove it, can't prove it can't prove it, can't prove that it can't prove that it can't prove it, etc. So the Godel sentence answers your question in a technical sense, but probably not the way you intended.

But colloquially, one says that "G is provably unproveable" when you show that G is equivalent to "consistency of ZF", so if you prove " (ZF is consistent) iff (G)", you have proved G is unprovable in common parlance, because the common intuition is that the consistency of an axiom system is to be taken for granted. But G is provable in a stronger system where the consistency of ZF is explicitly stated as a new axiom.

So in order to get a non-vacuous hierarchy, one could interpret your levels as follows:

level 0: "ZF proves that con(ZF) is equivalent to G." (So G is provably unprovable) level 1: "ZF proves that con(ZF+con(ZF)) is equivalent to G'. (G is unprovable, and it is provably not equivalent to con(ZF), so it is provably unprovably unprovable) level 2: "ZF proves that con(ZF+con(ZF+con(ZF))" (this is harder to state in English, but it's level 2)

etc, etc.

In this case, you can define the levels up to n, and higher levels by transfinite induction. This is studied in ordinal proof theory.

  • $\begingroup$ "all meaningful mathematical questions […] are settled from a strong enough axiom of higher infinity" — but they can be settled in different ways depending on which exactly axioms you choose. Do you suggest that we always have a way (although, not capable of being expressed as an algorithm) to eventually decide which particular axioms are correct and should be accepted to settle all meaningful mathematical questions correctly? $\endgroup$ Apr 7, 2021 at 0:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.