How much maths can we do in NF(U)?

Question

I have recently become interested in non-standard set theories, particularly in NF and NFU and have been reading some things here and there. Of course, I don't know much about it and I'm still trying to get my head around the very basics.

There is something I am very confused about and it's the issue of how much maths we can do within these theories. This is not a very precise question, but I think that's also not a very precise issue. I have been following some discussions in this site, but I haven't been able to find a clear answer. To be clear, I'm not interested in how (counter)intuitive or cumbersome NF(U) is, but in how it relates in terms of interpretability (and maybe in other terms) to other mathematical systems.

I know that both NF and NFU are supposed to be quite weak. NFU is weaker than PA and it has the same consistency strength as MacLane set theory (Z with bounded quantifiers). So, (some of) my questions are:

• How strong is MacLane set theory? Can we interpret some small (but "useful") system of arithmetic within it?

• Do Gödel incompleteness theorems apply to NF and/or to NFU? That is, can we interpret Robinson arithmetic within it? (Maybe this is very naïve. I suppose we can, but I'd like to have some confirmation of this fact.)

• And what about NFU + Inf + AC? In the SEP entry (on Alternative Axiomatic Set Theories) it is said that it is mathematically serviceable. But I don't really understand what that means.

Thanks a lot and sorry if my question is naïve, I'm a complete beginner in this field!

Answer 1

I know that both NF and NFU are supposed to be quite weak. NFU is weaker than PA and it has the same consistency strength as MacLane set theory (Z with bounded quantifiers).

MacLane set theory is significantly stronger than PA. It has the same consistency strength as Russellian unramified typed set theory (TST). In an answer to another question, I tried to explain in which sense this quite a strong impredicative theory.

How strong is MacLane set theory? Can we interpret some small (but "useful") system of arithmetic within it?

We can represent all of PA within it. We can also represent second-order arithmetic, and second-order arithmetic is sometimes called “analysis”. We can also represent impredicative n-th-order arithmetic (for finite n) within it.

Do Gödel incompleteness theorems apply to NF and/or to NFU? That is, can we interpret Robinson arithmetic within it?

Without Inf, we won't be able to interpret Robinson arithmetic. But with Inf (and that's probably what I would expect when I hear NFU), we get a sufficiently strong theory such that the Gödel incompleteness theorems apply.

And what about NFU + Inf + AC? In the SEP entry (on Alternative Axiomatic Set Theories) it is said that it is mathematically serviceable. But I don't really understand what that means.

You can use it instead of ZFC and it will just work most of the time. It's consistency strength is a bit weaker than ZFC, and the stratification can sometime be tedious, but on the other hand you have a "universe set" and "type level" tuples.

Answer 2

Most of the answers given above to this question were correct and to the point. One was not: NFU without infinity, or even with the negation of Infinity, does quite easily interpret Robinson arithmetic. The domain of strongly Cantorian natural numbers is a model of Robinson arithmetic (in fact, I believe, of bounded arithmetic with exponentiation).

Answer 3

To augment Randal Holmes’s answer, let me state for the record that Robinson’s arithmetic is interpretable already in the so-called adjunctive set theory, axiomatized by $$\exists z\:\forall t\:t\notin z,$$ $$\forall x\:\forall y\:\exists z\:\forall t\:(t\in z\leftrightarrow t\in x\lor t=y).$$ (That is, there exists $\varnothing$, and for any $x$ and $y$, there exists $x\cup\{y\}$; but note that extensionality is not included.) This result goes back to Szmielew and Tarski (Mutual interpretability of some essentially undecidable theories, in Proc. International Congress of Mathematicians, vol. 1, Cambridge, 1950). Thus, any set theory that proves these two weak axioms is subject to Gödel’s incompleteness theorems.

The adjunctive set theory is of course included in NFU without Infinity.