2
$\begingroup$

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

$\endgroup$
  • 2
    $\begingroup$ 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. $\endgroup$ – spaceisdarkgreen Dec 14 '18 at 18:50
  • 1
    $\begingroup$ 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. $\endgroup$ – spaceisdarkgreen Dec 14 '18 at 19:44
  • $\begingroup$ 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.. $\endgroup$ – Ettore Dec 15 '18 at 8:47
  • $\begingroup$ 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}$? $\endgroup$ – Ettore Dec 15 '18 at 11:15
  • 1
    $\begingroup$ The truth predicate for $\Sigma_n$ sentences is itself $\Sigma_n.$ The other two are $\Sigma_1$. $\endgroup$ – spaceisdarkgreen Dec 15 '18 at 22:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.