On Fri, Jun 14, 2019 at 10:15 AM 'Alexander van der Vekens' via Metamath < [email protected]> wrote:
> Concerning the circular definitions: are there any meaningful cases, or > even already examples in set.mm? > There are no circular definitions in set.mm. I was not clear, but the mmj2 definition checker uses the order of constants (not the definition) to determine which definitions are allowed to reference which others. So in the circular reference example, bar would be allowed to refer to foo but foo would be rejected as a forward reference (even though the constant bar is declared before the definition foo, the constant foo is declared before constant bar). On Fri, Jun 14, 2019 at 10:16 AM Benoit <[email protected]> wrote: > I would welcome such a convention. Some syntax statements are not > associated with definitions (e.g. wi, wn, cv, wal) and I see that you took > this into account in your proposal. What would the precise convention be? > Is it: > > Every statement with label df-xxx is an $a-statement with typecode |- > and is immediately preceded by an $a-statement with typecode wff and label > wxxx or with typecode class and label cxxx. > I would like to get away from label conventions in favor of something machine readable and not hardcoded. The mechanism I propose is: If an $a statement is given for a syntax typecode (i.e. not |-), then it is a definition iff the immediately following statement is a definitional axiom $a |- foo = ... which satisfies the usual rules. Otherwise, it is treated as an axiom, and a warning is issued if the label convention implies that the axiom would like to be treated as a definition and there is no warning-suppressing pragma attached to the axiom. We can add $j commands to define the df-* convention for issuing warnings, and suppressing warnings on the definitions that aren't actually definitions but are called df-* anyway. Some label changes I see (skimming through mmdefinitions.html) are: > wb --> wbi (and similarly for wo wa, w3o, w3a, wxo), even though df-bi > is a special case > df-v --> df-vv (to match cvv and avoid collision with cv) > The general rule has been to make constant names as short as possible while still disambiguated, because they are not visible to the user. (I'm starting to regret this choice in the recently completed lean translation because these names are literally all that I see.) In particular, making wceq and wcel longer will have a significant effect on total size of set.mm because they are by far the most common theorems applied. (Maybe we should use a Huffman encoding to choose label lengths?) On Fri, Jun 14, 2019 at 1:22 PM Norman Megill <[email protected]> wrote: > My first question is, how will it be checked? Can the mmj2 definition > check be modified to ensure it? > The definition checker is actually overdue for a rewrite. I've added a lot of $j's recently, and they should all be validated. I actually put a syntax error in a $j in one of my commits and it didn't get caught, which is bad. We need a complete reference of $j statements, which can update along with set.mm itself as new statements are created. Also the existing definition checker has hardcoded names all over the place, which has already caused problems on one occasion; adding a $j parser would fix this issue. For now, let's just say it's unchecked but I will put this on my todo list. On Fri, Jun 14, 2019 at 1:30 PM Norman Megill <[email protected]> wrote: > The four definitions df-bi, df-clab, df-cleq, and df-clel are excluded > from the current definition check. Any new software will have to treat > these 4 as special cases, for example by treating them as additional > axioms. Hopefully these 4 are the only ones that will ever need special > treatment. > I would like to renew my suggestion that we change these to ax-bi, ax-clab, ax-cleq, ax-clel. It adds complexity to the tooling to have an inconsistent naming convention, since we are signaling that these are definitions when they don't meet the criteria, and it's also a lie to the reader because these look like definitions and claim to be definitions and the user may even know that we check definitions for soundness, yet these definitions each have extremely subtle problems that make them invalid as definitions. If the goal is to be open and straightforward, I think it is a more honest approach to call them axioms and explain in detail why they are conservative. (In fact, df-cleq is not even conservative!) On Fri, Jun 14, 2019 at 5:45 PM 'ookami' via Metamath < [email protected]> wrote: > By using a tag (or other kind of reference) the positioning of entries > remains unrestricted, open for any future development. I interpreted > Mario's foo/bar example in a way that he himself was in doubt whether > forcing constant and definition into consequtive entries might cause harm > in the future. > set.mm has never allowed for circular or mutual recursive definitions. Even if some specialized development required them, they would certainly be introduced as axioms, so there would be no pairing and it would be irrelevant. Ideally, a definition wouldn't be two statements at all, and deriving important semantic data based on positional information is messy, but metamath is what it is and I want a way to minimize data loss when interpreting the database without breaking backward compatibility or adding too much boilerplate. Mario -- 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/CAFXXJSvumkJpsCC06%2B2DYdM6j_s-f%2Bf2XUZEjyKPZ%2BZmDsya1A%40mail.gmail.com.
