Home Philosophy Advances in ProofTheoretic Semantics
Soundness, Completeness, and InternalizationThe 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, fHPC A if and only if there exists a term s such that fT ∗ Π( A, s) ≡ T. The lefttoright 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 righttoleft 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 lefttoright 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 fT + s ≡ T, then there exists a term c such that fT + π 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.)

< Prev  CONTENTS  Next > 

Related topics 