Thank you, Norman. 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. > > 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4bc682ad-41e8-4c24-9e51-516fa4efe408n%40googlegroups.com.
