The Reception of the Theory of Constructions and the Second Clause
The foregoing derivation is carried out in the system T +. As we have noted, this system does not coincide with any of the variants of the Theory of Constructions explicitly adopted by Kreisel or Goodman. Nonetheless the derivation bears sufficient resemblance to that sketched by Goodman [17, pp. 107–109] so as to be a reasonable candidate for what we might call the formalized Kreisel-Goodman paradox. And although Goodman went on to develop T ω specifically to avoid the paradox, this initial observation about the “naive” theory we have been discussing played a substantial role in shaping subsequent opinion about the Theory of Constructions itself.
Before considering the various ways in which one might react to the paradox directly in Sect. 5, our goals in this section will be twofold. First, we will briefly describe the manner in which the conventional wisdom about the significance of the Theory of Constructions shifted during the 1970s and 1980s. Second, we will argue that several of the criticisms which have been directed against the theory appear to be based on misapprehensions about its relationship to the second clause and to the Kreisel-Goodman paradox.
The shift in the consensus about the status of the Theory of Constructions can be readily appreciated by comparing the following passages taken respectively from the prefaces of the first (1977) and second (2000) edition of Dummett's Elements of Intuitionism:
The mathematical theory of constructions is of the greatest importance for the foundations of intuitionistic logic, and it was with greatest regret that I omitted all but a mention of its existence; but it is as yet in an imperfect state, and its formulation is far too complicated to permit of a brief summary [7, p. viii].
In the original Preface I mentioned with enthusiasm the theory of constructions inaugurated by Kreisel, aimed at supplying a canonical semantics for intuitionistic logic; unfortunately, it did not prove fruitful [7, p. iv].
Although Dummett provides no further explanation for this change of heart, his reaction echoes that of other theorists who, in the intervening years, had come to conclude that the Theory of Constructions not only did not live up to Kreisel's promise of providing a “semantical foundation” for intuitionistic logic, but was also ill-motivated because of its association with the second clause. As we are now in a good position to appreciate, however, the formulation of a theory such as T is independent of how (or even if) we elect to attempt to use its object language to formalize the BHK clauses. And as such, it seems that criticisms of the Theory of Constructions which are grounded in objections to the propriety of adopting the second clause are likely to be off base.
Putting this observation to the side for the moment, it is also possible to identify two broad classes of criticisms which have been targeted at the second clause itself.
The first of these is that the transition from (e.g.) (P ) to (P2→) either adds nothing to the original BHK interpretation or does not serve to resolve the problems which appear to have motivated Kreisel to introduce it. For instance, Girard  says the following:
Since the → and ∀ cases were problematic (from [the .. .] foundational point of view), it has been proposed to add to (P→) [... ] the codicil “together with a proof that f has this property”. Of course that settles nothing, and the Byzantine discussions about the meaning which would have to be given to this codicil—discussions without the least mathematical content—only serve to discredit an idea which, we repeat, is one of the cornerstones in Logic [12, p. 7].
Although Girard does not comment further on the claim that the second clause is “without mathematical content”, several subsequent commentators appear to expand on his point that it leads to a substantial complication in how we should understand the meaning of implication. For instance Prawitz writes
One may ask whether [what is known in understanding an implication] should not consist of a description of the procedure together with a proof that this procedure has the property required, as suggested originally by Kreisel . But this would lead to an infinite regress and would defeat the whole project of a theory of meaning as discussed here [35, p. 27]
Such passages suggest that far from overcoming the apparent deficiency in the original BHK account of intuitionistic implication—i.e. that it requires that we understand what it means to quantify over all constructive proofs—the second clause in fact makes matters worse in the sense of introducing another kind of infinitary condition as part of its meaning.
Prawitz also does not expand on what he means by speaking of an “infinite regress”. But one interpretation is that he too is making the point that in order to formulate the second clause, we must allow for the fact that it makes sense to think of the proof relation as holding between a proof p and a sentence A which may itself make reference to this relation (and thus to other proofs and formulas). If it is acknowledged that this is legitimate, then there seems to be nothing to prohibit arbitrary iterations of the proof relation. For instance, if we continue to use R(x , y) to denote this relation, then an example of the sort of “regress” Prawitz appears to have in mind might correspond to the existence of a statement A and proofs p1, p2, p3,... such that R( A, p1), R( p2, R( A, p2)), R( p3, R( p2, R( A, p2))), . . . It is evident that the syntax of the Theory of Constructions allows us to express the existence of such a sequence in the sense that π ts1 ≡ T,π(π ts1)s2 ≡ T, π(π(π ts1)s2)s3 ≡ T,... are all well-formed formulas.
One might reasonably wonder on this basis if grasping the second clause interpretation of a formula ever requires that we grasp such an infinite sequence of conditions. Beeson discusses a related point:
Is it necessary to include [the second] clause? What does it really mean? At one extreme is the view that one should simply delete this clause: a constructive proof should contain the information a computer needs to verify the computational facts […] At the other extreme is the view that the “supplementary data” is a proof itself: a proof that q does indeed transform any proof of A into a proof of B. The difficulties with this view seem to be that (i) it makes the explanation of proof highly impredicative, destroying any hope of explaining proofs of complicated propositions in terms of proofs of simpler ones; and (ii) it seems to assume that “ p is a proof of A” is a mathematical proposition “on the same level as” A itself, in particular, capable of being proved mathematically.” [3, p. 402]
We will come back to discuss the second concern described by Beeson—i.e. that it assumes that p is a proof of A expresses a mathematical proposition “on the same level” as expressed by A itself—in the course of comparing the Theory of Constructions to systems like ITT (wherein p is a proof of A is regarded as a judgement as opposed to a proposition). But with regard to the first issue he raises, note that while Kreisel appears to have introduced the second clause precisely so as to avoid the form of impredicativity discussed in Sect. 2, Beeson suggests that it is this step itself which introduces impredicativity into the interpretation of intuitionistic implication.
Although Beeson also fails to expand upon the precise form this impredicativity takes, it again seems likely that what he also has in mind has something to do with the self-applicability of the proof relation. For note that not only does the formulation of the second clause require that we countenance the existence of proofs p which stand in the proof relation to statements A which may themselves refer to other particular proofs q (e.g. for A of the form R(B, q)), but also the case where A may contain a quantifier over all proofs (e.g. for A of the form ∀x R(B(x ), x )), presumably inclusive of p itself.
A potentially related point about the existence of proofs with this property is made by Weinstein in the following remark about the second clause:
If […] we suppose that universal quantifications over the universe of constructions applied to decidable properties have decidable proof conditions then we may view [(P2 )] as providing → an assignment of decidable proof conditions to each formula of the language of arithmetic […¶…] This means of securing the decidability of the proof conditions for formulas of arithmetic is not without cost. The alternative statement of the proof conditions for conditionals is self reflexive in a way that the original explanation was not. Both Kreisel and Goodman noticed that this self reflexivity leads to paradox in a theory of constructions which includes a reflection principle for the primitive which constructs the proof conditions for quantification over the universe of constructions applied to decidable properties [49, p. 264].
Rather than simply suggesting that the second clause is ill-motivated in virtue of leading to the sort of infinitary or impredicative proof condition mentioned by Prawitz or Beeson, Weinstein goes beyond this and suggests that it leads to a form of “selfreflexivity” which in turn is responsible for the Kreisel-Goodman paradox. It is this claim which we will focus on in the next section.