## An inconsistent variation on NF

### Sergei Tupailo

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.

Tarmo Uustalu

Last update 30.5.2006