> > This gives rise to the question, how the definitionChecker works: Does it > assume the current axiomatic foundation in place, or does it really do a > semantic check of axioms it finds in the file and individually derives > requirements for soundness? In other words: If I remove ax-5 from set.mm > and discard theorems based on it, is df-bust-verifier accepted then? >
The definition checker does not assume an axiomatic foundation: it reads the provided mm database (which has to be similar to set.mm, in terms of typecodes (e.g. "|-" and "setvar") but it also works e.g. on iset.mm). It checks Rules 1--5 I gave in the post above because we can prove, outside of Metamath, that a definition respecting these rules is conservative and eliminable (a similar metatheorem is proved for instance in Kleene's Introduction to metamathematics). In particular, if ax-5 is removed, df-bust-verifier will still be rejected, because it violates Rule 5, regardless of previous axioms (as long as no justification theorem for it is provable, but in that case the axiomatization would not be consistent). It is instructive to look at how $a-statements violate the various rules. To do this, remove the statements excluded from the check in the RunParms.txt file. Here is an example of an mmj2 output (most ax-* are rejected because of Rule 1): ------------ I-UT-0015 **** Processing RunParmFile Command #4 = SetMMDefinitionsCheckWithExclusions,ax-* I-PA-0201 Axiom df-bi has failed the definitional soundness check. The root symbol is not = or <->. I-PA-0202 Axiom df-clab has failed the definitional soundness check. The previous axiom ax-c14 uses the symbol being defined in this axiom. I-PA-0202 Axiom df-cleq has failed the definitional soundness check. The previous axiom ax-8d uses the symbol being defined in this axiom. I-PA-0202 Axiom df-clel has failed the definitional soundness check. The previous axiom df-clab uses the symbol being defined in this axiom. I-PA-0206 Axiom df-bust-verifier has failed the definitional soundness check. Dummy variables [y] are possibly free in the definiendum, and no justification is available. ----------- [By the way: the failure to pass the test for df-clab, df-cleq, df-clel should not be due to the obsolete axioms mentioned, but this is another matter.] Benoit -- 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/3fbb9305-3632-4ff8-9347-ce32a2486dd9%40googlegroups.com.
