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.