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 On Friday, October 1, 2021 at 7:35:05 AM UTC-4 Anarcocap-socdem wrote: > 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. > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/32fc021b-69ca-4aa7-ba72-aba0154ad79fn%40googlegroups.com.
