Download Metamath book

3.8. EXPLORING THE SET THEORY DATABASE
89
that are used along the way. Note that Metamath makes no distinction
between axioms and definitions. In set.mm they have been distinguished
artificially by prefixing their labels with ax- and df- respectively. For example, df-an defines conjunction (logical and), which is represented by the
symbol /\. Section 4.5 discusses the philosophy of definitions, and the Metamath language takes a particularly simple, conservative approach by using
the $a statement for both axioms and definitions.
You can also have the program compute how many steps a proof has if
we were to follow it all the way back to $a statements.
MM> show trace_back prth /essential/count_steps
The statement’s actual proof has 5 steps. Backtracking, a
total of 55 different subtheorems are used. The statement
and subtheorems have a total of 196 actual steps. If
subtheorems used only once were eliminated, there would be a
total of 25 subtheorems, and the statement and subtheorems
would have a total of 143 steps. The maximum path length is
20. A longest path is: prth <- imp4b <- imp4a <- impexp <imbi1i <- impbi <- bi3 <- expi <- expt <- pm3.2im <- con2d <con2 <- nega <- pm2.18 <- pm2.43i <- pm2.43 <- pm2.27 <com12 <- syl <- a1i <- a1i.1 .
This tells us that we would have to inspect 196 steps if we want to verify
the proof completely starting from the axioms. A few more statistics are also
shown. There are one or more paths back to axioms that are the longest;
this command ferrets out one of them and shows it to you. There may be a
sense in which the longest path length is related to how “deep” theorem is.
Finally, we might be curious about what proofs depend the theorem
prth. If it is never used later on, we could eliminate it as redundant if it
has no intrinsic interest by itself.
MM> show usage prth
Statement "prth" is directly referenced in the proofs of 4
statements:
anim12d mo 2mo ssxp tfrlem5 climunii climadd
Thus prth is used by 7 proofs, and indirectly by many more that make
use of those proofs, and so on. (The /recursive qualifier gives you all of
them.)
3.8.1
A Note on “Compact” Proof Format
The present version of Metamath (0.07.30) will display proofs in a “compact”
format whenever the proof is stored in compressed format in the database.
It may be be slightly confusing unless you know how to interpret it. (A
future version may eliminate this format from displays.) For example, if
you display the complete proof of theorem id1 it will start off as follows: