In this section, we assume that, on top of propositional calculus, there is given a provability predicate satisfying the three axioms ax-prv1 and ax-prv2 and ax-prv3. Note the similarity with ax-gen, ax-4 and hba1 respectively. These three properties of are often called the Hilbert–Bernays–Löb derivability conditions, or the Hilbert–Bernays provability conditions.
This corresponds to the modal logic (K4) (see previous section for modal logic). The interpretation of provability logic is the following: we are given a background first-order theory T, the wff means " is provable in T", and the turnstile indicates provability in T.
Beware that "provability logic" often means (K) augmented with the Gödel–Löb axiom GL, which we do not assume here (at least for the moment). See for instance https://plato.stanford.edu/entries/logic-provability/.
Provability logic is worth studying because whenever T is a first-order theory containing Robinson arithmetic (a fragment of Peano arithmetic), one can prove (using Gödel numbering, and in the much weaker primitive recursive arithmetic) that there exists in T a provability predicate satisfying the above three axioms. (We do not construct this predicate in this section; this is still a project.)
The main theorems of this section are the "easy parts" of the proofs of Gödel's second incompleteness theorem (bj-babygodel) and Löb's theorem (bj-babylob). See the comments of these theorems for details.