I've been working through a textbook, often encountering difficulties with the exercises. On mathstackexchange, with most of them I haven't arrived yet at a satisfactory solution.

As I understand, they might be not ideally phrased, but I don't know what should be changed, or I don't see a good possibility to rewrite them. If you miss some background information, I will try to provide it.

If it would cost too much time, maybe you like to leave hints for (better/more detailed) solutions or general, short descriptions how the solution 'looks like'.

In future I'll try to write in a way that can more easily be answered. Of course nobody should feel forced to answer, in the past it seemed people sometimes feel that way, to my surprise.

Here's a copy:

Would be great if someone could help me with the following exercise: (1.5.11. from 'proof theory and logical complexity', Girard, '87)

Let T be a theory in the language $L_0$; [Remark: That is the language of elementary arithmetic in this case, that is zero, successor, addition, product, prop. connectives and quantifiers, equality and less-than.]

assume that there is a formula $Prov[a,b]$ of $L_0$ such that

[Remark: ...for all natural numbers a, b, n...]

(i) $T \vdash A[\overline{n}] \rightarrow T \vdash Prov[\overline{\ulcorner A[x_0] \urcorner},\overline{n}]$

(ii) $T \vdash Prov[\overline{a},\overline{a}] \rightarrow Prov[\overline{\ulcorner Prov[x_0,x_0] \urcorner},\overline{a}]$

(iii) $T \vdash Prov[\overline{a},\overline{n}] \land Prov[\overline{\langle 19,a,b \rangle}, \overline{n}] \rightarrow Prov[\overline{b},\overline{n}]$.

Show that, if T is consistent, then $T \nvdash \neg Prov[\overline{\ulcorner \overline{0}=\overline{1} \urcorner},x]$.

[Remark: Above every number symbol there should be an overline, showing that we are speaking about numerals of the formal system rather than natural numbers, which is omitted for simplicity.

19 ist the Gödel number of the implication arrow.

The implication arrow in clause (i) isn't really an implication arrow, cause this is a usual (meta-)implication (if-then-statement).]

As I understand, Shepherdson and Bezboruah proved a version or 'variant' of Gödels second incompleteness theorem in some paper, it might have something to do with this, but I guess it would be to hard to work through the paper for me.

Thanks and kind regards,

Ettore