Is there a proof for "2+2=4" without passing through the reals?

[Anarcocap-socdem]

As discussed in the Proof Explorer page, the Metamath proof that "2+2=4" has 26,323 steps. 

The reason for such a long proof is Metamath first defines the real and the complex numbers. There are good reasons to do so.

However, I would like to check the proof that "2+2=4" using basic ZFC, which would probably result in a shorter proof.

I see there is another proof (the one of Principia Mathematica), but I think (but I am not 100% sure) that this proof is not the simple one I am looking for.

Has a simple proof for "2+2=4" been written in metamath?

Thank you in advance.

[Norman Megill]

In our construction of the complex numbers, even the "simple" natural numbers are complicated objects, and there isn't a simple direct ZFC proof of 2+2=4 that doesn't require going through the construction, leading to the large number of steps you see.

However, there is http://us.metamath.org/mpeuni/o2p2e4.html which is 2+2=4 for the ordinal natural numbers (finite integers starting at 0).  It uses the von Neumann ordinals, where 0 is the empty set, 1 is {0,{0}}, 2 is {1,{1}}, etc. I think that is about as close to the ZFC axioms as you can get.  'show trace_back o2p2e4/count/essential' still shows about 14K steps (many of which are just propositional and predicate calculus and could probably be made much shorter if the only goal were to prove o2p2e4).  In addition, the set.mm proof involves transfinite recursion to get the addition operation for finite and infinite ordinals at once, and it would be somewhat shorter if we limited ourselves to finite recursion.

There is a real number construction (not in set.mm) that uses the finite ordinals as the official natural numbers, then adds a disjoint set extending the collection to the integers, then adds rationals, and finally adds reals, each stage adding new elements to the existing stages.  It is described in Levy, Azriel, Basic Set Theory, Dover Publications, Mineola, N.Y. (2002), p. 217.  I assume it can be further extended to complex numbers (which Levy doesn't do).  That would get you a complex number construction where each stage would be about as close to ZFC axioms as possible for that stage.  In principle this could be a drop-in replacement for the complex number construction section in set.mm.  I think it is elegant in its own way, although I don't know how the size of the full construction would compare the existing one in set.mm.

Norm

[Anarcocap-socdem]

Thank you, Norman.

El dia divendres, 1 d’octubre de 2021 a les 16:36:43 UTC+2, Norman Megill va escriure:

[Norman Megill]

 By the way, if you want to see which ZFC axioms are needed for o2p2e4, you can use (in metamath.exe)

MM> read set.mm

...
MM> show trace_back o2p2e4 /essential/axioms/match ax-*
Statement "o2p2e4" assumes the following axioms ($a statements):
ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12
ax-13 ax-ext ax-rep ax-sep ax-nul ax-pow ax-pr ax-un

To see the path a specific axiom takes towards proving o2p2e4, an example is

MM> show trace_back o2p2e4 /to ax-pow
The proof of statement "o2p2e4" traces back to "ax-pow" via:
ax-pow($a) zfpow el dtru brprcneu fvprc ndmfv fvmpti fvmpt2i fvmpt2 mpteqb
eqfnfv eqfnfvd tfrlem1 tfrlem5 tfrlem7 tfrlem9 tfrlem9a tfrlem10 tfrlem11
tfrlem12 tfrlem13 tfrlem14 tfrlem15 tfrlem16 tfr1a tfr2a tfr1 rdgfun rdgdmlim
rdgfnon rdgvalg rdg0 rdgseg rdgsucg rdgsuc rdg0g frsuc oa0 oasuc onasuc
oa1suc

(This is a fortuitously short example. Tracing back ax-ext for example will show almost all set theory theorems up to o2p2e4 since ax-ext is involved in the definition and properties of class notation.)

Norm

[David A. Wheeler]

El dia divendres, 1 d’octubre de 2021 a les 16:36:43 UTC+2, Norman Megill va escriure:

In our construction of the complex numbers, even the "simple" natural numbers are complicated objects, and there isn't a simple direct ZFC proof of 2+2=4 that doesn't require going through the construction, leading to the large number of steps you see.

However, there is http://us.metamath.org/mpeuni/o2p2e4.html which is 2+2=4 for the ordinal natural numbers (finite integers starting at 0).  It uses the von Neumann ordinals, where 0 is the empty set, 1 is {0,{0}}, 2 is {1,{1}}, etc. I think that is about as close to the ZFC axioms as you can get.  'show trace_back o2p2e4/count/essential' still shows about 14K steps (many of which are just propositional and predicate calculus and could probably be made much shorter if the only goal were to prove o2p2e4).  In addition, the set.mm proof involves transfinite recursion to get the addition operation for finite and infinite ordinals at once, and it would be somewhat shorter if we limited ourselves to finite recursion.

I think others would be interested in some of this, so I created a pull request to extend some

of the proof comments so they’ll link to each other. I also extended the comment in df-suc to briefly

explain our (typical) approach for ordinal numbers:

https://github.com/metamath/set.mm/pull/2221

--- David A. Wheeler