Home Philosophy Advances in ProofTheoretic Semantics
StratificationGoodman's reaction to the paradox was guided by his view that an adequate foundation for intuitionistic logic must presuppose neither logic nor a doctrine of types. He thus proposed to retain the untyped lambda calculus as the basis of the Theory of Constructions and at the same time conceive of constructions as stratified into “levels” which he likens to set theoretic ranks.26 Thus while we have just seen that Kreisel's reaction to the “selfreferential” paradox about provability was at least superficially similar to Russell's resolution to the set theoretic paradoxes, Goodman explicitly suggests that his proposed resolution can be understood as analogous to that of Zermelo [50]: The settheoretic paradoxes are resolved by observing that sets must be sets of objects already at hand. Similarly we suggest that proofs must be about objects already constructed. Just as in Zermelo set theory there is an implicit cumulative theory of types, so we propose to formulate a theory of constructions involving a cumulative theory of levels. At the bottom level we will have constructive rules operating on each other ... Given any level L, we suppose that we can extend L to a new level containing all the objects of L, all proofs about objects of L, and certain additional constructions to be described below ... We emphasize that this is not a stratification by logical type, but rather a stratification according to the subject matter of proofs [17, p. 109]. In outline, Goodman proposes to implement this proposal by defining a “stratified” version of the Theory of Constructions T ω with the following features: (1) the untyped lambda calculus λβ is retained, as well as the possibility that terms may 26Goodman's other apparent reason for employing the untyped lambda calculus in formulation of T ω pertains to his desire to use the system for interpreting Heyting arithmetic. In particular, in order to define the natural numbers in the language of T ω , he first uses the pairing functions to define 0 = λx .λy.x , and n+1 = Dn0. He then shows that it is possible to use a fixed point combinator similar to Y in order to define a decidable natural number predicate. Goodman's foundational goals are thus somewhat more ambitious than those of (e.g.) MartinLöf [29] in the sense that he hoped to reduce not only intuitionistic logic, but also intuitionistic arithmetic to a primitive theory of constructions which does not itself contain a basic natural number type. be undefined, identity is to be understood intensionally, etc.; (2) the notion of a socalled grasped domain of constructions is introduced to play the role of a level in the stratified hierarchy of constructions as just described ^{[1]}; (3) such levels are understood as proceeding from a basic level B =df L0 and forming a hierarchy L0 ⊆ L1 ⊆ L2 ⊆ ... over which the variables of T ω are intended to range; (4) various primitive terms are introduced into the language of T ω to formalize this conception (e.g. Bx iff x is a basic level construction, Gx iff x is a grasped domain, Exy iff y is the grasped domain corresponding to the level extending x , etc.) together with axioms which ensure that they have various intended properties such as decidability; (5) the binary proof operator of π xy of the system T is replaced with a ternary proof operator π 3 xyz with the intended interpretation “x is a grasped domain containing y, and z is a proof that yw ≡ T for all w in x ”. Goodman's proposed resolution to the paradox [16, pp. 111–112] may be understood as turning on the following observations: (a) for each level Ln it is possible to formulate a term tn akin to Y (h(y, x )) which may be interpreted as expressing its own unprovability by all constructions at level n; (b) although it is still possible to reach a conclusion analogous to (ix) in the original demonstration expressing that such a term is true (i.e. T ftn ≡ T), proving this statement involves reasoning with a free variable over Ln ; (c) if we let cn denote this derivation, Goodman's rules for grasped domains only allow us to show that cn is in Ln+1, but not Ln ; (d) as such, no contradiction arises since cn is not in the range of the implicit universal quantifier over proofs which are asserted by tn ≡ T to not be proofs of tn . Needless to say, the fact that we cannot derive a formal contradiction in T ω in this manner does not itself constitute a proof that the system is consistent. For this reason, much of [16] is taken up with providing a formal consistency proof for T ω. However, the details of Goodman's proof of this are complex. And thus rather than commenting further on this feature of T ω, we offer the following general observations about the role he took this theory to have in resolving the paradox. First, note that it is evident that the transition from T to T ω is purchased at the cost of a substantial complication not only of the class of primitive operations and relations on constructive proofs which must be adopted (of which we have mentioned only a few), but also with respect to the axiomatic principles which must be assumed to hold of them to correctly describe the relationship between the levels in the stratified hierarchy of constructions which is the intended model of Goodman's theory. It would seem, however, that if we wish to provide an “informally rigorous” account of why T ω is indeed the appropriate formal system with which to achieve Kreisel and Goodman's goal of providing a semantic foundation for intuitionistic logic, then each of these principles must be individually justified in terms of the network of pretheoretical notions which figure in the BHK interpretation itself. However, it is unclear whether it is possible to do so in all of the relevant cases ^{[2]}. Second, one might reasonably question the basis of Goodman's claim that the stratification of the universe of constructions is a matter of “the subject matter of proofs” as opposed to one of “logical type”. For on the one hand, while the basis of Goodman's original contention that a foundation for intuitionistic logic must itself be typefree presumably derives from the observation that the notion of type does not explicitly figure in the original expositions of the BHK interpretation, it is equally evident that these expositions also do not contain any explicit reference to a stratification of constructive proofs into levels resembling set theoretic ranks ^{[3]}. And on the other hand, one consequence of Goodman's introduction of the ternary proof operator is to allow us to conclude that π 3st u ≡ ⊥ whenever it may be shown that the proof u is not in Es (i.e. the grasped domain formed by extending s). Thus although statements of the exhibited sort are still treated as syntactically wellformed, they are simply stipulated to be false whenever an appropriate containment relation fails to hold between levels and proofs. And thus although T ω does not contain the formal machinery of type judgements, the effect of typing seems to be implicitly enforced by other means.

< Prev  CONTENTS  Next > 

Related topics 