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
    Commented 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
    Commented Jul 22, 2012 at 15:06

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .