The next chapter of Conceptions of Set discusses set theories like NF that modify naive comprehension by imposing a stratification condition. My friend Thomas Forster, NF-iste extraordinaire, has been looking at some of Luca’s book too, and dropped me this note, which I thought it would be good to share here.
The usual on dit about stratification is that it has no semantics. This is the kind of thing people go around saying. And, as Luca points out, it simply isn’t true. There is this theorem of mine (building on work of Petry and Henson) that says that the stratifiable formulae are precisely those that are invariant under Rieger-Bernays permutations. I’m pretty sure that Dana Scott knew this result ages ago but didn’t feel the need to write it out. Henson must have known it too. I wrote it up and published it because it seemed to me that it mattered and that it should be brought out into the open. And that the on dit needed to be knocked on the head.
Here is another way of making the same point. There is the di Giorgi picture of (structures for the language of) set theory. A structure for the language of set theory is a set equipped with an injection into its power set (after all, a structure for the language of set theory is a set with an extensional relation on it, and an extensional relation on X is an injection from X into its power set [see my Logic, Induction and Sets, esp. §8.1]). We can think of this picture as each member of the set “coding” a subset of the set. Now Cantor’s theorem tells us that no such injection can be surjective. So some subsets must be left uncoded. So, in constructing a structure for the language of set theory, one has two steps to take. (i) One decides which sets are to be left out, and then (ii) one decides which surviving sets are to be coded by which elements. Natural question Q: which sentences have their truth-values already determined by stage (i)? That is, what sentences have the feature that their truth-values are determined purely by our decision about which subsets are going to be coded, and are not affected by our decision about which subsets are coded by which elements? Some examples are obvious. The structure believes the empty set axiom iff the empty set is in the range of the injection. The structure believes that every set has a singleton iff, whenever s is a subset that is coded, then the singleton of the element coding s is also a coded subset (never mind what the coding is). Answer to Q (of course): the stratified sentences!
But there is a larger question here. The Petry-Henson-Forster theorem relates one particular kind of invariance to one particular syntactic feature (namely stratification). In this case, it’s invariance under change of implementation. But there are other kinds of implementation-insensitivity, and typing systems that accompany them. There are people who understand the axiom scheme of replacement (not very many, it has to be said) and how it is all about implementation insensitivity. Here is an example: Does it make any difference to the abstract theory of ordinals you get whether you use von Neumann ordinals or Scott’s trick ordinals? It shouldn’t! But if you want to prove that it doesn’t then you need replacement.
Tomorrow, I hope, back to me on Luca’s chapter on NF.