Desktop version

Home arrow Philosophy

  • Increase font
  • Decrease font

<<   CONTENTS   >>

Diagnosing the Paradox

Our aim in the prior section was to argue that the ultimate evaluation of both the second clause and the Theory of Constructions should be separated from the task of diagnosing and responding to the Kreisel-Goodman paradox. For not only does the adoption of the Theory of Constructions not necessitate that we interpret the intuitionistic connectives using the second clause, but also the inconsistency of the

23The same is also true of Goodman's own derivation of the paradox in [17] in the following exact sense. First note that Goodman's proof is based on applying a fixed-point combinator to the

term h!(y, x ) = λy.λx .π(π yx ⊃1 ⊥)(xx ). As this term does contain an iterated application of

π , a plausible interpretation is that it is derived from attempting to express “x is not a proof of

y” within the language of T relative to its second-clause interpretation. However, the fixed-point which Goodman employs in his derivation is still obtained for the variable y and not x —i.e. it too can be understood as formalizing the existence of a self-referential formula as opposed to a self-dependent proof.

“naive” variant T + turns on assumptions which are independent of the suitability of its language for expressing the second clause.

Once these points are acknowledged, a number of other questions naturally arise:

(1) having eliminated the second clause as the direct source of the Kreisel-Goodman paradox, what other principles might be to blame? (2) was Goodman correct to conclude the most appropriate response to the paradox was to conceive of the universe of constructive proofs as stratified in the manner described by his theory T ω ?

(3) what is the status of his [16] proofs of consistency, soundness, faithfulness, and the interpretatibility of Heyting arithmetic for T ω ? (4) are such results available for unstratified variants of T ω ? and (5) might such systems be of independent conceptual or technical interest?

A truly systematic exploration of these issues is beyond the scope of the current paper. What we hope to achieve here is the more modest goal of laying out the various principles on which the paradox appears to depend and assessing them relative to the goal of providing an “informally rigorous” account of the BHK interpretation of the sort envisioned by Kreisel and Goodman.

Self-Reference and Typing

As we have seen in Sect. 3.2, one of the principles on which the Kreisel-Goodman paradox relies is the existence of terms t containing the operator π satisfying fixedpoint equations of the form Y (t )t (Y (t )). As we have suggested in Sect. 4.2, such terms can be understood to play a role analogous to that of self-referential sentences in traditional formulations of the semantic (or “intensional”) paradoxes such as the Liar and Montague's paradox. In particular, the term Y (h(y, x )) can be understood to express that x is not a proof of Y (h(y, x )) itself.

Whereas the existence of sentences with similar intended interpretations is guaranteed in the classical setting via the arithmetization of syntax and the Diagonal Lemma, the existence of Y (h(y, x )) is a consequence of the existence of fixed-point combinators like Y for the system λβ. But although these phenomena may themselves be understood to share a common basis (cf., e.g., [2, Sect. 6.7]), the question also naturally arises why we ought to base a formulation of the Theory of Constructions on a form of the lambda calculus for which such combinators may be shown to exist.

Part of the answer to this may be understood to follow from the goal of using the language of the Theory of Constructions to formalize the clauses of the BHK (or BHK2) interpretation. For note that it is now a familiar observation that the notions of function abstraction and application which form the basis of the lambda calculus also appear to be implicit in the BHK clauses. This point is often illustrated by pointing out that if the formulas appearing in the rules of a traditional natural deduction system for first-order intuitionistic logic are labeled with terms understood to represent their proofs, then the implication introduction rule can be understood to correspond to a form of function abstraction on proofs similar to the one which is implicit in (P→).

Similarly, the implication elimination rule can be understood to correspond to a form of function application on proofs.24

Such observations provide a strong basis for including the lambda calculus as part of the primitive machinery in terms of which we might attempt to formalize the BHK interpretation. It would seem, however, that the interpretation itself does not nominate a unique form of the calculus to serve in this capacity. For as Sørensen & Urzyczyn note:

[N]ot every lambda-term can be used as a proof notation. For instance, the self-application xx does not represent any propositional proof, no matter what the assumption annotated by x is. So before exploring the analogy between proofs and terms ... we must look for the appropriate subsystem of the lambda-calculus [38, p. 56].

Such observations are often cited as the basis of the Curry-Howard isomorphism which relates logical systems with various typed lambda calculi (such as the simply typed Church-style system λβ→ of [22]). This in turn provides the basis for the interpretation of intuitionistic logic which is provided by systems such as MartinLöf's ITT [1].

However λβ→ can also be distinguished from the system λβ on which we have

taken T to be based in virtue of the fact that the latter allows not only for selfapplication of terms (e.g. xx ), but also for the definition of fixed-point combinators like Y . The potential significance of this point with respect to the status of the KreiselGoodman paradox should now be clear—i.e. although it seems reasonable to base a formal theory in which we might seek to interpret the BHK clauses on some form of lambda calculus, not only does the informal presentation of the clauses fail to pick out a unique system, but there is also reason to suspect that λβ allows for the definition of terms which are not needed for the interpretation of proofs in intuitionistic logic.

Unlike Goodman, Kreisel does not explicitly formulate a paradox as an obstacle to formulating a “naive” variant of the Theory of Constructions. It seems likely, however, that he was aware of the foregoing observations. For in his first formulation of the theory [25, p. 203] Kreisel explicitly restricts lambda abstraction to the class of terms which are asserted by the axioms of the theory to be bivalent in the sense described above. His second formulation [26, pp. 128–129] of the theory is based on a form of typed lambda calculus similar to λβ→. Both approaches thus have the effect of prohibiting Y (h(y, x )) from being a well-formed term of the system in question. As such, Kreisel's apparent reaction to the threat of a paradox pertaining to the notion of construction can be compared both with Russell's [36] reaction to the set theoretic paradoxes and Tarski's [42] reaction to the semantic paradoxes—i.e. the existence of the offending self-referential entities (i.e. sets, formulas, or terms) are excluded on the basis of being improperly formed.

  • [1] Martin-Löf [30] cites the Theory of Constructions as one of several earlier systems which anticipated his development of ITT. It is indeed clear that there is an affinity between the manner in which the two systems define embeddings of intuitionistic logic into variants of the lambda calculus whose constituent clauses are intended to resemble those of the BHK interpretation. (Another historical affinity derives from the fact that Martin-Löf [29] presents ITT as a “predicative” reformulation of the system of [28] which was found to be inconsistent in virtue of Girard's paradox.) An important difference, however, is that constructive proofs are only represented indirectly in ITT as typed. But as typing judgements may not be iterated in ITT in the manner of the π operator, there is no evident manner in which the language of Martin-Löf's system can be used to express the second clause interpretations of →, ¬, and ∀
<<   CONTENTS   >>

Related topics