On the Stanford Encyclopedia of Philosophy article on alternative axiomatic set theories, it is stated without reference that bare $\mathsf{NFU}$ (i.e., $\mathsf{NFU}$ without the axiom of infinity) is weaker in consistency strength than $\mathsf{PA}$. In this Math SE answer, Randall Holmes states that $\mathsf{NFU}$ interprets Robinson arithmetic and furthermore says that it probably interprets bounded arithmetic with exponentiation (which I think means $\mathsf{I}\Delta_0 + \mathrm{exp}$, although I'm not completely familiar with the semi-formal terminology people use for these things).

This would put $\mathsf{NFU}$ right in the range of theories for which ordinal analysis should be well-behaved (i.e., those which are at least as strong as $\mathsf{I}\Delta_0$) but also should be feasible to actually do (e.g., those which are as strong as or not too much stronger than $\mathsf{PA}$). So this raises a question that I have been unable to find any discussion of.

Question 1. What is the proof-theoretic ordinal of bare $\mathsf{NFU}$?

More generally, a lot is known about consistency strength and interpretation of theories of first- and second-order arithmetic between $\mathsf{I}\Delta_0$ and $\mathsf{PA}$. Proof-theoretic ordinals are supposed to be a rough measure of consistency strength, but in principle this is a more fine grained issue.

Question 2. Where does bare $\mathsf{NFU}$ sit relative to well-known theories of arithmetic in terms of interpretation and consistency strength?

  • $\begingroup$ If one, perhaps accidentally, is interested in the strength of NFUM ---- it has been worked out by Zachiri McKenzie and myself in terms of the hierarchy of baby measurable cardinals (preprint widely available). The results for NFUA and NFUB by Ali Enayat and Robert -Solovay are by now classics. The answer for NFU is old and known. The connection with strong cuts in models of arithmetic is not yet explored. $\endgroup$ May 14, 2021 at 1:21

1 Answer 1


As in the question, I will use $\mathsf{NFU}$ for "bare" $\mathsf{NFU}$, i.e., the result of weakening the extensionality axiom in Quine's $\mathsf{NF}$ so as to allow urelements. Let $\mathsf{NFU}^{-\infty}$ be $\mathsf{NFU} \cup \{\lnot \mathsf{Infinity} \}$, where $\mathsf{Infinity}$ is the axiom of infinity.

In 2002, Solovay proved the following results. The proofs were disseminated among some NFU enthusiasts, but alas, they remain unpublished. In what follows $\mathsf{Exp}$ is the statement asserting the totality of the exponential function, and $\mathsf{SupExp}$ is the statement asserting the totality of the superexponential function (also known as tetration), i.e., the "stack of twos" function, $f(n)$, where $f(0) = 1$ and $f(n+1) = 2^{f(n)}$.

Theorem. (1) $\mathrm{I}\Delta_{0} + \mathsf{SupExp} \vdash\mathsf{Con}(\mathsf{NFU}^{-\infty}) \leftrightarrow\mathsf{Con}(\mathrm{I}\Delta_{0} + \mathsf{Exp})$.

(2) $\mathrm{I}\Delta_{0} + \mathsf{Exp} \vdash \mathsf{Con} (\mathsf{NFU}^{-\infty})\rightarrow \mathsf{Con}(\mathrm{I}\Delta_{0} + \mathsf{Exp})$.

(3) $\mathrm{I}\Delta_{0} + \mathsf{Exp} \nvdash \mathsf{Con} (\mathrm{I}\Delta_{0} + \mathsf{Exp})\rightarrow\mathsf{Con} (\mathsf{NFU}^{-\infty})$.

Suspected Answer to Question 1. Based on the above theorem (part 1), the proof theoretic ordinal of $\mathsf{NFU}^{-\infty}$ is likely to be the same as the proof theoretic ordinal of $\mathrm{I}\Delta_{0} + \mathsf{Exp}$, i.e., is $\omega^3$, if one were to follow the procedure given by Taranovsky to this question.

Answer to Question 2 Solovay's proof of the above theorem makes it clear that $\mathsf{NFU}^{-\infty}$ interprets $\mathrm{I}\Delta_{0} + \mathsf{Exp}$, but not vice versa; thus the interpretability relation between $\mathsf{NFU}^{-\infty}$ and $\mathrm{I}\Delta_{0} + \mathsf{Exp}$ is similar to the interpretability relation between $\mathsf{ACA}_0$ and $\mathsf{PA}$.

  • $\begingroup$ Are there published proofs of (1)-(2) with a stronger system in place of the weak "base theory" $\mathsf{I\Delta_0+(Sup)Exp}$? And are Solovay's arguments available somewhere, even if unpublished? $\endgroup$ Apr 1, 2021 at 23:06
  • $\begingroup$ Thank you. Is $\mathsf{NFU}^{-\infty}$ known to be conservative over $\mathrm{I}\Delta_{0} + \mathsf{Exp}$ (if we think of the finite strongly Cantorian cardinals as the naturals)? $\endgroup$ Apr 1, 2021 at 23:13
  • 1
    $\begingroup$ @NoahSchweberThe only published proof of the consistency of $\mathsf{NFU}^{- \infty}$ is the one that is implicit in Jensen's original paper on $\mathsf{NFU}$. Indeed, to my knowledge, the only published paper that explicitly talks about $\mathsf{NFU}^{- \infty}$ is the paper (available: fs2.american.edu/enayat/www/Enayat-Tehran-August%2024.pdf) which was published in Logic in Tehran, Lecture Notes in Logic, vol. 26, Association for Symbolic Logic, 2006. It shows the intimate relationship between Peano Arithmetic and a natural strengthening of $\mathsf{NFU}^{- \infty}$). $\endgroup$
    – Ali Enayat
    Apr 2, 2021 at 0:47
  • $\begingroup$ @NoahSchweber About Solovay's proofs: they were communicated directly to me via several long emails directly to me in 2002. $\endgroup$
    – Ali Enayat
    Apr 2, 2021 at 0:49
  • 2
    $\begingroup$ @JamesHanson $\mathsf{NFU}^{-\infty}$ is known to prove that the strongly cantorian cardinals satisfy $\mathrm{I}\Delta_0 + \mathsf{Exp}$ plus $\mathrm{B}\Sigma_1$ (the collection scheme for $\Sigma_1$ formula). Surprising, they also satisfy even more, namely, for a specific definable cut $\mathsf{I}(x)$ of strongly Cantorian numbers, $\mathsf{Con} ({\mathrm{I}\Delta_0 + \mathsf{Exp}})$ holds in $\mathsf{I}$, as shown by Solovay (alas, again unpublished). The precise theory that holds in the strongly Cantorian numbers (provably in $\mathsf{NFU}^{-\infty}$) has not been identified. $\endgroup$
    – Ali Enayat
    Apr 2, 2021 at 1:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.