On Wed, Jul 12, 2023 at 4:35 AM Marshall Stoner <mbstone...@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/CAFXXJSskrbo9yw0hEy2ALCMCoTeX1uv4uCtYetkkOpG9K0VXYA%40mail.gmail.com.
