The justification of definitions requires imposing additional structure on metamath databases in the form of being able to unambiguously parse statements into trees. Without it, you can't use the definition checker at all, and the rules do not make sense / could be circumvented without more rules.
On Wed, Jul 12, 2023 at 8:53 AM Marshall Stoner <mbstone...@gmail.com> wrote: > I wasn't talking about set.mm or mmj2. I was talking in metamath in > general, which doesn't seem to enforce non-ambiguity since it only reads > strings of tokens with no other underlying structure. I was in learning > the definition checker rules in terms of learning in detail how definitions > are theoretically justified. I didn't know there was a parsing step in > mmj2 separate from metamath itself, so I assumed it was part of the > definition checker (since theorem grammar is taken care of by 'w' axioms > during proof verification). > > > > On Wednesday, July 12, 2023 at 12:02:45 AM UTC-4 di....@gmail.com wrote: > >> On Wed, Jul 12, 2023 at 4:35 AM Marshall Stoner <mbsto...@gmail.com> >> wrote: >> >>> I trust that intuitively that these definitions are valid. The problem >>> is an alias rule can still fail if the syntax of the definition doesn't >>> meet certain criteria. If the parenthesis surrounding ↔ were missing in >>> the definition of the biconditional, for instance. If I could understand >>> how the definition checker for the set.mm database works I would have a >>> better understanding. I have my own hypothesis, but I'm not sure if it's >>> fully sufficient. >> >> >> That example fails for a very simple reason: it wouldn't parse. Step 0 of >> the definition checker is to parse the definition as a wff, and if you omit >> the parentheses then the parser would fail on this axiom. This would >> actually cause mmj2 to fail if you wrote a non-parsing statement anywhere, >> not just in a definition but in any $e, $a, or $p statement. >> >> If you changed the definition of the syntax "ph ↔ ps" itself to not have >> parentheses, and removed it from the definition as well, then it would >> parse, but mmj2 would still fail for a different parsing reason: the >> resulting grammar is ambiguous and the parser constructs some tables that >> witness unambiguity of the grammar, meaning that this parser construction >> will fail if the grammar is ambiguous. >> >> In both cases it isn't really the definition checker catching the error. >> The definition checker presupposes that the database has an unambiguous >> grammar and all statements parse by that grammar. >> > -- > 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+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/1c92e482-fcee-4659-a858-076edb89d6e5n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/1c92e482-fcee-4659-a858-076edb89d6e5n%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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSsEfcGJDJGf-mBByE%3DcND5mwd%3Dq8R%3DHygaf9S6g%2BwT9iw%40mail.gmail.com.
