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.
