Home Philosophy Advances in ProofTheoretic Semantics
The KreiselGoodman ParadoxAlthough Kreisel [25] sketched a means by which one version of the Theory of Constructions could be shown to be consistent relative to Heyting arithmetic, he also observed that a carelessly formulated version of the theory (e.g. the “starred” theory of [25]) might turn out to be inconsistent. Although he does not explicitly describe what form such an inconsistency might take, in retrospect it is not difficult to see that the intended interpretation of π makes the issue of consistency of a system such as T or T + a significant cause for concern. To better appreciate why this is so, it is useful to begin by considering the following paradox pertaining to the notion of informal (or “absolute”) provability. Suppose that we elect to express this notion by a predicate P(x ) of sentences. Additionally suppose that T is a mathematical theory which we have adopted for reasoning about the properties of P(x ) and that '•' is a device which allows us to name sentences in LT (such as Gödel numbering). In order to support such a mechanism, it seems reasonable to assume that T will contain Robinson arithmetic Q (either directly or by interpretation). And from this it will follow that T will also be able to prove the existence of selfreferential statements about the predicate P(x ) via the appropriate analog of Gödel's Diagonal Lemma. Now consider the following two intuitively correct principles pertaining to informal provability: (RfnP) If A is informally provable, then it is true—i.e. P(' A') → A. (IntP) If we can derive A, then A is informally provable—i.e. fA ∴ fP(' A'). It is now easy to see that the theory T+ obtained by adjoining all instances of RfnP to T and closing under the rule IntP is inconsistent. For by the Diagonal Lemma, let D be a sentence such that (1) T+ fD ↔ ¬ P('D'). Now since (2) T+ fP('D') → D by RfnP, we have by (1) that (3) T+ f ¬ P('D'). But again by (1), we then also have (4) T+ fD. It thus follows by IntP that (5) T+ fP('D'), yielding a contradiction with (3). The observation that an arithmetical theory which extends Q, derives all instances of RfnP, and is closed under IntP is inconsistent has come to be known as Montague's paradox ^{[1]}. Weinstein [49] subsequently suggested that the KreiselGoodman paradox can be understood as a translation of this result into the language of the Theory of Constructions. Goodman offers two expositions of the paradox—an informal one in [16], and a semiformal one in a system similar to the theory T + which is described in the introductory sections of [17]. We quote the former in full: The most natural formalization of the conception [of constructive proof] we have outlined so far is inconsistent. It suffices to construct, using π , a function f such that f (x ) = 0 if and only if x (x ) is a proof that no y proves that f (x ) = 0. Now suppose that y proves that f (x ) = 0. Then f (x ) = 0, and so no y proves that f (x ) = 0. This contradiction, together with the decidability of the proof predicate, shows that no y can prove that f (x ) = 0. Therefore there must be a function g such that, for any x , g(x ) proves that no y proves that f (x ) = 0. In particular, g(g) proves that no y proves that f (g) = 0. That is, f (g) = 0. Hence there is a proof that f (g) = 0, which is absurd [16, p. 5]. The foregoing passage provides the most complete informal description of the antinomy which subsequent authors have repeatedly associated with the Theory of Constructions. It should be borne in mind, however, that Goodman discusses the paradox before providing his “official” formulation of the theory T ω (which he then proceeds to show consistent in a manner we will discuss further in Sect. 5.2). The KreiselGoodman paradox thus should not be understood to correspond to a formal contradiction derivable within any of the variants of the Theory of Constructions which were adopted by Kreisel or Goodman themselves. Nonetheless, it will be useful for our current purposes to consider how the reasoning which Goodman describes can be mimicked in the theory T + of Sect. 3.1. As an initial step, we reconstruct the reasoning described in the prior passage in firstorder logic by taking the binary predicate R( A, p) to express the proof relation(i.e. “ p is a proof of A”), which we will assume satisfies appropriate analogs of Dec, ExpRfn, and Int^{[2]}. Goodman suggests that it is possible to define a function f (x ) (which itself should be thought of as a construction) satisfying the equation (1!) ff (x ) = 0 ↔ R(∀y¬R( f (x ) = 0, y), x (x )) Thus the proposition expressed by f (x ) = 0 can be understood to express something akin to what is expressed by the sentence D constructed in step (1) of the derivation of Montague's paradox—i.e. that f (x ) = 0 is true just in case x (x ) is a proof that this statement itself is not provable. Next suppose that we have the following instance of the explicit reflection principle ExpRfn for R( A, p) (2!) R( f (x ) = 0, y) ff (x ) = 0 But then note that by (1!) and modus ponens we also have (2!!) R( f (x ) = 0, y) fR(∀y¬R( f (x ) = 0, y), x (x )) Thus by ExpRfn again and universal instantiation we have (2!!!) R( f (x ) = 0, y) f ¬R( f (x ) = 0, y) If we now assume that R( A, p) is a decidable relation, then by an analog of the rule Dec we may conclude (3!) f ¬R( f (x ) = 0, y) from (2!!!). This in turn can be understood to correspond to the intermediate conclusion (3) ¬ P('D') in the derivation of Montague's paradox. But now note that since y was arbitrary in the foregoing reasoning, we should additionally be able to conclude by universal generalization that (3!!) f ∀y¬R( f (x ) = 0, y) Noting that the foregoing reasoning is also uniform in the variable x , we also ought to be able to internalize it in a manner analogous to Int. Doing so yields the existence of a function g(x ) such that (3!!!) fR(∀y¬R( f (x ) = 0, y), g(x )) By substituting g for x in (3!!!) we obtain fR(∀y¬R( f (g) = 0, y), g(g)). But then again taking x = g in (1!) and applying modus ponens yields (4!) ff (g) = 0 which can be seen as analogous to step (4) in the derivation of Montague's paradox. Internalizing this reasoning again leads to the existence of another construction h such that (5!) fR( f (g) = 0, h) But now instantiating y by h in (3!!) finally yields f ¬R( f (g) = 0, h), and thus a contradiction with (5!). Although we have not precisely specified the system in which the foregoing derivation is carried out, it is evident that it must satisfy a number of features. First, it must be capable of demonstrating the existence of an appropriate “selfreferential” construction f (x ) as appears in (1!). Second, it must treat constructions as “selfapplicable” in the sense that it makes sense to apply a construction like f (x ) to another construction g(x ). Third, the proof relation R( A, p) must be understood to satisfy the analogs of ExpRfn and Dec ^{[3]} which are employed at steps (2!), (2!!), and (3!). Fourth, it must support the sort of firstorder reasoning which stands behind the use of universal generalization and instantiation employed at steps (3!!), (4!), and (5!). And fifth, it must also support the use of an appropriate analog to Int applicable to reasoning mediated by all of the prior forms of reasoning about the proof relation. Although the system T which we sketched in Sect. 3.1 is designed so as to satisfy the second and third of these conditions, it is not clear whether it satisfies the first, fourth, or fifth. This complicates the task of interpreting the more formal derivation of the paradox described by Goodman [17, Sect. 9] which appears to be an attempt to regiment the prior reasoning in a formal system similar to T . Note, however, that although this system itself does not directly contain the Diagonal Lemma, it is still sufficient for demonstrating the existence of selfreferential statements by another means. For recall that we have defined T so that it includes the untyped lambda calculus in the form of the equational theory λβ (see note 6). Over this theory it is possible to define socalled fixedpoint combinators—i.e. lambdaterms Z such that for any term x , fλβ Zx ≡ x (Zx ). A well known example of such a term is the socalled Curry combinator Y =df λ f.(λx . f (xx ))(λx . f (xx )). Goodman [17] observed that it is possible to use a similar fixedpoint combinator in conjunction with the term π so as to obtain a term t (x ) which can be understood to express that x is not a proof of this term itself. He then proceeds to describe a derivation which can be understood as a “freevariable” variant of (1!)–(5!), in which it is again assumed that an appropriate internalization principle is available. What we present here is a simplication of this derivation which employs the combinator Y itself. First note that although we would naturally formulate the proposition expressed by “x does not prove y” in the language of T as the equation π yx ≡ ⊥, it can also be expressed as a term h(y, x ) =df λy.λx .(π yx ⊃1 ⊥). If we now apply the Y combinator to h(y, x ) we get a term Y (h(y, x )) with only x free such that fT Y (h(y, x )) ≡ h(Y (h(y, x )), x ). We may now reason in T as follows19: (i) fT Y (h(y, x )) ≡ h(Y (h(y, x )), x ) defn. of Y (ii) π(Y (h(y, x )))x ≡ TfT Y (h(y, x )) ≡ T ExpRef (iii) π(Y (h(y, x )))x ≡ TfT h(Y (h(y, x )), x ) ≡ T (i), transitivity of ≡ (iv) π(Y (h(y, x )))x ≡ TfT (π(Y (h(y, x )))x ⊃1 ⊥) ≡ T defn. of h(y, x ) (v) π(Y (h(y, x )))x ≡ TfT ⊥ ≡ T defn. ⊃1
This derivation—which up to this point may be carried out in the system T as presented above—can again be roughly aligned with steps (1)–(4) in the derivation of Montague's paradox—e.g. the use of ExpRfn at step (ii) in the former aligns with the use of RefP at step (2) in the latter, step (vi) of the former corresponds to step (3) in the latter, etc. In order to continue the derivation, however, we need to assume that we are working over a system T + which satisfies the principle Int. We may now continue the derivation as follows20: 19At step (v) we use the rule Δ, π uv ≡ T fT ⊥ ≡ T ∴ Δ fT π uv ≡ ⊥ which can be derived from Dec and the cut rule in T . 20The step analogous to (xi) in Goodman's own presentation of the paradox is (5) on p. 108 of [17]. At this point he simply writes that the relevant internalizing term “must exist” without providing any further explanation. Note also that his system includes a substitution rule of the form Δ fu ≡ v ∴ s ≡ s, Δ[s/x ] f u[s/x ] ≡ v[s/x ] where the extra premise s ≡ s serves to ensure the term s is defined. Hence to bring step xi) into better conformity with Goodman's system, we should also include axioms c ≡ c for the new “internalizing constants”.
Finally, we observe that it follows that the derivability of T ≡ ⊥ from no premises in T + entails that all equations are derivable from no premises in this system. But this is precisely how inconsistency is traditionally defined for systems based on the lambda calculus.

< Prev  CONTENTS  Next > 

Related topics 