Alternative Proofs

[Antony Bartlett]

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

[David A. Wheeler]

> On Aug 28, 2022, at 7:19 AM, Antony Bartlett <a...@akb.me.uk> wrote:
>
> 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).

This is really interesting!! Thanks for doing this!

...

> 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

Interesting results. I took a look at a few of these.

Sadly, the few cases I reviewed seem to be intentional:
* ax1 is a proof of axiom ax-1 starting from the *Lukasiewicz* axioms, showing
that our chosen axiom system is at least as powerful as the *Lukasiewicz* axioms
(in the sense of being able to prove at least as much).
There's a naming convention here: We generally know that names-with-hyphens
can be duplicated by same-name-drop-last-hypen, e.g., ax-1 <-> ax1.
Also, note that ax1 is marked
"(Proof modification is discouraged.)" and "(New usage is discouraged.)", suggesting
that this is a pretty special thing.
* idALT is an alternative proof of id. You can tell because its name adds "ALT" to another name.
* frege27 is specifically *commented* as being the same as id :
"Identical to ~ id". It's also marked as "(Proof modification is discouraged.)" - suggesting
that something weird/special is going on.
* con4 notes in its comments that it's an "Alias for ~ ax-3 to be used instead of it for labeling consistency."
So its comment specifically notes the duplicate. You could argue that this duplication
isn't helpful (why not just consistently use the name of the axiom directly?), but
it certainly isn't hidden.

I suggest adding a few heuristics to omit the *intentional* duplicates, so we
can see just the *unintentional* duplicates. I suggest these heuristics:
1. Omit names with ALT or OLD that appear to duplicate one without the marking;
we already know they're alternatives.
2. Omit names with comments that refer to the other duplicate proof, e.g., "~ id" in frege27.
Obviously we *knew* about the duplications in those cases, since they're expressly noted
in the comments.
3. Omit names that only different because of a hyphen (ax-1, ax1).
4. MAYBE: Omit names with comments "(Proof modification is discouraged.)" or
"(New usage is discouraged.)"; these are already highly specialized.
This specific heuristic might omit too much, so I suggest experimenting.
Maybe just omit those that say "(Proof modification is discouraged.)", since that
says we don't want to replace the proof during minimization?
Or maybe the other heuristics are good enough.

I suspect the tool will still find things with some heuristics, but its
results will then be focused on unintentional duplications.

What do you think?

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

That would be interesting! But I think you'd have even more "false positives"
in the sense of looking for unintentional duplicates, so I think it'd be even more
important to filter out some cases.

I think there's a kernel of a good idea here, but it needs some refining/tweaking
to keep the output from being overwhelming.

--- David A. Wheeler

[Antony Bartlett]

On Sun, Aug 28, 2022 at 5:17 PM David A. Wheeler <dwhe...@dwheeler.com> wrote:

> This is really interesting!! Thanks for doing this!

Thanks!  I'm thrilled you think so.

> I suspect the tool will still find things with some heuristics, but its results will then be focused on unintentional duplications.

Cool.  I was investigating where this is done intentionally, but it's good if it can also be used for spotting unintentional duplications.

I've done the filtering on labels that you asked for (in a single function called filterAssertion, so it can easily be removed or refined)

> 1. Omit names with ALT or OLD that appear to duplicate one without the marking; we already know they're alternatives. 

After reviewing common suffices I actually went with this list: ['ALT', 'ALT2', 'ALT3', 'OLD', 'ALTN', 'OLDN', 'VD']

> 3. Omit names that only differ because of a hyphen (ax-1, ax1).

And for what it's worth I'll send you (off-list) the 218 lines of output (down from 661) that we now get, but I think the filters by comment content that you propose will actually deliver the most value.  Being a (repurposable) validator, checkmm doesn't currently have the capability to associate the correct comment with an assertion.  I think I'd prefer to put this functionality in in the context of html generation (where it's easy to test), then circle back around to alt-mm results filtering.

    Best regards,

        Antony

What do you think?

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

That would be interesting! But I think you'd have even more "false positives"
in the sense of looking for unintentional duplicates, so I think it'd be even more
important to filter out some cases.

I think there's a kernel of a good idea here, but it needs some refining/tweaking
to keep the output from being overwhelming.

--- 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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/B7C2232E-23AF-4B0D-98D9-43481BCB60F8%40dwheeler.com.

[Benoit]

Hi Antony,

That's a nice work.  @savask did some similar things, see https://github.com/metamath/set.mm/issues/2128.  Apparently his search is not exhaustive, so maybe you can see together how your methods differ and how to improve on one another. As for the big list, it would be interesting to have it. In another issue (https://github.com/metamath/set.mm/issues/2710), @savask linked to a file he posted on gist.github.com. I don't know how easy it would be to do it for you.

Note: you wrote on the first line of your first post "proofs that are identical", but the proofs can differ: what you mean is that the statements are identical (more precisely, as you wrote later: the $f, $d, $e and $p statements of the associated frame).  And probably not up to variable renaming ?

Benoît

[Antony Bartlett]

On Tue, Aug 30, 2022 at 12:10 AM Benoit <benoit...@gmail.com> wrote:

> That's a nice work.

Thanks :-)

> As for the big list, it would be interesting to have it.

Please find the original unfiltered alt-mm output here https://github.com/Antony74/alt-mm/blob/1cef09bc1976bd673d10ae76bdc872ff476b2fa1/set-mm-output.txt

And with the label filtering suggested by David here https://github.com/Antony74/alt-mm/blob/master/set-mm-output.txt

I don't know why I didn't think of committing the output to the git repository before.  If I make further improvements I should be able to keep that output file in sync.

Note: you wrote on the first line of your first post "proofs that are identical", but the proofs can differ: what you mean is that the statements are identical (more precisely, as you wrote later: the $f, $d, $e and $p statements of the associated frame).  

I think it's the bit where I said axioms, definitions, and proofs were assertions, that I went wrong.  A proof does contain an assertion but it contains more than just that.  We're only concerned here with the assertion part.  The concept of an assertion is just something I've picked up from the checkmm source code, sorry if it's not proper terminology.

> And probably not up to variable renaming ?

No.  Savask has got further with this question than me by considering which sets of variables can be used interchangeably.  Sounds like a challenging problem to resolve programmatically (though easily guessed when looking at an .mm file).  After solving that I would probably just re-assign variables alphabetically in order of appearance - imposing a consistent ordering makes a test for equality trivial -  except I think that falls apart here because the hypotheses in which variables may appear are themselves unordered.

    Best regards,

        Antony

[Alexander van der Vekens]

I had a look at Anthony's filtered list (218 entries), and I removed the theorems with the following name patterns (because they are definitive in mathboxes): wl-*, bj-*, rp-*, bnj*, *RP, frege* , axfrege* . Then 103 entries remain. In general, theorems of mathboxes should not be considered.

There are, however, duplicates in the mathboxes (mainly from GS):

* fdmfifsupp, fidmfisupp (fidmfisupp in GS's mathbox, can be removed)

* le2addd, leadd12dd (leadd12dd in GS's mathbox, can be removed)
* fz0ssnn0, fzssnn0 (fzssnn0 in GS's mathbox, can be removed)

* tendopl2, tendospdi2 (both in NM's mathbox, tendospdi2 could be removed)

* mapss2, mapssbi (both in GS's mathbox, mapss2 could be removed)
* fnfvimad, fnfvima2 (both in GS's mathbox, fnfvima2 could be removed)
* climd, clim2d (both in GS's mathbox, clim2d could be removed)
* volicorecl, volicore (both in GS's mathbox, volicore could be removed)

Attached my reduced list, containing some comments (including the above listed comments).

@Glauco: Maybe you can have a look at this list and find additional duplicates. Could you remove these, please?

[Glauco]

Thanks, Alexander

now I'm working on tooling, but as soon as I get back to set.mm with new proofs, I will certainly look into this list.

BR

Glauco

[Antony Bartlett]

Alexander writes:

> I had a look at Anthony's filtered list (218 entries), and I removed the theorems with the following name patterns (because they are definitive in mathboxes): wl-*, bj-*, rp-*, bnj*, *RP, frege* , axfrege* . Then 103 entries remain. In general, theorems of mathboxes should not be considered.

Yes, I'm afraid the deficiencies in my list aren't likely to be remedied at least until I settle on an mm parser to adopt.  Also the rationale I gave for this tool wasn't as a duplicate checker, pleasing though it is that some utility is being found in this regard.

However, for what it's worth, I ran alt-mm again last night, the differences in output since the first time I ran it can be found here

https://github.com/Antony74/alt-mm/commit/fabcf71e272b131574a3dc95c4d247e22bf1176b

    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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/c6751e4e-98de-4d88-a479-8494716c16a6n%40googlegroups.com.