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 On Friday, October 1, 2021 at 11:05:08 AM UTC-4 Anarcocap-socdem wrote: > 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/5ec0d06c-0315-4e04-9852-b3d3137b7af9n%40googlegroups.com.
