# What are some good expositions of the Hilbert-Bernays-Löb derivability conditions for PA?

The Hilbert-Bernays-Löb derivability conditions state that for $$P$$ to be a provability predicate it must obey the following for all sentences $$A, B$$:

1. If $$A$$ is provable, so is $$P(\ulcorner A\urcorner)$$.
2. $$P(\ulcorner A\urcorner) \rightarrow P\bigl(\ulcorner P(\ulcorner A\urcorner)\urcorner\bigr)$$ is provable.
3. $$P(\ulcorner A \rightarrow B \urcorner) \rightarrow \bigl(P(\ulcorner A \urcorner) \rightarrow P(\ulcorner B \urcorner)\bigr)$$ is provable.

From these three conditions the second incompleteness theorem as well as Löb's theorem follow. However, the fact that PA has such a proof predicate is almost universally omitted, usually with a reference to Hilbert and Bernays' 1939 Volume II of Grundlagen der Mathematik. Surely there's been some improvements since then. Is a more modern treatment available somewhere?

• Chapter 2 of The Logic of Provability by Boolos. Mar 6, 2020 at 4:50
• This is material which is treated in the proof of Godel's incompleteness theorems - texts on Lob's theorem and the HBL conditions are assuming that as background. That said, I really like the exposition (of this and most things) in Boolos/Burgess/Jeffrey's book Computability and logic. Mar 6, 2020 at 16:10

Peter Smith, whom one may come across time to time contributing to Maths Stack Exchange, gives a lucid exposition in his book An Introduction to Gödel’s Theorems (delicately typeset by himself and freely downloadable).

He allocates Chapter 35 to the examination of the Hilbert-Bernays-Löb (HBL) derivability conditions for Peano Arithmetic (PA) and dwells also on generalising them to some other arithmetics.

• To be clear, he gives a proof sketch for condition 3 and a “sketch of a sketch” for condition 2, though he thankfully does supply references to detailed proofs that aren’t from 1939. Apr 10 at 23:05

You can find some details about the Hilbert-Bernays-Löb derivability conditions in the followings:

1. Boolos G. The Logic of Provability. Cambridge University Press; 1994. Chap. 2. as already mentioned by @spaceisdarkgreen.

2. Rautenberg W., A Concise Introduction to Mathematical Logic. Springer; 2010, and Grandy R., Advanced Logic for Applications. Springer; 1977 are both mentioned in Smith's book An Introduction to Gödel’s Theorems and contain proofs of both the second and third derivability conditions.

3. Halbeisen L., Krapf R., Gödel's Theorems and Zermelo's Axioms. Birkhäuser Cham; 2020. Chap. 11. provides a detailed proof of the provable $$\Sigma_1$$-completeness used to prove your second derivability condition. They follow, in a slightly different context, some proofs by S. Swierczkowski in "Finite sets and Gödel's incompleteness theorems", Dissertationes Mathematicae 422 (2003), 1-58. that might also be worth taking a look.

4. Galvan S., Teoria formale dei numeri naturali. F. Angeli; 1983. I have been told that this 768 pages book contains extremely detailed proofs of all three derivability conditions (in Italian, and quite difficult to get a copy).