Self-Referentiality of Justifications
LP admits self-referential types of the sort f.F(f) stating that t is a proof of a sentence F, which explicitly contains t. This self-referentiality is supported by the provability semantics that includes an arithmetical fixed-point argument.
But is self-referentiality actually needed for realization of S4? For BHK semantics?An inspection of the realization theorem, Theorem 6.5 shows that self-referential proof terms can appear as realizers of modalities by this particular realization algorithm. This, however, does not answer the question of whether self-referentiality can be avoided here.
The BHK clause for implication, though informal, also appears to be self- referential because a proof s of an implication A → B should be a construction that accepts any proof of A and returns a proof of B, and among the proofs of A could possibly be s itself.
These considerations: partial for S4 and informal for BHK, point at the possibility of a negative answer. It is time for us to be precise.
Definition 9.26 (Direct Self-Referentiality) A constant specification formula c:A is directly self-referential if A contains an occurrence of c.
Consider the so-called Moore sentence: It rains but I don’t know it. If p stands for it rains and ? denotes “knowledge” then a modal formalization of the Moore sentence is
M is easily satisfiable in S4, hence consistent, e.g., when p is true but not known. However, it is impossible to know Moore's sentence.
The question of the self-referentiality of BHK-semantics for IPC has been answered by Junhua Yu in Yu (2014). Extending Kuznets' method, he established
Yu’s Theorem: Each LP realization of the intuitionistic law of double negation 
requires directly self-referential constant specifications.
More generally, Yu has proved that any double negation of a classical tautology (by Glivenko's Theorem all of them are theorems of IPC) needs directly self-referential constant specifications for its realization in LP. Another example of unavoidable self-referentiality was found by Yu in the purely implica- tional fragment of IPC. This suggests that the BHK semantics of intuitionistic logic (even just of intuitionistic implication) is intrinsically self-referential.
These results by Kuznets and Yu indicate that provability BHK semantics for S4 and IPC is essentially self-referential and needs a fixed-point construction to connect it to formal proofs in PA or similar systems. This might explain, in part, why any attempt to build provability BHK semantics in a direct inductive manner without self-referentiality was doomed to fail.