I think it is fairly weak evidence of the associative law, since you still can't write a /\ b /\ c /\ d - in fact you now need substantially more associativity laws to handle all the ways you can make groupings of two and three things. I understand the desire to reduce parentheses, but I think the appropriate solution to that is simply to use a proper parser and/or pretty printer.
Regarding the magnitude of the change, I think in principle it can be completely automated. You parse all statements, replace `w3a a b c` with `wa (wa a b) c`, then re-print and insert the new parenthesis characters in statements; also perform this replacement in syntax construction in theorems. That will eliminate the w3a without removing any theorems, but then you can do a minimize run to eliminate use of w3a theorems that are now copies of a wa theorem after statement rewriting, and then remove all the unused theorems. Those that remain may need to be renamed to accommodate the new shape. Alternatively, it can be done manually over a long period: we start by declaring w3a as discouraged for use, and then gradually remove it from proofs without touching any of the w3a theorems or the definition. Once all the downstream theorems are fixed, it is possible to remove or rename the w3a theorems, and remove the definition. On Sat, Jul 23, 2022 at 2:04 AM 'Alexander van der Vekens' via Metamath < [email protected]> wrote: > On Saturday, July 23, 2022 at 12:56:00 AM UTC+2 [email protected] wrote: > >> The triple conjunction and disjunction in particular lead to a big >> combinatorial blowup in the number of conjunction manipulation theorems we >> have to handle. I didn't implement these at all in MM0 (it's much simpler >> to write automation without them), and I would support removing them from >> set.mm. >> > > I am often torn between loving these triple conjunctions and disjunctions, > because they save some brackets, and hating them, because they don't fit > for the current situation and I have to convert them. Although I could go > with Mario's proposal in principle, to remove the triple conjunction and > disjunction from set.mm would be a very big deal, because a lot of proofs > would be affected. > > I think Norm's motivation to introduce them was mainly because they are > also defined in [WhiteheadRussell], but also because > > *This abbreviation reduces the number of parentheses and emphasizes that > the order of bracketing is not important by virtue of the associative law > ~ anass * > > see comment for ~df-3an. With the first argument I fully agree (see > above), but limitedly with the second argument: Sometimes the order is > important or at least meaningful, e.g., `( A e. V /\ B e. W /\ A =/= B )` > is more natural than `( A e. V /\ A =/= B /\ B e. W )`, and `( ( A e. V /\ > B e. W ) /\ A =/= B )` would be even more natural in my opinion. > > -- > 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/78b1a20a-d7b1-49b4-ada1-e95db611b460n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/78b1a20a-d7b1-49b4-ada1-e95db611b460n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSuVwOEhxOcCiriqsatRzRdPWzmnkPYqJ8vByKQuxcJbeQ%40mail.gmail.com.
