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
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
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
