Arithmetical Completeness of the Logic of Proofs
According to Corollary 9.6, the logic of proofs is sound with respect to the intended arithmetical interpretation. In particular, if an interpretation * makes a constant specification CS true, then all theorems of LP(CS) are also true (provable in PA) under interpretation *.
This section is devoted to establishing the arithmetical completeness of the logic of proofs with finite constant specifications. A fundamental corollary of the completeness theorem states that any finite constant specification can be made true/provable in PA under an appropriate arithmetical interpretation. This applies also to constant specifications containing formulas of the type c.A(c). Such self-referential specifications cannot be true under arithmetical interpretations based on the standard provability predicate “from the textbook” because the Godel number of a proof c* should be greater that the Gddel number of a formula A* containing this very c*, which is inconsistent with the monotonicity of Godel numbering. So, a provability interpretation of c.A(c) requires special proof predicates obtained by an arithmetical fixed-point construction. 
The remaining parts of * are constructed by an arithmetical fixed point equation that follows. 
Indeed, if X is atomic, then X* is provably A1 by the definition of *. If X is t:Y, then (f.Y)* is Prf(t*, Y*), which is provably A1 as well.
Because the set of
There is another fundamental corollary of arithmetical completeness: it provides a comprehensive class of arithmetical interpretations necessary for indepthjustification of derivations from given constant specifications. The arithmetical completeness for LP(CS) guarantees that F * is true under each interpretation *, which makes all formulas from the constant specification CS true. But what if (CS)* is false under all arithmetical interpretations *? The first suspect could be
which is a legitimate constant specification. The same monotonicity argument as earlier shows that this constant specification cannot be made true by any proof predicate based on the standard Godel numbering.
However, Theorem 9.12 provides a desired arithmetical interpretation, which makes this specification true. Moreover, by this theorem, any constant specification CS is true under some normal arithmetical interpretation.
Theorem 9.22 (Nonemptiness of provability semantics for LP) For any finite constant specification CS there exists an arithmetical interpretation * such that (CS)* is true (provable in PA). 
174 Arithmetical Completeness and BHK Semantics
The significance of self-referential constant specifications will be also demonstrated in Section 9.5 where it is shown that neither S4 nor IPC can be realized without using self-referential constant specifications, which contain formulas of type c:A(c). None of such formulas can be realized by proof predicates based on monotonic Godel numbering.
9.4