# Examples of provably${}^n$ unprovable statements

Given any statement $A$ and a classical theory $T$ which we assume is at least as strong as Peano Arithmetic ($\sf PA$), we have that $T\vdash A$ implies $T\vdash T\vdash A$ (that is, if a statement is provable, then it is provably provable). Let $T_1=T$ and $T_{n+1}=T_n+{\sf Con}(T_n)$. (We need stronger theories if we want to prove unprovability.) Given this, simply by considering the truth values of the relevant statements, we get the following classification of statements by unprovability:

1. $T\vdash A$ ($A$ is provable)
2. $T_2\vdash T\not\vdash A$ ($A$ is provably unprovable)
3. $T_3\vdash T_2\not\vdash T\not\vdash A$ ($A$ is provably unprovably unprovable)

...

$\omega$. For all $n$, $T_n\not\vdash\dots \not\vdash T_2\not\vdash T\not\vdash A$ (we can't say anything about $A$'s provability)

We can refine this hierarchy by also considering the status of $\lnot A$. Let's call a class $m,n$ statement one such that $A$ is at level $m$ above and $\lnot A$ is level $n$ in the list. Since $T\vdash\lnot A$ implies $T_2\vdash T\not\vdash A$, the only nonempty classes at level $1$ are the class $1,2$ statements (provable statements) and the class $2,1$ statements (refutable statements). Independent statements are in class $2,2$. The class $1,1$ is nonempty iff the theory is inconsistent.

My question is: Are there any (preferably "natural") statements that fall further into this hierarchy? I know many examples of independent statements, like the continuum hypothesis or the axiom of choice relative to $\sf ZF$, or the Paris–Harrington theorem relative to $\sf PA$. But I know no examples of even any class $2,3$ statements. I expect there may also be natural examples of $\omega,\omega$ statements. My guess is that all the classes $m,n$ with $m,n\ne1$ are nonempty, but examples elude me.

• Possibly relevant: Absolutely undecidable statements in Peano Arithmetic – hmakholm left over Monica May 13 '16 at 18:55
• @HenningMakholm I'm hoping to avoid the pedantic answer shown in that and similar results - that the hierarchy collapses because $T\vdash T\not\vdash A$ is always false, unless $T$ is inconsistent - by using a hierarchy of just-barely strong enough theories $T_n$ to make sense of an unprovability claim. – Mario Carneiro May 13 '16 at 19:06
• x @Mario: Yes, I noticed that -- thus "possibly relevant" rather than "duplicate"". – hmakholm left over Monica May 13 '16 at 19:17

[This is a partial answer, but I decided to post it anyway since no one else has answered for a long time now. Very interesting question by the way!]

Note that if $T = PA + \neg Con(PA)$, then $T \vdash \neg Con(T)$ and hence $T_2$ is inconsistent and proves everything, so your hierarchy collapses. So it's not enough just to assume that $T$ contains $PA$. I think you need the much stronger condition of assuming that $T$ is arithmetically sound, namely that every arithmetical statement that $T$ proves is true for $\mathbb{N}$. This would happen if for example $T$ has an $ω$-model, namely that there is a model of $T$ where the arithmetical part is $\def\nn{\mathbb{N}}$$\nn$. If the language of $T$ is the language of arithmetic (with no extra symbols), then these two notions are equivalent and just mean that $\nn$ satisfies $T$, but in general arithmetic soundness is weaker.

So we shall from now assume that $T$ has decidable proof validity and is arithmetically sound. Note that by induction $T_n$ is arithmetically sound for every $n \in \nn$.

Let $D(n)$ denote the class of sentences at level $n$ in your hierarchy, and let $D(m,n)$ denote your class $m,n$. And let $D^*(k,l) = \bigcup \{ D(m,n) : k \le m \le ω \land l \le n \le ω \}$.

Firstly, your statement that independent sentences are in $D(2,2)$ is not correct, because all you know is that it is in $D^*(2,2)$, since the very definition of independence is equivalent to being in $D^*(2,2)$. Note that our entire discussion is in some meta-system, usually taken to be ZFC. The question of whether or not a sentence over $T$ is independent over $T$ has a fixed truth-value in the meta-system. Even if we cannot prove some sentence independent, it does not change which class it falls in.

Some sentence over $T$ is in $D^*(2,3)$.

Claim: $Con(T_2) \notin D(1)$. Proof: If $T_1 \vdash Con(T_2)$ then $T_1 \vdash Con(T_1)$, which gives a contradiction.

Claim: $( \neg Con(T_2) ) \notin D(1)$. Proof: If $T_1 \vdash \neg Con(T_2)$, then $T_1 \vdash ( T_1+Con(T_1) \vdash \bot )$, and hence $T_1 \vdash ( T_1 \vdash \neg Con(T_1) )$, but by arithmetical soundness this implies $T_1 \vdash \neg Con(T_1)$, which gives a contradiction.

Claim: $( \neg Con(T_2) ) \notin D(2)$. Proof: If $T_2 \vdash ( T_1 \nvdash \neg Con(T_2) )$, then $T_2 \vdash Con( T_1 + Con(T_2) )$, and hence $T_2 \vdash Con(T_2)$, which gives a contradiction.

Claim: $Con(T_2) \in D(2)$. Proof: $T_2 \vdash ( T_1 \nvdash Con(T_1) )$, and hence $T_2 \vdash ( T_1 \nvdash Con(T_2) )$.

Conjecture: $( \neg Con(T_2) ) \in D(3)$.

Therefore $Con(T_2) \in D^*(2,3)$, and I think it is in $D(2,3)$.

I also think that there is some sentence $φ$ over $T$ that is in $D^*(ω,ω)$, but don't see why.

• In the part where you say my claim about independent vs. $D(2,2)$ is wrong, do you have a typo there? I think you wanted to write $D^*(2,2)$. Really, though, I think this depends on your interpretation of "independent" - generally a statement is not said to be independent until this fact is proven, in which case it falls in $D(2,2)$. Before this happens we would generally say "it is not known to be independent" which is the case for most open problems like RH. ... – Mario Carneiro May 28 '16 at 22:01
• ... If you consider also statements which "are" independent (that is, the statement of independence is true in the metatheory) even if this is not provable, then you get $D^*(2,2)$ instead. – Mario Carneiro May 28 '16 at 22:01
• @MarioCarneiro: Yes there is a typo, and I intended to convey what you have in your last comment. I've expanded that point accordingly. Basically the point is that, to even talk about independence over any formal system, we need to be outside it, working in some meta-system. And in the meta-system either it is independent or it isn't, regardless of whether we can prove it. This is classical logic. The concept of "known" does not exist even in the meta-system but in natural language, so one could say that technically it is an ill-formed notion. =) – user21820 May 29 '16 at 2:24