# Property of “provability predicate”

In A Simple Proof of Gödel’s Incompleteness Theorems, the provability predicate $P$ is defined:

• Let $g$ denote the Gödel number function.
• Let $\operatorname{Proof}(x,y)$ be a binary predicate that translates "$x$ is the Gödel number of a proof of the formula whose Gödel number is $y$".
• Define $\operatorname{Pr}(y) = \exists x \operatorname{Proof}(x,y)$.
• Define $P(X) = Pr(g(X))$.

The properties of $P$ are stated but not proved:

• If $\vdash X$, then $\vdash P(X)$.
• $\vdash P(X \implies Y) \implies (P(X) \implies P(Y))$.
• $\vdash P(X) \implies P(P(X))$.

Each seems to be intuitively obvious, but how does one go about proving those properties?

• I think this is discussed in Boolos' Book "The Logic of provability" to some extent and less handwavy then usual. I'm also curious if anyone has other literature recommendations where these issues are discussed in some detail. – Achilles Sep 12 '17 at 19:46
• Boolos is also what Mendelson cites for the result (particularly the third condition). – Henning Makholm Sep 13 '17 at 2:31

These three properties are famous under the name Hilbert-Bernays provability conditions.

The middle one is the easiest. You need to have done a lot of fiddlywork proving things about how Gödel numbers for symbol sequences work in general, of course, but once you have an appropriate box of tools, it's pretty simple: Your proof system contains an explicit rule (number 5 in the paper you link to) that says a proof of $Y$ can consist of a proof of $X$ together with a proof of $X\Rightarrow Y$. All you need to to is prove that the proof you construct has a Gödel number -- and that the precise definition of $Pr$ (which the author helpfully leaves it to you to work out in detail) works as advertised.

The first one is already pretty tedious -- though not particularly difficult, once you get in the rhythm. You work by induction on the structure of the proof of $X$ -- or in other words, by long induction on the length of the proof of $X$. The rules 4, 5, 6 in your system say that a proof of something can be constructed as a combination of (necessarily shorter) proofs of various other things. When the proof of $X$ concludes with one of these rules, apply the induction hypothesis to those shorter proofs, giving you $P(\cdots)$ for those, and then combine them in the same way as the middle one.

If your proof of $X$ is by one of the rules 1, 2, 3, there are no shorter proof to appeal to -- so what you do there is just verify that your $Pr$ considers each instance of these axioms to be a proof of itself.

Once you cross the t's and dot the i's you have a proof of the first property.

The third property is where it really gets hairy.

To begin with it doesn't actually hold in the system of the paper you link to -- because the proof system that was presented cannot even represent $P$. By definition, $P(X)$ means $\exists x\, \mathit{Proof}(x, g(X))$, but the system of the paper only covers propositional logic. It contains neither a Gödel number for the $\exists$ symbol, nor proof rules to allow you to prove things with $\exists$ in them, nor a way to consider $\exists$ an abbreviation. And without that, the notation $P(P(X))$ doesn't even make sense!

Also, there don't seem to be any axioms that tell you how arithmetic works, so proving anything about numbers is going to be tough.

But all of that is fixable. Let's suppose we have fixed it. Then, of course, we need to define a new better $P$ for our extended system, and prove the two the Hilbert-Bernays properties once again for the extended system. Much work, not particularly enlightening, but it can be done.

Then you hope that you have not only extended your proof system enough to express $P$ in it, but also to formalize the proofs of ordinary mathematics. Because the strategy is now to prove that everything you did to prove the first property can be formalized in the system you are considering. If you manage to convince yourself of that, the third property is nothing more than the system proving the first property about itself.