Thanks to everyone who worked on this issue. As described in that github
issue, we now have a (better) working definition checker as part of the
Travis build.
The definition checker means that unsound definitions are a matter of
"well, we might or might have an elegant design but we at least have a
way of catching mistakes or people who don't understand the system well
enough" as opposed to "OMG we need to rearchitect the whole thing
because how can we trust the hundreds of definitions in set.mm?".
On 9/24/19 11:54 AM, David A. Wheeler wrote:
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/a0108bbd-b35e-71ec-223a-6b9e0c591be7%40panix.com.
