Recall that $NFU$ is the Quine-Jensen system of set theory with a universal set; it is based on weakening the extensionality axiom of Quine's $NF$ so as to allow urelements.
Let $NFU^-$ be $NFU$ plus "every set is finite". As shown by Jensen (1969), $NFU^-$ is consistent relative to $PA$ (Peano arithmetic). $NFU^-$ provides a radically different "picture" of finite sets and numbers, since there is a universal set and therefore a last finite cardinal number in this theory.
The following summarizes our current knowedge of $NFU^-$.
1. [Solovay, unpublished]. $NFU^-$and $EFA$ (exponential function arithmetic) are equiconsistent. Moreover, this equiconsistency can be vertified in $SEFA$ (superexponential function arithmetic), but $EFA$ cannot verify that Con($EFA$) implies Con($NFU^-$). It can verify the other half of the equiconsistency.
2. [Joint result of Solovay and myself]. $PA$ is bi-interpretable (and therefore equiconistent equiconsistent with ) the strengthening of $NFU^-$ obtained by adding the statement that expresses "every Cantorian set is strongly Cantorian". Again, this equiconsistency can be verified in $SEFA$, but not in $EFA$.
3. [My result]. There is a "natural" extension of $NFU^-$ that is equiconistent with second order arithmetic $\sf Z_2$.
For more detail and references, you can consult the following paper:
A. Enayat. From Bounded Arithmetic to Second Order Arithmetic via Automorphisms, in Logic in Tehran, Lecture Notes in Logic, vol. 26, Association for Symbolic Logic, 2006.
A preprint can be found here.
