I've written a short program (https://github.com/Antony74/alt-mm) that
lists out assertions (axioms, definitions, and proofs) that are identical
(and therefore interchangeable).
It uses the checkmm validator to parse the .mm file. Kind of wish I'd
asked here first because it's slightly more involved than I'd anticipated
to check if two assertions are the same. It's not just the expressions
that have to match, it's any hypothesis expressions (unordered), and any
disjoint variable conditions (unordered). What I realised but haven't
explored is that an assertion lacking a particular hypothesis or disjoint
variable condition is presumably still compatible, but only in one
direction.
When I run it on set.mm I get 661 lines of output. I'll reproduce the
first 20 here. It's impossible to know if I've got this completely
correct, but the output is very plausible, grouping similarly named labels
suffixed with ALT or OLD.
Each line contains the labels representing a group of repeated assertions,
ordered by the first appearance
a1ii, dummylink
ax-mp, nic-stdmp, re1axmp, e0a
ax-1, minimp-ax1, luklem5, ax1, tbw-ax2, retbwax2, re1tbw2, tb-ax2, wl-ax1,
ax-frege1
ax-2, minimp-ax2, ax2, re1ax2, wl-ax2, ax-frege2
ax-3, con4, ax3, wl-ax3, ax3h
mp2, e00
a1i, wl-a1i, wl-impchain-a1-1
imim2i, wl-imim2i
id, idALT, id1, wl-id, frege27
idd, frege26
a1d, wl-a1d, wl-impchain-a1-2
com12, wl-com12
syl5, wl-syl5
pm2.27, wl-pm2.27
a1dd, wl-impchain-a1-3
pm2.43, minimp-pm2.43, merlem11, luklem6, merco1lem9
imim2, luklem8, bj-imim2ALT, wl-imim2, frege5
imim1i, wl-imim1i
imim1, luk-1, nic-luk1, tbw-ax1, re1luk1, retbwax1, re1tbw1, re2luk1,
tb-ax1, ax-luk1, frege9
pm2.04, luklem7, tbwlem1, re1ax2lem, wl-pm2.04, axfrege8, ax-frege8
I'm particularly interested in where our axioms have been proved because
this shows there's nothing unique about them. While the Tarski-based
Metamath axiom system is no doubt an excellent choice, this is how and
where we show that other perfectly adequate axiomisations also exist. It's
tempting to try to write a program ('reaxiom') that takes one .mm file and
outputs another with axioms you specify removed and proofs you specify
converted to axioms. Lots of DAG (directed acyclic graph) construction and
walking, same as the 'shuffle' algorithm I previously proposed which could
also be a feature of such a program. I think I'm going to stay focused on
my prettier plug in and html generation for the time being, however.
Hope this is not completely uninteresting.
Best regards,
Antony
--
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/CAJ48g%2BA1SxAF2-imoe7Ktm9vxKxuoy8NwicAZ16cj59oX-D5tQ%40mail.gmail.com.
