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.
