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,


  • $\begingroup$ You said that number symbols should have overlines, to indicate numerals. I'm reasonably sure that $n$ counts as a number symbol and that $x_0$ doesn't, but what about $a$ and $b$? $\endgroup$ – Andreas Blass Dec 23 '18 at 23:04
  • $\begingroup$ @AndreasBlass: Hi Andreas, thanks for the questions, yes that's right. I just added the overlines as in the textbook. I hope this clarifies the issue. When 'Prov[a,b]' is first mentioned, 'a' and 'b' are metavariables for terms, I think, so they do not need overlines. Similarly in clause (iii), '19', and right after it 'a' and 'b' indicate in fact natural numbers, not numerals, which are then computed to an number by the angles, of which we want to use the corresponding numeral in the formula, hence only the long overline over '19', 'a' and 'b' is needed. $\endgroup$ – Ettore Dec 24 '18 at 10:25

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.