Desktop version

Home arrow Philosophy arrow Advances in Proof-Theoretic Semantics

Decidability

Although 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 Kreisel-Goodman 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.

  • [1] For reasons discussed in footnote 18 the same effect is also formally achieved by either reasoning about the proof relation in intuitionistic first-order logic or by adopting Kreisel's [26] proposal to base the Theory of Constructions on the calculus λβ→ (wherein all terms always reduce to normal form).
  • [2] A similar reaction is voiced by Sundholm [40, p. 16]: “Since [the second clauses] had been introduced by Kreisel solely to guarantee that decidability, I found Beeson's theory lacking proper motivation as well as wanting in simplicity”
 
Found a mistake? Please highlight the word and press Shift + Enter  
< Prev   CONTENTS   Next >

Related topics