Desktop version

Home arrow Philosophy arrow Advances in Proof-Theoretic Semantics


The 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 Kreisel-Goodman 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 first-order 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 Kreisel-Goodman paradox differs from ExpRfnR and ExpRfnPr not only in that it is formulated in terms of the derivability relation f-T 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 first-order 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 Kreisel-Goodman paradox, the free variables of T (in conjunction with the relevant form of substitution principle) function very much like universally bound variables in first-order 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.

  • [1] A partial exception to this is Kreisel who, after observing that ExpRfn is “obvious on the intended interpretation” excludes this principle from his official “unstarred” theory. Although he does so on the basis of his other observation that ExpRfn is “troublesome for the consistency proof” [25,p. 204], he does not offer further non-instrumental justification for this.
  • [2] Moreover, inspection of the proof reveals that this is essential. For if x were not understood as free on the lefthand side of step ii), then it would be not admissible to substitute c for x at step (xi). 34For discussion of a related point see [31, pp. 137–138]
  • [3] Goodman's formulation of the analogous rule in T ω [17, p. 118] is

    Δ, ax ≡Tf-T ω bx ≡ T

    Δ, Ga ≡ T f-T ω π 3ab(pab) ≡ T

    where x is stipulated to not occur free in Δ, a or b and pab is explained as being an “infinite canonical proof of ab ... which depends only on a and b and not on the structure of the formal proof [of bx ≡ T from Δ, ax ≡ T]” [17, p. 111]. Despite Goodman's disavowal of the relationship between pab and the relevant formal derivation in T , we will see that it is precisely this dependency which is made explicit in the system QLP described below

Found a mistake? Please highlight the word and press Shift + Enter  
< Prev   CONTENTS   Next >

Related topics