According to
https://math.stackexchange.com/questions/1123312/theory-of-definitions,
(referencing the same book as the question you mentioned) these properties are
required by all definitions, and there are also some criteria listed and
explained for a certain type of definition. Maybe this is a
Thanks. I got it. I'm rusty with LaTex and forgot about redefinition
commands. It was late when I looked so I gave up when I got errors.
It is what I thought it was. I have proved line 8 of 4.2 in a different
way from other results. I wrote it as...
⊢ eq( φ ,φ ) where I define eq( phi ,
"I couldn't convert them to something I could actually read like latex or
unicode"
The proof format is meant to allow readability by both machines (easy and
flexible when able to code) and humans (in a text editor without word wrapping).
Apart from some missing spaces, these formulas are in
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.
Sorry I didn't have time to read the proof you shared. I couldn't read it
easily and wasn't sure if it completely answered what I really wanted since
I want to show that definitions satisfy the precise meaning of
eliminability and non-creativity. Maybe the proofs help but I couldn't
convert
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
