BHK Semantics
We recall that the intended meaning of intuitionistic logic is given by the informal Brouwer-Heyting-Kolmogorov (BHK) semantics of constructive proofs, cf. Section 1.2:
Informally there are objects of two sorts in BHK: proofs and (computable) functions.
Note that, conceptually, proofs/provability in a broad mathematical context can express computability, but the converse is not immediate. For example, in true arithmetic TA, which is the set of all arithmetical formulas true in the standard model of arithmetic, all computable functions are represented by corresponding terms. However, there is no conventional notion of a proof/provability represented in TA. So, it is a priori unlikely that computational programs alone could represent BHK adequately, whereas proofs alone might do.If we want to capture some notion of a BHK proof then a natural question might be “proofs where”? Derivations in an intuitionistic system itself make such semantics immediately circular, which undermines foundational ambitions. Derivations in the usual classical system, if applied naively, do not satisfy BHK conditions for V.
Historically, we observe two distinct classes of BHK-style semantics:
• Computational BHK, originating from Kleene's discovery (1945) of a computational content of intuitionistic logic. Kleene, according to his students' recollections, thought about formalizing proof-based BHK but found it to be too hard. However, Kleene found a computational version of BHK, which was an outstanding discovery: a computational content of constructive reasoning. A good example of a computational BHK semantics is given by Martin-Lof type theory. Though it uses a BHK proof terminology, Martin- Lof “proofs” or “constructions” are not identified with formal proofs, but rather have a natural computational interpretation.
• Provability BHK, originating from Godel's works on modal logic of provability S4 (Godel, 1933), on systems with explicit proofs (Godel, 1938), and completed within the framework of the Logic of Proofs LP in the mid 1990s. Since the modal logic S4 embeds to the logic of proofs (Realization theorem) and LP enjoys the arithmetical proof interpretation, S4 receives an exact arithmetical provability semantics consistent with BHK and Godel's sketches.
In addition Kreisel (1962) tried to develop a provability BHK from scratch but the system turned out to be inconsistent, cf. Dean and Kurokawa (2016) for a complete survey of this thread.
Kleene realizability, Kleene (1945), as a formalization of “constructively true” is reminiscent of BHK semantics; here the role of BHK proofs is played by computational programs (indices of recursive functions). In particular, a realizer of an implication A → B is a program p, which when applied to any realizer x of A returns a realizer of B. Symbolically:
All BHK clauses are satisfied by the computational semantics except for disjunction. In computational semantics for disjunction there is a requirement of a bit selector that points at the proper disjunct: 
This adjustment illustrates a difference between proofs and computational programs in the BHK setting: the proof predicate
p is a proof of F (9.1)
is decidable, whereas the realizability assertion
p realizes F (9.2)
is not decidable. The “selector” is needed for (9.2) but is redundant for (9.1) because given proof p, one can compute the right disjunct.
Let us discuss how the provability BHK works in the context of the logic of proofs, LP. For each modal formula F, let Fr denote a realization of F in the logic of proofs by some r (Theorem 6.5).
According to Corollary 6.6, S4 ' F if and only if LP ' Fr for some normal realization r.Corollary 9.23 (Arithmetical completeness of S4) S4 ' F, Fr is
(provably) valid for some normal realization r.
Recall that by Godel’s translation tr(F) of an intuitionistic formula F we understand the result of prefixing every subformula of F with the modality ?. According to Gddel-McKinsey-Tarski, cf. Section 1.2,
which defines IPC inside S4.
Definition 9.24 A propositional intuitionistic formula F is proof realizable if (tr(F))r is arithmetically valid under some normal realization r.
Theorem 9.25 (Provability completeness of IPC) For any propositional in- tuitionistic formula
Proof A straightforward combination of the aforementined Godel-McKinsey- Tarski equivalence and Corollary 9.23. ?
Theorem 9.25 provides an exact specification of IPC by means of a classical notion of proof that is consistent with BHK semantics. In addition to Godel’s translation tr(∙) one could consider the McKinsey-Tarski translation that prefixes only atoms and implications in F. A result similar to Theorem 9.25 holds for proof realizability based on such a McKinsey-Tarski translation too.
IPC is sound and compete with respect to the class of proof systems in arithmetic in the following precise sense:
1. Any derivation of F in IPC produces a realization consisting of a proof term assignment supported by a constant specification CS. This realization
9.5