> 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 > <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 > <http://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 <https://github.com/metamath/set.mm/pull/2221> --- David A. Wheeler -- 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/94313917-86AB-4D8D-816D-3A5F38C9289A%40dwheeler.com.
