Home Philosophy Advances in ProofTheoretic Semantics
ReflectionThe explicit reflection principle ExpRfn formalizes the principle that if p is a construction proving A, then A is true. Like decidability, such a principle may plausibly be regarded as part of the intended interpretation of the proof relation. To the best of our knowledge, no one has ever argued explicitly that ExpRfn should be given up in the face of the KreiselGoodman paradox ^{[1]}. But although we do not wish to challenge this consensus, we will now adduce several considerations which suggest that finding an appropriate formulation of reflection in the Theory of Constructions may not be as straightforward as it might appear. The central difficulty is most readily appreciated by again invoking the analogy between the proof relation R( A, p) and the arithmetical proof predicate ProofT (x , y). If we continue to assume that the system in terms of which we reason about the former contains intuitionistic firstorder logic, than one might at first think that the relevant analogs of ExpRfn would take the forms (ExpRfnR) R( A, p) → A (ExpRfnPrT) ProofT(n, 'φ') → φ Here n should be understood as abbreviating a numeral of the form sn (0) for some fixed n ∈ N, which may in turn be understood as the Gödel number of a proof in T. And on this model, it seems reasonable to think of p in A as abbreviating some (possibly complex) closed term in the language of T (or a similar theory) which is intended to denote a particular constructive proof. Note, however, that the principle ExpRfn which is used in the derivation of the KreiselGoodman paradox differs from ExpRfnR and ExpRfnPr not only in that it is formulated in terms of the derivability relation fT of the Theory of Constructions, but also in that it may be used in the case where t is a variable of the theory^{[2]}. But note that the free variable instances in ExpRfnR and ExpRfnPr—i.e. R( A, x ) → A and ProofT(x , 'φ') → φ (where we assume x ∈/ FV( A) and x ∈/ FV(φ))—are equivalent over intuitionistic firstorder logic to the following “implicit” reflection principles: (RfnR) ∃x R( A, x ) → A (RfnPrT) ∃x ProofT(x , 'φ') → φ The contrast between ExpRfnPrT and RfnPr is likely to be familiar: (i) all instances of ExpRfnPr are both true in the standard model of arithmetic and provable in T ⊇ Q; (ii) but while all instances of RfnPrT are true in the standard model, in light of Löb's theorem for T, the only instances of RfnPrT which will be provable in T (provided it is consistent) are those for which T fφ. Moreover, although arithmetical theories T ⊇ Q will satisfy an analog of the rule Int—i.e. if T f φ, then T f ∃x ProofT(x , 'φ')—the result of closing a theory T! which already proves all instances of RfnPrT! will be inconsistent in light of Montague's paradox. A related observation is that not only will instances of ∃y(ProofT(y, '∃x ProofT(x , 'φ') → φ') be unprovable in T when T � φ, theywill in fact be false in the standard model in light of the formalized version of Löb'stheorem. As the foregoing observations pertain to formal provability in the arithmetical theory T, it is not immediately clear what (if any morals) can be read off about the status of ExpRfn or RfnR on their intended interpretations^{[3]}. What they do suggest, however, is that when the term t in ExpRfn is allowed to contain free variables, the effect of including this principle in a theory such as T may be closer to the effect of adding RfnR rather than ExpRfnR. For as is exemplified by the derivation of the KreiselGoodman paradox, the free variables of T (in conjunction with the relevant form of substitution principle) function very much like universally bound variables in firstorder logic. And thus although the Theory of Constructions contains neither quantifiers nor implication in its object language, the instance of ExpRfn with t = x can be understood as expressing for all proofs x , if x is a proof of s, then s is true.

< Prev  CONTENTS  Next > 

Related topics 