Guilt by Association?
The passages collected in the prior section make clear that not only have most commentators reacted negatively to Kreisel's proposed modifications to the clauses (P→), (P¬), and (P∀), but also that this reaction has contributed to their assessment of the Theory of Constructions itself. Against this backdrop, we now wish to frame two observations: (1) the second clause interpretations of the intuitionistic connectives play no role in the formulation of the Theory of Constructions itself—rather the theory merely provides a formal language in which these interpretations can be expressed; (2) the Kreisel-Goodman paradox also does not arise in virtue of assigning the connectives appearing in its premises their second clause interpretations.
The first point may be appreciated by simply recalling that variants of the Theory of Constructions like T are indeed “logic free” in the sense that they do not contain logical connectives such as →, ¬ or ∀ amongst their primitive symbols. Rather such systems contain other primitives—e.g. the abstraction operator λ and the proof operator π —which Kreisel and Goodman hoped to show are sufficient for analyzing the meaning of the intuitionistic connectives. As we have seen, these analyses take the form of providing a definition of a predicate Π( A, s) which they suggest can be
understood as formalizing the second clause variants of the traditional BHK clauses.
Only once such a definition has been undertaken may we ask whether the defined proof relation Π( A, s) has certain properties such as decidability. But as we are now in a good position to appreciate, such features apply to the “internal logic” of a theory which is being interpreted in a system like T and not to the formal properties of the Theory of Constructions itself . But from this it also follows that since the second clause variants of (P→), (P¬), and (P∀) are conditions which we attempt to interpret in T , they are no more an intrinsic feature of such a system than is the decision to interpret the natural numbers as finite von Neumann ordinals an intrinsic feature of ZF set theory.
It is also evident that the second clause plays no direct role itself in the formulation of the Kreisel-Goodman paradox as discussed in Sect. 3.2. One indication of this is that although our proposed regimentation of Goodman's informal description of the paradox is conducted in first-order logic, no special treatment is accorded to the connectives →, ¬ or ∀. Similarly, when we attempt to mimic this reasoning in T +, it is evident that the derivation of a contradiction does not require that we interpret the occurrences of the logical connectives occuring in the semi-formal version in accordance with the second clause interpretations (K→), (K¬), or (K∀).
From this it would appear to follow that Weinstein is unjustified in at least his contention that the Kreisel-Goodman paradox is directly engendered by reasoning with the intuitionistic connectives relative to their second clause interpretations. What remains to be seen, however, is whether it is possible to sustain what appears to be his more general point—i.e. that the paradox reveals that any attempt to formalize
the clauses (P2 ), (P2 ), and (P2 ) will result in a system which is inconsistent in virtue→ ¬ ∀
of being “self-reflexive”.
In evaluating this claim, it seems possible to interpret the relevant notion of “selfreflexivity” in one of three ways which we will respectively label “self-applicability”, “self-dependency”, and “self-referentiality”. We have already considered a sense in which the Theory of Constructions formalizes a notion of “self-applicable” proof in the sense that it allows for iterations of the proof operation in expressions such as π(π st1)t2 ≡ T. But on its own, this property does not seem to lead obviously to any sort of antinomy about the proof relation R(x , y). Some evidence of this is provided by the fact that it is not only consistent with familiar systems T of formal arithmetic that there exist statements A and pairs of numbers n, m such that
ProofT(n, 'ProofT(m, ' A')'), but instances of such statements will typically be
provable in T itself.
The foregoing example pertains only to self-applicability in the general sense that the proof relation R(x , y) is allowed to hold of a sentence A and a proof s in the case where A itself contains R(B, t ) for some sentence B and proof t . But although it would seem that this is all that is needed for the formulation of the second clause, it might also be thought that the Kreisel-Goodman paradox turns on the existence of proofs which are “self-dependent” in the sense that their definitions rely on the fact that they must be understood to already exist. An example would be witnessed by the existence of a statement D and a proof u such that R(R(D, u), u), whose truth would appear to entail that u is self-dependent in the sense that the statement proven by u refers to u itself.
In his second exposition, Goodman appears to attribute the paradox to the existence of proofs with this property:
There is an essential impredicativity in our definition of implication. For [Π( A → B, y)] involves quantification over all proofs of A, including proofs which may themselves have been built up in some way from y. Unless something is done to moderate this impredicativity, it actually leads to paradox [17, p. 107].
Goodman says this after defining Π( A → B, y)—i.e. the proof condition for the implication A → B—in the same manner as Kreisel's second clause variant (K→). It is notable, however, that in our reconstruction of Goodman's formulation of the paradox the derivation of an inconsistency depends on our ability to construct in T a term Y (h(y, x )) which functions in a manner analogous to the formula D in the derivation of Montague's paradox. But although this statement is indeed self-referential in the traditional sense of being provably equivalent to its own unprovability, it does not depend on the existence of a proof which is self-dependent in the sense just described.23
Note finally that we have already seen in Sect. 2 that the concerns which Goodman raises about the impredicativity of implication appear to already arise for the original BHK clause (P→). As we suggested there, this may indeed highlight an important conceptual problem about how the notion of constructive proof should be understood. It seems, however, that the sort of “self reflexivity” which engenders the KreiselGoodman paradox is more closely related to traditional forms of self-reference which figure in classical inconsistency results like Montague's paradox. And this in turn suggests that not only is the paradox not engendered by the second clause in the direct sense of requiring that we interpret the logical notions which figure in its derivation in accordance with (P2), (P2 ), and (P2 ), but also that it is not engendered indirectly → ¬ ∀
by introducing an impredicative element into the concept of constructive proof whichwas not already present.
-  Among subsequent commentators on the Theory of Constructions, Troelstra  presentsa version of the theory in which Π( A, s) is itself treated as a primitive notion, whereas Sundholm [39, 40] (while clearly aware of the technical distinction between π st and Π( A, s)) continues to speak of properties like decidability as features which might be stipulated (rather than proven) to hold for Π( A, s)
-  For instance in the case where T fA, the existence of n and m such that T fProofT (n, 1ProofT (m, 1A1)1) is a straightforward consequence of the first and third HilbertBernays derivability conditions for ProofT (x , y)