Realization of FOS4 in FOLP
Definition 10.11 (Realization) Let A be a first-order modal formula. By a realization of a formula A we mean a formula Ar of the language of FOLP that is obtained from A by replacing all occurrences of subformulas of the form 
for some proof terms t where
To avoid unnecessary
formalism, we suggest thinking of a realization as a result of an iterated procedure, which always replaces an innermost
A realization is normal
if all negative occurrences of ? are assigned proof variables.
Remark 10.12 If Ar is a realization of A, then for every subformula B of A, 
where P is a predicate letter, and logical rules:
derives
Similar to Theorem 6.5, this proof fits for all axiomatically appropriate and schematic constant specifications CS, cf. Section 6.3.
Corollary 10.17 FOS4 is the forgetful projection of FOLP.
Corollary 10.18 F is derivable in HPC if and only if its Godel translation is realizable in FOLP.
10.2.1 Implications for First-Order BHK Semantics
Godel’s translation of HPC into FOS4, followed by realization of FOS4 in FOLP, provide a formal analysis of first-order BHK semantics which respects Kreisel’s critique (Kreisel, 1962; cf. also Dean and Kurokawa, 2016). Along with fixing clauses for implication and negation, cf. Section 9.4, FOLP offers a fix to the case of universal quantifier. In the original BHK, this case was presented as
• a proof of VxA(x) is a function converting c into a proof of A(c).
The deficiency of this definition is vividly demonstrated by the following example which is due to Helmut Schwichtenberg (Schwichtenberg, n.d.).
10.3