 Home Philosophy Advances in Proof-Theoretic Semantics

# Stratification

Goodman'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 “self-referential” 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 :

The set-theoretic 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.) Martin-Löf  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 so-called grasped domain of constructions is introduced to play the role of a level in the stratified hierarchy of constructions as just described ; (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  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 pre-theoretical 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 .

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 type-free 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 . 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 well-formed, 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.

•  27Goodman [17, pp. 109–110] describes such a domain as the class of constructions which has been “grasped as a totality” and which is maximal in the sense of “including everything which is understood when its elements are understood”
•  Especially problematic in this regard is the inclusion in T ω of a so-called reducibility operator F . Roughly speaking, F is supposed to achieve the role of reducing a “noncanonical” proof of an assertion to the objects pertaining to some level Ln in the hierarchy of constructions (i.e. one which might make reference to proofs of yet higher level) to a proof which is present at level Ln+1. Such an assumption plays an important instrumental role in Goodman's formulation of the clause (P2 ) in T ω as it allows him to replace the quantifier over all constructive proofs with one which only ranges over the level one higher than that of the term interpreting AB. To justify this he writes “It seems to us essential to the intuitionistic position that given a fixed assertion A about a well-defined domain, there is an a priori upper bound to the complexity of possible proofs of A” [17, p. 111]. But as Weinstein  observes, it is not at all clear whether there is anything implicit in the BHK interpretation itself which justifies this assumption
•  This is at least true of the formulations given by Heyting [20, pp. 13–15] and Kolmogorov [24, pp. 329–330]. Martin-Löf [30, p. 128] claims that typing is already implicit in clause (P→) if we additionally accept that every function must have a type as its domain. But it is unclear what necessitates that we adopt such an assumption Found a mistake? Please highlight the word and press Shift + Enter Related topics