FYI: @wlammen recently posted an example where an unsound definition causes problems: https://github.com/metamath/set.mm/pull/1089 Details below if you'd like.
This is expected per the Metamath book, because definitions are just axiomatic ($a) statements, and Metamath verifiers merely confirm that proven ($p) statements follow from $a statements. There are far fewer definitions than proven statements, and definitions are generally far simpler than proofs. That said, we don't *really* want unsound definitions. mmj2 already has a number of checks on definitions. Thanks to Mario, mmj2 version v2.5.3 now has a tweaked definition checker that does a deifnitional soundness check, which rejects this kind of nonsense. This version of mmj2 is now incorporated in our CI build, so every merged change into set.mm will be checked to prevent these kinds of crazy things. A related improvement: previously mmj2's checkers were configured to exclude df-sbc , because it reused a constant that has already been introduced, namely [ A / x ] ph. However, Norm changed it to use new constants in Jan 2017. df-sb is '[ y / x ] ph' and df-sbc is now '[. A / x ]. ph'. So df-sbc can be removed from the exception list, so that's one less thing that needs to be handled specially. For more about this, see: https://github.com/metamath/set.mm/pull/1089 --- David A. Wheeler P.S. Here's the definition that caused the problem. $( Declare a new symbol. $) $c BustVerifier $. $( A meaningless symbol $) $( Extend wff definition to include BustVerifier. $) wbustverifier $a wff BustVerifier $. ${ $d x y $. $( Try to bust the proof verifier using this definition. (Contributed by Wolf Lammen, 9-Sep-2019.) $) df-bust-verifier $a |- ( BustVerifier <-> x = y ) $. $} ${ $d x y $. $( A contradiction. (Contributed by Wolf Lammen, 9-Sep-2019.) $) bust-verifier $p |- ( -. x = y -> F/ x x = y ) $= ( weq wnf wn wbustverifier df-bust-verifier bicomi nfv nfxfr a1i ) ABCZAD LELFAFLABGHFAIJK $. $} -- 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/E1iCpxQ-0004A7-Ix%40rmmprod07.runbox.
