The foregoing clauses can thus be understood as providing a means of interpreting the language of HPC into the language of T so as to provide an analysis of Π( A, s) as characterized informally by the BHK2 clauses. The next question we must consider is how this interpretation comports with the intuitionists' desire to identify truth and constructive provability. But needless to say, this question is complicated at least to the extent that it is traditionally maintained that “constructive provability” must be distinguished from “provable in a given formal system”.

One might think that this entails that the related notion of “constructive validity” which we might hope to characterize using a system in which the BHK clauses can be interpreted must be distinguished from “valid with respect to a particular form of formal semantics”^{[1]}. Nonetheless, Kreisel and Goodman both appear to have viewed the Theory of Constructions as providing an “informally rigorous” analysis of constructive validity. In particular, both present versions of the following result for the systems described in [25, 26], and [17] (wherein T ∗ is the relevant formulation of the Theory of Constructions):

(Val) For all formulas A in the language of HPC, f-HPC A if and only if there exists a term s such that f-T ∗ Π( A, s) ≡ T.

The left-to-right direction of Val can be taken to express a form of soundness for Kreisel's interpretation of HPC into T ∗—i.e. if A is derivable from what are normally regarded as intuitionistically valid principles of reasoning, then A is indeed “constructively valid” in the sense that there is some construction which witnesses its derivability. Conversely, the right-to-left direction of Val can be taken to express a form of completeness (also known as faithfulness) of the interpretation—i.e. if A is “constructively valid” in the sense that Π( A, s) holds for some construction s, then A is in fact derivable from intuitionistically valid principles^{[2]}.

Although both Kreisel and Goodman announced versions of these results, the situation surrounding their claims is complicated by several factors which we will not consider in detail here

^{[3]}. For what is more germane to our immediate concerns is not whether any particular variant of the Theory of Constructions satisfies Val, but rather whether such systems satisfy what can be understood as a generalized form of soundness which we will refer to as internalization. Note that if we are able to demonstrate the left-to-right direction of Val (say by induction on the length of proofs in HPC), then it also seems reasonable to suppose that we ought to be able to do this for all derivations carried out in T itself ^{[4]}. This would suggest that the Theory of Constructions ought to satisfy a principle of the following form:

(Int) If f-T + s ≡ T, then there exists a term c such that f-T + π sc ≡ T.

Here c might either be taken as a new constant or as a complex term which is built up according to the structure of the derivation of s ≡ T. (Although we will return to discuss this issue in Sect. 5.5, for the moment we will assume the former interpretation so as to maintain conformity with the way in which Kreisel and Goodman handle internalization.)

[1] For discussion of the intuitive notion of constructive validity and its relationship to various formal semantics for intuitionistic logic, see (e.g.) Scott [37], Dummett [7, chap. 5], and McCarty [32]

[2] Compare Scott [37, p. 256]: “The reason that A is intuitionistically (constructively, if you prefer) valid is that there is a specific term τ […] such that the assertion fτ ∈ A is provable in the theory of constructions.”

[3] For instance, although Kreisel states versions of the completeness and faithfulness results ([25,

p. 205] and [26, Sect. 2.311]), in neither case are proofs given. And although Goodman [16] contains complete proofs of both directions, the interpreting theory in his case is not T , but rather the stratified theory T ω .

[4] In fact, this is exactly how the soundness proof for HPC given by Goodman [16, Sect. 11–15] for T ω proceeds

Found a mistake? Please highlight the word and press Shift + Enter