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