Formalizing the BHK Interpretation in T
Recall that Kreisel's original goal in introducing the Theory of Constructions was to formulate a formal system which could play a role analogous to Tarski's definition of truth for Heyting Predicate Calculus (HPC). In order to see how this might be achieved, it is useful to note that at least at an informal level, the BHK clauses can be understood as serving a role analogous to the clauses in Tarski's definition of truth in a model—i.e. that of providing a characterization of “constructive validity” relative to which it might be hoped that a logical system such as HPC could be shown to be sound and complete in the same sense that the Classical Predicate Calculus CPC is sound and complete with respect to classical validity (i.e. truth in all Tarskian models).
But before investigating how Kreisel and Goodman proposed to interpret the BHK2 clauses in the language of T , it is useful to first remark upon one important sense in which these clauses differ from those of Tarski. For note that on the one hand what occurs on the righthand side of one of the Tarski clauses is a proposition stating
in the language of set theory what must be true in order for a formula A(−→x ) to be true in a model A relative to an assignment v of values to variables −→x . But what occurs on the righthand side of the BHK (and BHK2) clauses are not propositions but rather conditions stating the circumstances under which a certain object is to be regarded as a proof of A(−→x ) (relative to an assignment of vales to the free variables −→x ). Thus whereas the formalization of the Tarskian satisfaction relation A |=v A(−→x ) yields a sentence which can be formalized in the language of set theory, we should expect the formalization of the BHK clauses to yield a predicate—which Kreisel  symbolizes as Π( A(−→x ), s)—which is intended to hold of a proof s just in case it is a proof of a formula A(−→x ).
Kreisel and Goodman's formalizations of the BHK clauses thus can be understood as attempting to provide a definition of Π( A(−→x ), s) which were intended to serve
the role of providing a formalization of the proof relation as defined above. In order to understand the general form which their definitions took, note first that as with the analogous Tarski clauses, the BHK clauses (as well as their BHK2 counterparts) employ logical connectives on their righthand sides—e.g. the clause (P→) states that p is a proof of A → B just in case for all proofs x , if x is a proof of A, then p(x ) (i.e. the result of applying p to x ) is a proof of B. In addition to the problem of impredicativity discussed in Sect. 2, there is also another apparent obstacle in rendering the conditional if ... then appearing in this clause as a term in the “logic free” language of T .
Kreisel and Goodman proposed to circumvent this problem by taking advantage of the following observations: (1) it is intuitionistically admissible to apply classical propositional logic to decidable statements; (2) if the truth values T and ⊥ are taken
as abbreviating particular λ-terms, it is possible to define bivalent λ-terms ∩k , ∪k , and ⊃k which mimic the classical truth functional connectives ∧, ∨, and → applied to binary terms with k free variables ; (3) the application of these terms to terms of the form Π( A(−→x ), s) will always yield a term which is defined as long as it can be
ensured that Π( A(−→x ), s) is itself defined so that it is bivalent.
Taking these observations into account, we can now formulate Kreisel's  definition of Π( A, s) (where we assume that the free variables of A and B are
contained in −→x of arity k) in the language of T as follows :
(K∧) Π( A ∧ B, s) := λ−→x .(Π ( A, D1s) ∩k Π(B, D2s))
(K∨) Π( A ∨ B, s) := λ−→x .(Π ( A, D1s) ∪k Π(B, D2s))
(K→) Π( A → B, s) := λ−→x .π(λy.(Π ( A, y) ⊃k Π(B,(D2s)y)), D1s)
(K¬) Π (¬ A, s) := λ−→x .π(λy.(Π ( A, y) ⊃k Π (⊥,(D2s)y)), D1s)
(K∀) Π (∀z A(z), s) := λ−→x .π(λy.Π ( A[y/z],(D2s)y), D1s)
(K∃) Π (∃z A(z), s) := λ−→x .Π ( A[(D1s)/z], D2s)
Note that these clauses provide a straightforward expression of the clauses of the BHK2 interpretation—e.g. (P2→) is formalized by requiring that Π( A → B, s) holds just in case s is a pair such that D1s is a proof that D2s has the property of being such that if Π( A, y), then Π(B,(D2s)y)). But since (K→), (K¬), and (K∀) are all of the form π st , Kreisel's clauses can be understood as defining Π( A, s) in terms of π xy in such a way that the decidability of the primitive proof relation is transferred inductively to the complex proof relation.
-  For instance if we take T =df λxy.x and ⊥ =df λxy.y (cf. ), then we may define ⊃1 to be
-  Goodman [16, 17] provides a related interpretation of the BHK clauses in the language of the stratified theory T ω . However, relative to his interpretation, the variable y in (K→), (K¬), and (K∀) is asserted to range over proofs of a lower “level” than that of the proof D1s (see Sect. 5.2). Kreisel and Goodman also handle the case of atomic formulas differently. On the one hand, Kreisel introduced primitive terms into the language to serve as constructions which act as the characteristic functions of non-logical predicates, which are then individually asserted to be decidable. On the other hand, Goodman considers only the language of primitive recursive arithmetic, wherein all atomic statements are equations of the form f1(−→x ) = f2(−→x ). True equations of this form are asserted to fall under the decidable equality predicate Q which he introduces as another primitive to the language of T ω