...without using the Axiom of Infinity? I've become interested recently in the fragment of ZF without the axioms of regularity/foundation and infinity, since it seems that much of math can be developed without these or the axiom of choice. Looking at the Metamath proof that 2 + 2 = 4 (2p2e4), I saw that it requires the axiom of infinity. Now on the surface this makes sense, because the axiom shows that the natural numbers (in some sense) are a set, and without that there's no reason a priori to think that you have numbers like 2 and 4. Indeed, the proofs that 2 is real or complex (2re and 2cn) rely on the axiom of infinity. Additionally, the proof that addition is associative (addass), clearly needed or at least useful in this proof, requires the same. This is derived from the requirement on the closure of addition (addclsr). But the existence of 2 = S1 = SS0 would appear to follow from the axioms of pairing and null set. Indeed, it seems that the natural numbers should exist in this fragment of ZF, though the collection need not be a set. Is it known that the axiom of infinity is needed? Also, as an aside, is there a good name for this fragment of ZF? I seem to remember reading a name for it, though it may be colloquial.