Home Philosophy Advances in Proof-Theoretic Semantics
The feature of the Theory of Constructions which we have yet to examine is the principle of internalization we have labeled Int. This principle has evident affinities with both the first Hilbert-Bernays condition for the arithmetical proof predicate
ProofT(x , y) (i.e. if T fφ, then T f ∃x ProofT(x , 'φ')) and with the Necessi-
tation rule of normal modal logics (i.e. if fφ, then fD A). But such proof theoretic
analogies aside, Kreisel and Goodman's motivations for including such a principle
in the Theory of Constructions are at least somewhat obscure.
For instance, when rendered in the notation of the theory T , Kreisel's original presentation of Int is as follows:
For any sequence p of sequents, cp is a term (if p is a formal derivation in our system of s ≡ T then cp presents an—intuitive—proof of s ≡ t ) [... ¶.. .] If p is a formal derivation of s ≡ T, then π scp ≡ T is an axiom [25, pp. 203–204].
Kreisel says nothing about how cp is defined relative to the derivation p, nor does he further elaborate on the distinction between “intuitive” proofs and formal derivations. Moreover, he does not provide any examples to justify the inclusion of an internalization principle in his system. And while Goodman provides a somewhat more straightforward presentation of internalization as a formal rule of proof, his intuitive explanation of this principle is similarly opaque .
Rather than attempting to provide a direct reconstruction of Kreisel or Goodman's treatment of internalization in the Theory of Constructions, what we will now do is to present a partial reconstruction of the reasoning underlying the Kreisel-Goodman paradox using yet another system—Fitting's  Quantified Logic of Proofs [QLP]— for which a precise account of internalization is known to be available. QLP is an extension with first-order quantifiers over proofs of Artemov's  Logic of Proofs [LP], which itself may be understood as an “explicit” variant of the traditional modal
logic S4 wherein instances of the operator D are labeled with expressions similar in
form to the terms of the Theory of Constructions.36 We will present only the features
of the system which are necessary to reconstruct the relevant portion of the derivation of the paradox here and refer the reader to [1, 9] for additional details.
Like T , the language of QLP contains expressions known as proof terms s, t, u,... which are intended to denote constructive proofs. These are given by the grammar
t := x , y, z,... | ai (−→x ) | (!t )| (t • t )| (t + t ) | ((t (x )∀x ))
x , y, z,... are known as proof variables, and a1(x ), a2(x ), ... as axiom terms, !, •,
+ and (t (x )∀x ) denote proof operations respectively called proof checker (unary),
application (binary), sum (binary), and uniform verifier (binary). Also like T , the language of QLP contains a primitive expression intended to denote the proof relation R( A, t )—in particular t is a proof of A is expressed as t : A. However, unlike T (but like the semi-formal system of Sect. 3.2) the language of QLP contains the standard first-order connectives and quantifiers.
The axioms of QLP correspond to those of a standard Hilbert system for first-order logic (where for simplicity we regard all classical tautologies as axioms) together with the following axioms about the proof relation:
(LP1) t : ( A → B) → (s : A → t • s : B)
(LP2) t : A → A
(LP3) t : A →!t : t : A
Among the rules of QLP are modus ponens and the standard formulation of the first-order universal generalization rule UG (i.e. if Δ f-QLP A(x ), then Δ f-QLP (∀x ) A(x ) if x ∈/ FV(Δ)). As it is a form of modal logic, QLP also possesses a form of the traditional Necessitation rule:
(AxNec) If B is an axiom of QLP, then f-QLP aB : B for some unstructured proof term aB with the same free variables as B.
Note that the rule AxNec is not only similar in form to the principle Int, but can be given a justification similar to that which Kreisel gestures at above—i.e. if B is an axiom of the system, then we ought to be able to introduce a constant symbol aB which is stipulated to bear the proof relation to B to record the thought that we regard this formula as an axiom of the system.
One of the characteristic features of both LP and QLP is that while such an internalization principle is asserted to hold for their axioms, it is possible to establish a parallel result for their theorems as a metatheorem about the system as opposed to a basic principle. In particular, we have the following:
(Lift) If s1 : A1,..., sn : An f-QLP B, then for some proof term t , s1 : A1,..., sn :
An f-QLP t (s1,..., sn ) : B.
This result (which is traditionally called the Lifting Lemma—cf. [1, 9]) can be established by a straightforward induction on derivations. For instance, in the case of LP (which can be regarded as the quantifier-free fragment of QLP), the case where B is an axiom is handled by AxNec, and the case where B is derived from A → B and A by modus ponens is handled by LP1 as follows: if we assume (as
induction hypotheses) that u(−→x ) : A → B is derivable from −→s (−→x ) : Δ =df
s1(−→x ) : A1(−→x ), . . . , sn (−→x ) : An (−→x ) and v(−→x ) : A is also derivable from
the same premises, then it follows by LP1 that u • v(−→x ) : B is also derivable from −→s (−→x ) : Δ. However, in order to extend this result to QLP, we also need
to handle the case where s1 : A1,..., sn : An f-QLP (∀x )B(x ) is derived from s1 : A1,..., sn : An f-QLP B(x ) by UG (and the appropriate free variable condition is met). This requires the adoption of an additional rule—called explicit universal generalization –governing the introduction of the universal verifier symbol (•∀•):
(Eug) If s1 : A1,..., sn : An ft (x ) : B(x ), then s1 : A1,..., sn : An f(t ∀x ) :
(∀x )B(x ), where x ∈/ FV(si : Ai ) for 1 ≤ i ≤ n.
With this machinery in place, we can now begin to record several additional observations about the role of the principle Int in the derivation of the Kreisel-Goodman paradox. Note first that whereas the terms c which are introduced by applications of Int are treated as constants in the language of T +, we have just seen that the terms t (s1,..., sn ) which are introduced by Lift will typically be complex functional expressions whose compositional structure represents the derivation of formula B from the premises s1 : A1,..., sn : An . In particular, although the derivation (i)–(xii) given in Sect. 3.2 of the Kreisel-Goodman paradox can be reconstructed (essentially) line by line in QLP, in the context of such a reconstruction, the proof term corresponding to the constant c which is introduced at step (x) will be a complex term which encodes the structure of the preceding steps (i)–(ix).
This is significant because while we have seen above that in T +, free variables
are treated as universally bound in the derivation of Sect. 3.2), the same effect is achieved in QLP by the use of the traditional first-order quantifiers. Thus while it is the fact that variable x occurs free in the equation Y (h(y, x )) ≡ T which allows this expression to be interpreted as expressing the unprovability of the term Y (h(y, x )), the fact that a formula D has the analogous property would be expressed in QLP as D ↔ (∀x )¬x : D.
In order to reach a contradiction analogous to the clash between steps (x) and
(xi) in the Kreisel-Goodman paradox, an internalizing term d(z) must be found such that f-QLP d(z) : D and also that f-QLP ¬d(z) : D (where it is assumed that z : (D ↔ (∀x )¬x : D) in parallel to the assumption at step (i) of the original derivation). However in order to construct d(z) we must rely on the analog of RfnR for QLP—i.e. (RfnQ) (∃x )x : A → A Like T +, however, QLP also does not contain among its axioms an “implicit” reflection principle of this sort, but rather its “explicit” counterpart LP2. But like ExpRfn, LP2 admits the case where t corresponds to a free variable x . And it is thus straightforward to show that RfnQ is derivable in QLP by intuitionistically valid first-order reasoning about proofs.
This, however, is not sufficient to construct the term d(z) we have described above.
In addition, we must show that the derivation of RfnQ we have just described can itself be internalized within QLP. This is accomplished by the following derivation:
(i) fx : A → A LP2
(ii) fr (x ) : (x : A → A) AxNec
(iii) f(r (x )∀x ) : (∀x )(x : A → A) Eug, (ii)
(iv) fq : (∀x )(x : A → A) → ((∃x )x : A → A) AxNec
(v) fq • (r (x )∀x ) : ((∃x )x : A → A) LP1, (iii), (iv)
In this derivation r (x ) is an axiom term internalizing the instance x : A → A of LP2, and q is an axiom term internalizing the first-order Hilbert axiom ∀x ( A(x ) → B) → (∃x A(x ) → B) where x ∈/ FV(B). The complex proof term q • (r (y)∀y) then serves to internalize the relevant instance of RfnQ, which in turn must serve as a constituent in the construction of the yet more complex term d(z) which figures in the derivation of the paradox.
While the existence of the internalizing constant c required in the original derivation of the Kreisel-Goodman paradox is obtained directly from the rule Int, we can now see that the term d(z) required to reconstruct the reasoning of the paradox in QLP is obtained as a consequence of Lift. As we have just seen, the construction of this term depends not only on the fact that RfnQ can be derived in QLP from LP2, but also that this proof can be internalized in the system itself. In particular, since Lift differs from Int in virtue of being a metatheorem rather than a basic rule, it is also possible to inquire into the status of each of the elementary principles on which its derivability depends. And as we have observed, this requires a means of internalizing each of the basic deductive rules of QLP. If this theory is axiomatized via a Hilbert system as described here, then these correspond to the case of citing an axiom, modus ponens, and universal generalization. These principles are respectively internalized by AxNec, LP1, and Eug.
Upon inquiring further into the status of these principles, it is evident that LP1 can be justified on the basis of the analogy between implication elimination and function application which we have suggested is implicit in the BHK for implication. But finally taking a step towards a conceptually motivated resolution to the paradox, note that it is less clear what to say about either AxNec and (to an even greater extent) Eug. For although in the context of the Theory of Constructions it might at first seem unobjectionable to introduce a primitive constant c to record the fact that we regard
a statement as a “self-evident” truth about constructive proofs (e.g. f-T T ≡ T), it
is already less clear what to say about the interpretation of such a term in the case
where the axiomatic principle in question contains a free variable (e.g. an instance of ExpRfn such as π ⊥x f-T ⊥ ≡ T).
When we move to a system like QLP wherein the sort of quantification over constructive proofs which is implicit in the use of free variables in the Theory of Constructions is made explicit, it is even less clear what to say about the justification of the rule Eug. For it would seem that in order to be intuitively justified in concluding that a particular term (t (x )∀x ) is a proof of a universally quantified statement about constructive proofs (∀x ) A(x ), there must be constructive justification for the fact that a proof which is uniform in x is sufficient to demonstrate that A(x ) holds of all constructive proofs simultaneously. When understood relative to the original formulation of the clause (P∀), this would appear to presuppose that we possess a means of describing the intended range of the quantifiers of a system such as QLP (or analogously for the interpretations of free variables in the Theory of Constructions). And although both systems may be understood as attempting to provide a description of such a domain, what we appear to lack is an independent criterion for deciding whether they have succeeded in adequately doing so.