Symbol for ordinal number 0

[Alexander van der Vekens]

I want to suggest to provide a special symbol ` 0o `for the ordinal number 0, which actually is the empty set `(/) `, see ~0elon and df-1o. It would be just a synonym for ` (/) `:

` df-0o $a |- 0o = (/) $. `

With such a symbol, the theorems in the context of ordinal numbers can be written in a more intuitive way. For example

` map0e $p |- ( A e. V -> ( A ^m (/) ) = 1o )`

could be written as

map0e $p |- ( A e. V -> ( A ^m 0o ) = 1o )

Was this already proposed/discussed before? What do others think about it?

[Jim Kingdon]

I'm a bit skeptical.

I remember Norm wrote a message to the mailing list (which I'm not sure how to find) about why we use e. and C_ for ordinal less than and ordinal no greater than, rather than having, say, <o and <_o (I think he even said we tried the latter for a while). I don't know if there was a similar discussion of 0o and (/).

If applying definitions in metamath were more automatic, maybe I would feel differently (or maybe I wouldn't, I'm not sure), but as it is, there would be a number of extra theorems (0o e. _V, 0o e. _om, 0o e. 1o, etc) and steps converting between 0o and (/).

--
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/c6bc77ee-56cd-458c-a176-3f616e0c862an%40googlegroups.com.

[savask]

>I remember Norm wrote a message to the mailing list (which I'm not sure how to find) about why we use e. and C_ for ordinal less than and ordinal no greater than, rather than having, say, <o and <_o (I think he even said we tried the latter for a while).

I think you mean the following post of Norm about philosophy and goals of set.mm: https://groups.google.com/g/metamath/c/mnkBQV1_cXc/m/zz4C8_2KAAAJ The paragraph "rules for introducing new definitions" is especially relevant.

[Jim Kingdon]

Thank you. I'm pretty sure that was the message I was thinking of. It sounds like the separate symbols for ordinal less than and less than or equal were very early (well before anything which is in git, which starts with something Norm called set.mm.1998-03-16-from-vax).

On 7/21/22 23:24, savask wrote:

>I remember Norm wrote a message to the mailing list (which I'm not sure how to find) about why we use e. and C_ for ordinal less than and ordinal no greater than, rather than having, say, <o and <_o (I think he even said we tried the latter for a while).

I think you mean the following post of Norm about philosophy and goals of set.mm: https://groups.google.com/g/metamath/c/mnkBQV1_cXc/m/zz4C8_2KAAAJ The paragraph "rules for introducing new definitions" is especially relevant.

--
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/13af2ad6-951d-4d34-918a-9ab46d4fb01an%40googlegroups.com.

[Alexander van der Vekens]

Thank you for the hint to Norm's "rules of thumbs":

Definitions are at the heart of achieving simplicity.  While developing 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?

[Benoit]

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

[Mario Carneiro]

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.

--

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/6513d1ff-47d9-4665-89e3-ccf0377b694cn%40googlegroups.com.

[Alexander van der Vekens]

On Saturday, July 23, 2022 at 12:56:00 AM UTC+2 di....@gmail.com 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.

[Mario Carneiro]

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.

--
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/78b1a20a-d7b1-49b4-ada1-e95db611b460n%40googlegroups.com.

[Alexander van der Vekens]

As far as I interpret the comments until now, there is the tendeny towards not defining 0o, and generally avoid new definitions. This corresponds to our convention "New definitions infrequent.`" (although there can always be exceptions if they are reasonable and broadly accepted).

Just for the record: I also thought about a definition of "not defined" as ` df-ndef $a |- N/D = (/) $. ` to distinguish between the meaning of `(/) ` as " not defined" and "defined result". ~fvprc, for example, could become ` $p |- ( -. A e. _V -> ( F ` A ) = N/D ) $= `. Alternatively, N/D could be defined as predicate for classes: `df-ndef $a |- ( N/D A <-> A = (/) ) $. ( ~fvprc could become ` $p |- ( -. A e. _V -> N/D ( F ` A ) ) $= .