Predicativity, Decidability, and the BHK Interpretation

One of Kreisel's goals in proposing the Theory of Constructions was to respond to a potential objection to the BHK interpretation which had been raised by Gödel. This problem can be understood to arise in two stages. First note that the BHK clauses initially appear to provide a characterization of the relation “ p is a proof of A” in terms of the logical form of A, an observation which might in turn be taken to provide an implicit definition of the class of constructive proofs to which the interpretation refers. But on the other hand, note that the BHK clauses themselves cannot be taken as constituting a proper inductive definition of such a class in virtue of the fact that the clauses (P→), (P¬), and (P∀) contain quantifiers which are intended to range over the class of all constructive proofs, potentially inclusive of those which figure in the proof conditions of yet more complex formulas.

We will refer to this prima facie objection to the BHK interpretation as the problem of impredicativity. Gödel remarked on this aspect of the interpretation already in the following passage from a 1933 lecture in which he is attempting to compare the relative merits of Hilbert's finitism (as codified by the system he calls A) and intuitionism as foundational frameworks for formulating mathematical consistency proofs:

So Heyting's axioms concerning absurdity and similar notions differ from the system A only by the fact that the substrate on which the consequences are carried out are proofs instead of numbers or other enumerable sets of mathematical objects. But by this very fact they do violate the principle, which I stated before, that the word “any” can be applied only to those totalities for which we have a finite procedure for generating all their elements. For the totality of all possible proofs certainly does not possess this character, and nevertheless the word “any” is applied to this totality in Heyting's axioms, as you can see from the example which I mentioned before, which reads: “Given any proof for a proposition p, you can construct a reductio ad absurdum for the proposition ¬ p”. Totalities whose elements cannot be generated by a well-defined procedure are in some sense vague and indefinite as to their borders. And this objection applied particularly to the totality of intuitionistic proofs because of the vagueness of the notion of constructivity [13, p. 53].

Gödel can be understood as flagging three points which have played a substantial role in guiding the subsequent understanding of the BHK interpretation: (1) a crucial difference between finitism and intuitionism is that, unlike finitists, intuitionists do not reject the meaningfulness of unrestricted quantification over a potentially infinite domain; (2) the class of constructive proofs form such a totality; but (3) this class should not be regarded as inductively generated in virtue of the occurrence of the universal quantifier over proofs in (e.g.) the clause (P¬).

The first point is stressed by Weinstein [49] in the course of suggesting how the Theory of Constructions might play a role in how an intuitionist ought to reply to Benacerraf's [4] dilemma in philosophy of mathematics. One horn of the dilemma alleges that a “combinatorial” theorist (i.e. one who attempts to identify truth and provability in the characteristic manner of both intuitionism and formalism) will be unable to provide a semantical account of mathematical language which is continuous with the standard referential semantics which we may wish to give for natural language as a whole. But in addition to this, Benacerraf also argues that Hilbert's development of finitism has the added disadvantage of needing to provide distinct accounts of finitary (i.e. “real”) and infinitary (i.e. “ideal”) mathematics.

It is in this regard that Weinstein suggests that intuitionism may have an advantage over finitism in the sense that the BHK clauses can be understood as providing a uniform semantic account applicable to both real and ideal mathematical statements. As he stresses in the following passage, however, this advantage can only be claimed if it is ensured that the proof relation is decidable:

Proofs, for the intuitionist, are not to be equated with formal proofs, that is with some kind of finite quasi-perceptual objects, and, more to the point, decidable properties of proofs may involve considerations about the intuitive content of these mathematical constructions. Hence, it is precisely by admitting as meaningful the notion of a decidable property holding for arbitrary mathematical constructions that intuitionists achieve an interpretation of those sentences which are from Hilbert's point of view devoid of intuitive content. And, for intuitionists, to admit this notion as meaningful is to claim that statements asserting that decidable properties of mathematical constructions hold universally have tolerably clear proof conditions. Thus, by enlarging the contentual portion of mathematics to include universal decidable statements which are not finitary the intuitionists achieve an interpretation of mathematical statements of arbitrary logical complexity [49, p. 268].

Weinstein goes on to explain the connection between the decidability of the proof relation and the attribution of content to mathematical statements as follows:

[I]ntuitionists identify the truth of a mathematical statement, A, with our possession of a construction, c, which is a proof of the statement A. This latter statement, that the construction c is a proof of A, involves no logical operations and is moreover the application [of] a decidable property to a given mathematical construction. Hence, this statement does not itself require a non-standard semantical interpretation and, it is hoped, can be understood along the lines of statements like “The liberty bell is made out of brass” [... ] The idea is just that the intended intuitionistic interpretation of a mathematical language reduces the truth of any sentence of that language to the truth of an atomic sentence which is the application of a decidable predicate to a term and this latter sentence can be understood as having an ordinary referential interpretation [49, pp. 268–269].

Although we will see below that the decidability of the proof relation has occasionally been disputed, these passages make clear why it has traditionally been thought to play a crucial role in ensuring that the BHK clauses are compatible with the general goal of explaining how truth can be understood in terms of constructive provability. To see how this is related to Gödel's second and third points about how the class of constructive proofs may be characterized, note that if we assume that the proof relation itself is decidable, then the clauses (P→), (P¬), and (P∀) are all analogous in form to Π 0 statements in the language of arithmetic—i.e. they begin with an unrestricted universal quantifier over proofs applied to a decidable matrix^{[1]}. As such statements are not in general decidable in the technical sense of computability theory, it seems that there is reason to worry that they do not satisfy Weinstein's criteria of having “tolerably clear proof conditions” even when understood informally.

It is now only a small step which must be taken to justify the use of the term “impredicativity” to label the problem which was described by Gödel. For as Kreisel later observed

[I]t is one of the peculiarities of constructive logic that, for some A, a natural formal proof of A goes via proofs of A → B and ( A → B) → A: such a proof of A actually contains a proof of A → B [27, p. 58].

Although Kreisel formulates this point for formal proofs, there seems to be no a priori reason to suspect that the same comment should not apply to the pre-theoretical notion of constructive proof which the BHK interpretation seeks to characterize. And if this is indeed the case—i.e. that there exist formulas A which are demonstrable by proofs which may contain sub-demonstrations of formulas which contain A itself—then it seems that the quantifier over constructive proofs occurring in (e.g.) (P→) must be understood as ranging over a totality to which it itself belongs.

A variety of other commentators have also used terms like “circular” or “impredicative” to describe either the BHK clauses or the status of implication in intuitionistic logic more generally^{[2]}. As we will see below, it appears that Kreisel added the second clause to the formulations of (P→), (P¬), and (P∀) precisely to avoid such charges and thereby also to provide a characterization of the proof relation which could plausibly be regarded as decidable. What remains to be seen is whether his attempt should be regarded as successful and also whether the various latter day critiques which have been directed towards the second clause also undermine the rationale for adopting the Theory of Constructions itself.

[1] It might also be objected that the explanation of implication given by (P→) is circular because it employs the conditional “if p is a proof of A, then f ( p) is a proof of B” on its righthand side. Note, however, that if it can be maintained that the proof relation is decidable, then it can also be maintained that it is permissible to interpret this conditional truth functionally

[2] E.g. Gentzen [11, p. 167], Goodman [16, p. 7], Troelstra [45, p. 210], Dummett [7, Sect. 7.2], Fletcher [10, p. 81], and Tait [41, p. 221]

Found a mistake? Please highlight the word and press Shift + Enter