Home Philosophy Advances in ProofTheoretic Semantics
DecidabilityAlthough the strategies of Kreisel and Goodman may be sufficient for obtaining a consistent version of the Theory of Constructions, their approaches are not clearly grounded in considerations which follow directly from the BHK interpretation itself. As such, it seems reasonable to consider the status of the other principles which figure in the KreiselGoodman paradox. We will begin by considering the role of the decidability of the proof relation. As we have seen, this is formalized within the system T by the rule Dec, which may in turn be understood to ensure that terms of the π st are always defined ^{[1]}. We have also seen that the informal motivation for including such a principle derives from the desire to ensure that the relation between constructive proofs and theorems is decidable so as to in turn make available the sort of epistemic account of truth described in Sect. 2. But finally, we have seen that Kreisel introduced the second clause interpretations precisely so as to ensure that the defined proof relation Π( A, s) introduced in Sect. 3.1 is decidable (provided that appropriate assumptions are made about the atomic case, this does indeed follow from the decidability of π st by a straightforward induction on its definition). These considerations notwithstanding, Beeson [3, pp. 404–410] has argued against the propriety of including a rule like Dec in a version of the theory of constructions as follows: (1) he first formulates a formal inconsistency result for a system similar to T +; (2) he then argues that this result can be understood as a reductio of Dec. But since he also advocates for the inclusion of second clauses on the interpretation of →, ¬, and ∀, his overall motivation for rejecting decidability appears somewhat incongruous ^{[2]}. As such, we will henceforth assume that giving up the rule Dec does not correspond to a well motivated response to the paradox.

< Prev  CONTENTS  Next > 

Related topics 