# properties of the provability predicate applied to open formulas

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.

-
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)$. –  Zhen Lin Jul 22 '12 at 9:12

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).