On Friday, March 27, 2020 at 11:25:25 AM UTC-7, Marnix Klooster wrote:
>
> Hello all,
>
> Occasionally I see people here spending effort on making Metamath proofs
> as short as possible. And every time I wonder, Why?
>
>
>From one point of view, "I just want to know what the theorems say" the
shortness of the proof means little. But for the business of collecting a
large number of proofs, having shorter proofs is a boon to those that have
to store them, read them and understand them. Indeed, most proofs in the
database can be expanded to thousands of steps by eliminating their
dependence on proofs that came before, so emphasis on shortening proofs is
practical even from the non-mathematical viewpoint of a curator.
Shortening a proof means either a) one has eliminated wasteful steps by
taking a more direct route, avoiding deriving the same statement twice, or
using a step like "bicomi" (commuting a logical equivalence) more often
than required or b) it means you proved the same statement with more
powerful tools. And powerful tools are good things.
Since Metamath builds up from the axioms, it starts a long way from the
concepts that even children using math deal with on a daily basis ("2p2e4"
is an example, since this concept of addition is powerful enough to work on
negative, rational and complex numbers while the underlying set theory
pieces don't speak immediately to such concepts).
A recent example would be "intss" (If A is a subclass of B, then the
intersection of class B is a subclass of the intersection of class A) which
was shortened from a 10-step technical argument about the elements of A and
B to a 5-step proof which points out that the subset relation of A and B
gives rise to an implication of restricted quantifications, which gives
rise to a subclass relation between classes of element which meet those
restricted quantifications. When those classes are equated with the
definition of the intersection of a class, we are done.
The shorter proof is easier to translate. It's more symmetric in that it
treats A and B identically. It's philosophically more concise in that it
doesn't rely on the existence of a universal class of all sets.
References:
http://us.metamath.org/mpeuni/bicomi.html (logical equivalence commutes)
http://us.metamath.org/mpeuni/2p2e4.html ( 2 + 2 = 4 )
http://us2.metamath.org:88/mpeuni/intssOLD.html (short lived link to proof
from 1999)
http://us2.metamath.org:88/mpeuni/intss.html (short lived link to proof
from 2020)
--
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/bb9250a2-60fc-45e2-bc37-1520bd6d60a7%40googlegroups.com.
