Kreisel's Theory of Constructions, the Kreisel-Goodman Paradox, and the Second Clause
Abstract The goal of this paper is to consider the prospects for developing a consistent variant of the Theory of Constructions originally proposed by Georg Kreisel and Nicolas Goodman in light of two developments which have been traditionally associated with the theory—i.e. Kreisel's second clause interpretation of the intuitionistic connectives, and an antinomy about constructive provability sometimes referred to as the Kreisel-Goodman paradox. After discussing the formulation of the theory itself, we then discuss how it can be used to formalize the BHK interpretation in light of concerns about the impredicativity of intuitionistic implication and Kreisel's proposed amendments to overcome this. We next reconstruct Goodman's presentation of a paradox pertaining to a “naive” variant of the theory and discuss the influence this had on its subsequent reception. We conclude by considering various means of responding to this result. Contrary to the received view that the second clause interpretation itself contributes to the paradox, we argue that the inconsistency arises in virtue of an interaction between reflection and internalization principles similar to those employed in Artemov's Logic of Proofs.
Keywords BHK interpretation • Intuitionistic logic • Theory of Constructions • the Kreisel-Goodman paradox • Logic of Proofs
The Brouwer-Heyting-Kolmogorov (BHK) interpretation of intuitionistic logic is traditionally characterized as a means of associating with each formula A of firstorder logic a so-called proof condition which specifies what is required for an object to serve as a constructive proof of A in terms of its structure. An interpretation of this form was originally proposed by Heyting [19–21] and Kolmogorov , leading to the now familiar formulation reported in :
(P∧) A proof of A ∧ B consists of a proof of A and a proof of B. (P∨) A proof of A ∨ B consists of a proof of A or a proof of B.
(P→) A proof of A → B consists of a construction which transforms any proof of
A into a proof of B.
(P¬) A proof of ¬ A consists of a construction which transforms any hypothetical proof of A into a proof of ⊥ (a contradiction).
(P∀) A proof of ∀xA consists of a construction which transforms all c in the intended range of quantification into a proof of A(c).
(P∃) A proof of ∃xA consists of an object c in the intended range of quantification
together with a proof of A(c).
Alongside such a formulation it is conventional to add the caveat that the notions of proof and construction alluded to in these clauses should be understood as primitives, and thus cannot be taken to correspond to derivations in any particular formal system. Rather than providing a formal semantics for intuitionistic first-order logic in a manner parallel to that provided by Tarski's definitions of truth and satisfaction for classical logic, the BHK interpretation is now often described as providing a so-called meaning explanation of the intuitionistic logical connectives —i.e. “an account of what one knows when one understands and correctly uses the logical connectives” .
Despite the fact that it itself is not intended as a mathematical interpretation in the technical sense, the BHK interpretation has been a substantial source of work in proof theory and related disciplines which can be understood as attempting to provide a formal semantics for intuitionistic logic. Among such developments are Kleene realizability, Gödel's Dialectica interpretation, and Martin-Löf's Intuitionistic Type
Theory [ITT]. The class of systems which we will investigate in this paper—i.e. the
so-called Theory of Constructions which was originally developed by Georg Kreisel [25, 26], and Nicolas Goodman [16–18] in the 1960s and 1970s —was also put forth in much the same spirit. For instance Kreisel originally explained the aims of the theory as follows:
Our main purpose here is to enlarge the stock of formal rules of proof which follow directly from the meaning of the basic intuitionistic notions but not from the principles of classical mathematics so far formulated. The specific problem which we have chosen to lead us to these rules is also of independent interest: to set up a formal system, called 'abstract theory of constructions' for the basic notions mentioned above, in terms of which formal rules of Heyting's predicate calculus can be interpreted.
In other words, we give a formal semantic foundation for intuitionistic formal systems in terms of the abstract theory of constructions. This is analogous to the semantic foundation for classical systems  in terms of abstract set theory [25, pp. 198–199] (emphasis in the original).
The Theory of Constructions was thus unabashedly put forth as an attempt to mathematically formalize the BHK interpretation. But as we will see, there are at least two reasons to view the theory as providing a more direct analysis of the individual BHK clauses than the approaches mentioned above. First, (unlike, e.g., Dialectica or ITT) it treats constructive proofs explicitly as abstract objects whose properties we can reason about directly. This allows us to construct expressions which can be understood as direct translations of the BHK clauses into a language with variables which are intended to range over such proofs. Second, Goodman describes his formulation of the system as “a typeand logic-free theory directly about the rules and proofs which underlie constructive mathematics” [17, p. 101]. At least in the eyes of its originators, the Theory of Constructions thus represents an attempt to provide an account of intuitionistic validity in terms of elementary notions which (unlike, e.g., Beth or Kripke models or Kleene realizability) do not presuppose classical logic or mathematics.
But despite these far ranging ambitions, the Theory of Constructions has largely been neglected in surveys of the semantics of intuitionistic logic (e.g. [7, 46]) from the early 1980s onward. Two reasons for this appear to be as follows: (1) a “naive” form of the theory was shown by Goodman [16, 17] to be inconsistent in virtue of a “self-referential” antinomy involving constructive provability (we will see below that this is similar in form to what is now known as Montague's paradox); (2) it was in the context of presenting the Theory of Constructions in which Kreisel first presented a modification to the clauses (P→), (P¬) and (P∀) (which has come to be known as the second clause) which proved to be controversial and has subsequently been excised from modern expositions of the BHK interpretation.
The broad goal of the current paper will be to take some initial steps towards reevaluating the Theory of Constructions with respect to its original foundational goals. We will do so by first focusing on how the aspects of the theory just mentioned—
i.e. Kreisel's second clause and the Kreisel-Goodman paradox—influenced both the original formulation of the theory as well as its subsequent reception. In Sect. 2, we will consider the features of the original formulation of the BHK interpretation which appear to have motivated Kreisel to introduce the second clause—i.e. the decidability of what we will refer to as the proof relation and the putative impredicativity of the clauses (P→), (P¬) and (P∀). In Sect. 3 we will then provide a concise account of the various formal systems considered by Kreisel and Goodman, their use in formalizing the BHK interpretation (inclusive of the second clause), and their relationship to the Kreisel-Goodman paradox. In Sect. 4 we will consider the reaction of various theorists to the Theory of Constructions and the second clause, as well as evaluating Weinstein's  claim that the second clause is itself to blame for the paradox. After concluding that this contention is unjustified, in Sect. 5 we will consider other potential diagnoses of the paradox, as well as discussing the prospects for formulating a version of the Theory of Constructions which addresses Kreisel and Goodman's original foundational goals.
-  As we will see below, the theories which are presented in these papers as “theories of constructions” vary in some crucial respects. Although it is thus inaccurate to speak of a unique formal system as corresponding to “the” Theory of Constructions, we will retain the definite article in speaking of the family of theories in question when no confusion will result