Home Philosophy Advances in Proof-Theoretic Semantics
Without further ado, we now present Kreisel's proposed modification of (P→):
(P2→ ) A proof of A → B consists of a construction that transforms any proof of A into a proof of B together with a proof that this construction satisfies the desired property.
The italicized material represents what is customarily referred to as the “secondclause”—i.e. the requirement that a constructive proof q of a conditional A → B is not just a construction transforming arbitrary proofs of A into proofs of B in the sense of the original clause (P→) but rather a pair ( p, q) consisting of such a construction together with another proof p which demonstrates that q has this property. The second-clause variants are formed by adding similar clauses to (P¬) and (P∀).
Such a reformulation of BHK—which we henceforth refer to as the BHK2 interpretation—was stated for the first time by Kreisel [25, p. 205] and again in [26,
p. 128]. In both instances, Kreisel used the formal language of the Theory of Constructions to formulate (P2→
neither instance does Kreisel motivate the second clause directly nor does he flag that he is intending to either refine or depart from Heyting's original intentions.
These observations notwithstanding, the initial reception of the second clause appears to have been positive—e.g. second clauses are included in both Troelstra [43, p. 5] and van Dalen's [48, p. 24] surveys of intuitionistic logic (again without additional historical comment). But as we will discuss further below, by the early to mid-1980s the consensus appears to have shifted to the view that not only should the second clause not be included in the canonical formulation of BHK, but also that its very formulation rested on dubious assumptions about the nature of constructive proof .
One of our goals below will be to better understand what underlies this shift in opinion about the second clause. Although subsequent commentators have typically followed Troelstra and van Dalen in formulating (P2→) informally, we will suggest below that its status is bound up not only with the issues of impredicativity and decidability discussed in the prior section, but also with certain details about how (P2→) should be formalized within the Theory of Constructions itself. Before turning to such considerations, it will thus be useful to consider both the formulation of the theory and how it may be used to formalize the BHK2 interpretation.