# n-consistency - provability/truth of $\Sigma^0_n$ and $\Pi^0_{n+1}$ -formulas; n-consistent extensions, etc.

I am facing difficulties with the following exercise.
(It is 1.5.9. from 'proof theory and logical complexity', Girard, '87)

(i) T is $$\textbf{n-consistent} \ (n>0)$$ if any $$\Sigma^0_n$$ - theorem A of T, A closed, is true.
Show that if T is n-consistent, then all closed $$\Pi^0_{n+1}$$ -theorems of T are true.
Show that n-consistency of T is a $$\Pi^0_{n+1}$$ -formula, when T is prim. rec.

(ii) Assume that T is n-consistent; form a theory U by adding to T all true closed $$\Pi^0_{n}$$ -formulas. If T is prim. rec., show that $$Thm_U$$ is $$\Sigma^0_{n+1}$$. (Hint: define first a $$\Pi^0_n$$ -formula $$Val^0_n$$ such that if A is $$\Pi^0_n$$ and closed, $$Val^0_n[\overline{ \ulcorner A \urcorner}] \leftrightarrow A.$$ )

[Remark: I guess he means $$truth$$ of $$Val^0_n[\overline{ \ulcorner A \urcorner}] \leftrightarrow A.$$ , not provability in T or U.]

I am probably shortly going to add (iii) and (iv).

Idea for (i):

I think the first thing to show in (i) is pretty clear.
If one is given a $$\Pi^0_{n+1}$$ -theorem B, then B[t] is provable for any t. (t takes the place of the first variable). But B[t] is a closed $$\Sigma^0_n$$ -theorem, hence it is true - for any t. So B is true.

The second thing to show may work with induction on n, but it's a wild guess. I'm not even sure what he means by n-consistency "being" a such and such formula, what formula exactly does he have in mind?
Also I am not sure if/how the system is able to tell whether a formula is $$\Sigma^0_n$$ or not.

Thanks,

Ettore

PS: I left a link on mathoverflow also: https://mathoverflow.net/questions/319285/n-consistency-provability-truth-of-sigma0-n-and-pi0-n1-formulas-n

• There is a truth predicate $T_n$ for $\Sigma_n^0$ sentences, and of course you have a provability predicate and a "this sentence is $\Sigma_n^0$" predicate. The $n$-consistency statement "any $\Sigma_n^0$ sentence that is provable is true" can be expressed in terms of these three predicates. – spaceisdarkgreen Dec 14 '18 at 18:50
• I didn't see you said you weren't sure about the "this formula is $\Sigma_n^0$" predicate. A formula having less than or equal to $n$ nestings of $\exists-\forall$ blocks is a syntactical property that can be decided by parsing the formula... it is recursive. Being provably equivalent to such a sentence is just a statement about such an equivalence proof existing. – spaceisdarkgreen Dec 14 '18 at 19:44
• thanks @spaceisdarkgreen! I will think about it and try something out a bit...I thought it should be possible to tell whether $\Sigma^0_n$ or not, so I more or less believed it from the beginning, but do not clearly see before my eyes how this is realized/works, but that is not terribly important. Maybe I will also need the HBL-derivability conditions? I wouldn't have thought about the truth predicate, I only recall that the general truth predicate does not exist by tarski's theorem.. – Ettore Dec 15 '18 at 8:47
• In that case I guess our formula would be something like $\forall x (\Sigma^0_n (x) \land \exists y Pr(x,y) \rightarrow Tr_n(x))$. But why is it $\Pi^0_{n+1}$? – Ettore Dec 15 '18 at 11:15
• The truth predicate for $\Sigma_n$ sentences is itself $\Sigma_n.$ The other two are $\Sigma_1$. – spaceisdarkgreen Dec 15 '18 at 22:28