We turn then to Chapter 6 of Luca’s book, ‘The Stratified Conception’.
This chapter starts with a brief discussion of Russell’s aborted ‘zigzag’ theory, which tries to modify naive comprehension by requiring that it applies only to sufficiently “simple” properties (or strictly, simple propositional functions). It seems that Russell thought of the required simplicity as being reflected in a certain syntactic simplicity in expressions for the relevant properties. But he never arrived at a settled view about how this could be spelt out. It is only later that we get a developed set theory which depends on the comprehension principle being constrained by a syntactic condition. In Quine’s NF, the objects which satisfy a predicate A form a set just when A is stratifiable — when we can assign indices to its (bound) variables so that the resulting A* would be a correctly formed wff of simple type theory. And so the rest of Chapter 6 largely concerns NF.
Luca also touches on NFU, the version of Quine’s theory which allows urelemente. And — though this is a matter of emphasis — I’m was a bit surprised that the main focus here isn’t more consistently on this version. At the beginning of the book, Luca seems to hold that the most natural form of a set theory should allow for individuals: thus he describes the iterative conception (for example) as being of a universe which starts with individuals, and then builds up a hierarchy of sets from them. And if, when considering its technical development, we then concentrate on an iterative set theory without individuals, that’s because of easy equi-consistency results: adding urelements to ZFC’s theory of pure sets doesn’t change the scene in a deep way, so for many purposes it just doesn’t matter whether we discuss ZFC or ZFCU. But, famously, it isn’t like this with NF vs NFU. The consistency status of NF is still moot (Randall Holmes claims a proof, but its degree of opacity remains extremely high), and NF is inconsistent with Choice. While NFU is well known to be consistent (if enough of ZF is) and is consistent with Choice. Thus Holmes himself writes of NF and its variants that “only NFU with Infinity, Choice and possibly further strong axioms of infinity … is really mathematically serviceable.” That’s a judgement call, given Rosser’s earlier work on maths within NF. But it is certainly arguable that NF is something of a curiosity, while NFU wins mathematically. And given that it is more natural anyway in allowing for individuals, I’d have rather expected that NFU would have been the ‘best buy’ stratified theory for Luca to choose to highlight.
Now, some would say that a chapter called ‘The Stratified Conception’ must be mistitled — for there isn’t really a conception of the set-theoretic world at work here! In §6.4, Luca talks of the ‘received view’ of NF(U) as being, precisely, a set theory which lacks conceptual motivation. Thus he quotes D. A. Martin calling it “the result of a purely formal trick … there is no intuitive concept”. Similarly, Boolos writes that NF “appear[s] to lack a motivation independent of the paradoxes”. Fraenkel said “there is no mental image of set theory” which leads to NF’s characteristic axiom. If this received view is right, then Luca’s chapter could be very short!
But after outlining NF (and some of its oddities!) in §6.2, putting it into the context of the paradox-avoiding choice between indefinitely extensibility and universality in §6.3 (NF chooses the second), and noting the received view in §6.4, Luca turns in §6.5 to describe how there is a path from type theory to NF. To negotiate the annoying repetitions of e.g. cardinal numbers at each type, Russell had already adopted a policy of using untyped claims which are to be read as typically ambiguous. So allowed instances of comprehension should be stratifiable though the explicit type indications are dropped. Then, as Luca explains, it is a rather natural step to consider keeping the stratifiable instances of comprehension while no longer supposing that the hidden stratifications are ontologically significant — i.e. we collapse the ontological type hierarchy into a single untyped domain. Which is what NF does (and indeed the theory is equiconsistent with adding to the simple theory of types an axiom schema that registers type ambiguity by saying that a typed wff is equivalent to the result of raising the types of all variables in that wff by one). So — to some extent contra the ‘received view’ (though in fact this is quite well known) — there is a pretty natural route which ends up with NF(U).
So far so good. But while observing that we can arrive at NF(U) by collapsing types gives the theory some motivation, more than the baldest version of the ‘received view’ might allow, that doesn’t yet really give us a positive conception of the resulting world of sets. We have a genealogy, but more needs to be said: and that’s going to be the business of Luca’s §§6.6 and 6.7, to be discussed in the next post.
But first, it is perhaps worth noting that NFU can be developed without initially introducing the stratifiability condition at all (well, I at least find this intriguing!). Here I’m thinking of the axiomatization for set theory given by Randall Holmes in his Elementary set theory with a universal set. The domain contains atoms, sets, and (primitive) ordered pairs. Assume as fixed background that (i) extensionality holds for sets, (ii) atoms have no members. And now consider the following bunches of axioms:
- Axioms telling us that the sets form a Boolean algebra — there’s the empty set at the bottom, the universal set at the top, every set has a complement, any two sets have an intersection and a union which is also a set.
- An axiom of set union of the usual kind (given a set A of sets, there’s a set which is the union of the members of the members of A).
- Some axioms telling us that every object has a singleton. Some axioms telling us that for any two objects there is an ordered pair of them, and that pairs and projections from pairs behave sensibly. Various axioms telling us sets have Cartesian products, and that binary relations as sets of ordered pairs behave sensibly.
So far, with details filled in, we get what might look to be a pretty natural base theory if we are trying to articulate a conception of sets which permits sets to behave the Boolean way we naively expect, and also allows a few familiar elementary constructs in the theory of relations and functions. Now suppose we add to this base theory two more specific axioms. These might not be ‘axioms we first think of’ but the first looks entirely unsurprising as a set-theoretic truth; and while the second gives us a set which is ‘too big’ by limitation-of-size principles, if we are going to buy a universal set, then this seems a reasonably natural assumption of the same flavour too.
- For any relation, there is a set of the singletons of the objects that stand in that relation.
- The pairs (x, y) where x is a subset of y form a set.
And now here’s the pay-off. A theory with these axioms proves NFU’s stratified comprehension axiom as a theorem. And (still assuming the fixed principles (i) and (ii)), stratified comprehension gives us everything else except the defining axioms for pairs. I’m not quite sure what to make of this re-axiomatization result. But it might suggest that we can also motivate a route to NFU that doesn’t depend on what could perhaps still look like trickery with types.
To be continued.
Seeing stratified comprehension as what you get when you take typed comprehension and drop the type labels does help one get a better feel for what NF is doing. But it also has a disappointing and rather puzzling limitation. It is natural and quite safe to generalize simple type theory to a theory of cumulative types, in which a set of type n can have as elements any sets of type k<n. So, one is prompted to try loosening the stratification constraint in NF's comprehension condition to one of 'cumulative stratification'. The formal articulation is straightforward but, sadly, it immediately leads to inconsistency using the principle that any two sets with the same elements are identical. So, one wonders, what is really going on?
I don’t think that finding a pretty natural route from type theory to NF(U) is very contra the ‘received view’ — NF(U) would still appear to “lack a motivation independent of the paradoxes”, for example, especially since type theory was also motivated by the paradoxes. And since type theory is not a very natural starting point, a route from type theory to NF(U) can’t make NF(U) natural. That each step is natural, given the starting point, does not mean the steps transfer naturalness to the system they’re steps to.
Incurvati points out that there is also a route from type theory to ZF, iterative set theory, and the cumulative hierarchy, and he quotes Godel as saying that, because of such routes, only one solution to the paradoxes has been found, and it’s type theory.
But the iterative conception has its own intuitive motivation. It doesn’t have to be seen as motivated by the paradoxes; and the ‘paths’ can be followed in either direction: if the cumulative hierarchy is what you get if you start with type theory and remove ‘certain superfluous restrictions’, then type theory is what you get if you start with the cumulative hierarchy and put superfluous restrictions in.
I have to wonder whether type theory is getting the credit because it came first historically (at least in a rational reconstruction), so that if something can be seen as a simplification of type theory, that’s treated as what it essentially is.
Anyway, re later §s, I hope you (or someone) explains how the idea of sets as objectified properties works, because I’ve read those §s several times now an still can’t make sense of it. At some points, it seems that sets are extensions — a set is the set of objects that have the corresponding property — and that also seems to be what the logical conception of sets was about. On p 174, we even have “x ∈ y is to be read as x has property y”.
But at other points (p 176), it seems that something completely different is going on: sets are proxies for properties, or are implementing properties, in such a way that “a particular association of properties with objects is arbitrary: there is no reason for thinking of an object as a proxy for a certain property rather than another one.” And “Should we identify a property P with a different object in the first-order domain, P would still hold of the same things.” If it’s a set, rather than some other sort of object, that P is identified with, it’s hard to see how that set could be P’s extension.
The part on p 177 about being “∈-permutation invariant” reminds me of Putnam’s cats and cherries.
Later on page 177, we’re back to saying sets are extensions.
Re type theory, I don’t think that being motivated by Fregean considerations precludes being motivated by the paradoxes, especially since it’s largely Fregean considerations that gave us the disastrous idea of unrestricted comprehension in the first place.
I didn’t think my saying “type theory is not a very natural starting point” would be very controversial. Even your blog post described it as having “annoying repetitions”. Even Quine, whose esteem for the Fregean “naive” conception was so great that he thought it the only intuitive one and that its inconsistency meant “common sense is bankrupt”(!) explicitly included type theory among the proposals he thought lacked an intuitive foundation (p 128).
Also Quine on type theory, as quoted on p 172:
In any case, even if type theory is natural, the naturalness of steps leading away from it would not mean that any of its naturalness is necessarily transferred, step by step, to the other end of the path.
Re later sections, I hope you explain the ‘proxy and permutation’ idea in a way that makes it clearer what’s going on. In the places where it doesn’t seem that the set that goes with a property would be a set containing (just) the things that have the property, it seems the idea is something like this: