Good day!

Let $\mathrm{T}$ be a first-order theory which contains the Peano arithmetic and has a recursively enumerable set of axioms. It is well known that one can construct a predicate $\mathrm{Pr}$, which indicates whether a formula is provable in $\mathrm{T}$. For the proof of the incompleteness theorem $\mathrm{Pr}$ is often constructed such that for all sentences $A, B$ the following conditions hold:

  1. $\mathrm{T} \vdash A$ implies $\mathrm{T} \vdash \mathrm{Pr}\left({\ulcorner{A}\urcorner}\right)$,
  2. $\mathrm{T} \vdash \mathrm{Pr}\left({\ulcorner{A}\urcorner}\right) \rightarrow \mathrm{Pr}\left({\ulcorner{\mathrm{Pr}\left({\ulcorner{A}\urcorner}\right)}\urcorner}\right)$,
  3. $\mathrm{T} \vdash \mathrm{Pr}\left({\ulcorner{A}\urcorner}\right) \land \mathrm{Pr}\left({\ulcorner{A \rightarrow B}\urcorner}\right) \rightarrow \mathrm{Pr}\left({\ulcorner{B}\urcorner}\right)$.

For instance this is shown in "The incompleteness theorems" by C. Smorynski.

Do these conditions also hold for open formulas $A, B$? Actually I think so, but then I don't understand why Smorynski exlicitly says "all sentences" in The incompleteness theorems. Am I wrong? Is there some easy counterexample if so?

EDIT: I've read now Smorynski's proof again (3.2.3-3.2.5 in http://www.compstat2004.cuni.cz/~krajicek/smorynski.pdf), and he actually uses (1) and (3) on the open formula $A(x) \rightarrow \exists x A(x)$ to conclude the validity of (2)... Also I think that the whole proof should work out for open formulas, because (2) and (3) only concern Gödel numbers of $A$ and $B$, and I think that symbols for free variables can be encoded as good as symbols for numbers. Additionally, the proof of (1) is quite easy and I don't see why it shouldn't work with free variables. So I guess, Smorynski states the properties (1)-(3) only for sentences, because he doesnt need them for open formulas in the proof of the incompleteness theorem. Or have I overlooked something?

EDIT2: In Tourlakis Lectures in Logic and Set theory. Volume 1 I just now found a detailed proof of (1)-(3) for all formulas. So the question is answered for me.

  • $\begingroup$ The only subtlety I can think of is in (3), since $A \to B$ is not the same as $(\forall \vec{x} . \, A) \to (\forall \vec{x} . \, B)$. $\endgroup$
    – Zhen Lin
    Jul 22, 2012 at 9:12

1 Answer 1


I think the point is that it is enough to show that the conditions (known as the Hilbert-Bernays derivability conditions) hold for all sentences.

Requiring that they work for all wffs would be a stronger condition and so make the eventual conclusions that assume the conditions weaker.

By the way, it is not sufficient that $T$ contains the axioms of Peano Arithmetic. In order to construct the Pr predicate, one needs the set of axioms of $T$ to be recursively enumerable. (Or at least arithmetical, but I think property 2 will be hard to establish for an arithmetical but non-r.e. set of axioms).

Also, you probably shouldn't call them "the Peano axioms", because that can refer to Peano's original set of second-order axioms, whereas I suppose you're working in first-order logic here.

  • $\begingroup$ I think, you are right with the last two remarks, so I've edited the original post respectively. $\endgroup$
    – yexela
    Jul 22, 2012 at 15:06

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.