Is the Axiom of Infinity Necessary for Proving 2 + 2 = 4 in ZF Set Theory?

[CRGreathouse]

...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.

 

[CRGreathouse]

Megill writes (Appendix 5):

For example, we see that the Axiom of Choice ax-ac was not needed to prove 2 + 2 = 4 2p2e4, but we did need the Axiom of Infinity ax-inf2. Why did we need Infinity? Well, our number 2 is a real number, and the Axiom of Infinity is needed to prove that any real number exists. (And why is this? Very informally, we can think of an arbitrary real number as having an infinite list of digits after the decimal point, and we need an axiom that tells us that such infinite lists exist before we can manipulate them with set variables.) But the place where Infinity is used is buried deep inside the proof tree—you have to drill down through 33 layers of proof to find it.


So I this is related to the manipulation of real numbers in general. Are there ways of working with real numbers (or something similar) without the axiom of infinity, or with a weaker version?

 

[LukeD]

I would think that you couldn't get the real numbers or even the rational numbers (at least as usually constructed by equivalence classes) without the axiom of infinity. Though you should be able to get a model of the rational numbers that admits an infinite number of copies of each rational number by considering each pair (x,y) as being a (non-unique) rational number where x and y are integers.

Of course, this is moot if you can't get the natural numbers.

However, it seems that we can just define them as usual... I.e., 0 = {}, 1 = {0}, 2 = {0,1}, and so on.

Then we could define a natural number n recursively as being the set of the form {0,1,...,n-1}.

I don't see any need for the axiom of infinity here unless you want to be able to say that the collection of natural numbers is a set.

---

On to the definition of addition:

We could define addition in terms of a successor, (n+1 = n union {n})... I seem to remember being able to define addition of the natural numbers just with that, but I can't think of how to do it easily right now.

Anyway, I'd agree that you probably don't need the axiom of infinity to prove most of the things about finite sets of natural numbers.