Kreisel’s Theory of Constructions, the Kreisel-Goodman Paradox, and the Second Clause
Walter Dean, Hidenori Kurokawa · Trends in logic · 2015
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.