On the [Stanford Encyclopedia of Philosophy article on alternative axiomatic set theories](https://plato.stanford.edu/entries/settheory-alternative/), 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](https://math.stackexchange.com/questions/899024/how-much-maths-can-we-do-in-nfu/3508736#3508736), 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?
> 
> 
> 



What is the proof-theoretic ordinal of bare $\mathsf{NFU}$?
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](https://en.wikipedia.org/wiki/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](https://math.stackexchange.com/questions/2334724/small-proof-theoretic-ordinals) 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}$.


