Thursday, xx xxxxx 2006, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Abstract: In the last year several people have asked me the following question:
"Why not relax the definition of stratification in NF so that in occurrences of $x \in y$ it is demanded only that $\type(x)<\type(y)$ [not $\type(y)=\type(x)+1$, as it is in the official definition]?"
My answer to this question so far always has been:
"I have not seen anything of this kind, but don't think anything good would come out of this."
Now I think this extension can be shown to be inconsistent.
Let's call the new, relaxed, definition 'n-stratified', whilst the old (official) definition 'o-stratified'. NF+ is the theory consisting of Comprehension for n-stratified formulae plus Extensionality, whilst NF is the theory consisting of Comprehension for o-stratified formulae plus Extensionality. Obviously, NF is a subsystem of NF+.
The formula $\Tran(a)$, "$a$ is transitive", $\A x \in a \A y \in x y \in a$, is n-stratified, so, in NF+, by Comprehension there exists a set of all transitive sets. On the other hand, NF proves that the set of all transitive sets does not exist: see Forster's book, [T. E. Forster. Set Theory with a Universal Set, 2nd edition. Clarendon Press, Oxford, 1995], Proposition 2.1.16. Forster credits this proof to Boffa. Since NF is a subsystem of NF+, NF+ also proves the same fact, and thus turns out to be inconsistent.
P.S. If anyone (e.g. a student or so) is interested to do automated theorem-proving in NFU (that one is known to be consistent, so no need to be afraid here :-), please let me know. I have a colleague in the USA, who has an automated NFU theorem-prover, and who might be interested if there is anyone. But I cannot write to him before I know that there is anyone.