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.
On Fri, Jul 22, 2022 at 6:50 PM Benoit <[email protected]> wrote: > This definition would be redundant, and there are probably borderline > cases were the empty set could as well be considered as the zero ordinal or > the empty set. And after that, should we have another symbol for the only > function from the empty set to a given set ? Etc. > > With each new definition comes a number of new associated basic lemmas, so > this increases the search space when scrolling the website or searching a > result, when writing a proof, minimizing a proof... (both for a human and a > computer). > Also, we shouldn't add definitions with the sole purpose of having an > aesthetically pleasing display. There are actually already a number of > definitions which are not clearly justified (although I'm not proposing to > remove them now, only not to add new ones of that kind): > * triple conjunction and disjunction df-3an and df-3or, > * negated equality and negated membership (this is a borderline case), > * alternative denial df-nan, since ` -/\ ` is the same as ` -> -. ` (also > intuitionistically), > * I recently ran across df-lindf and df-linds, of which only one should > remain, probably that of independent set (this would imply a few changes > for theorems using the definition of independent family), > * indeed, I had already thought about df-1o, which could be removed (note > that "one" is encoded the same way in the Von Neumann and Zermelo > encodings, is not too long to type, and is objectively the second simplest > set after the empty set; it diverges beginning at 2). > > Benoît > On Friday, July 22, 2022 at 9:06:57 AM UTC+2 Alexander van der Vekens > wrote: > >> Thank you for the hint to Norm's "rules of thumbs": >> >> >> *Definitions are at the heart of achieving simplicity. While developing >> set.mm <http://set.mm>, two rules of thumb that evolved in my own work were >> (1) there shouldn't be two definitions that mean almost the same thing and >> (2) definitions shouldn't be introduced unless there is an actual need in >> the work at hand. Maybe I should add (3), don't formally define something >> that doesn't help proofs and can be stated simply in English in a theorem's >> comment. * >> >> So my suggestion would break rule (1) and maybe also rule (3)*. *But are >> the "problems" (reasons for the rules) mentioned by Norm also problems for >> 0o? Are really a lot of conversions needed as long as we are in the >> context of ordinal numbers? What is bad about a theorem ` 0o e. 1o ` which >> is identical with ` 0lt1o $p |- (/) e. 1o $= `? Would not even the >> definition of 1o break these rules, because 1o is identical with `{ (/) >> }`(see ~ df1o2), which is also often used outside the context of ordinal >> numbers? >> > -- > 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/6513d1ff-47d9-4665-89e3-ccf0377b694cn%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/6513d1ff-47d9-4665-89e3-ccf0377b694cn%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/CAFXXJSu8hjbM-z9-paSwRMabMYprLPZX6mNkC437aAh%3Dw7iyew%40mail.gmail.com.
