The metamath C implementation is correct in this case, that is a correct theorem. A $d constraint on two variables asserts that the substitutions to those variables have no *variables* in common. A constant expression like "0" has no variables in it, so it is disjoint with itself.
The use of != here is misleading, because a $d on two variables is not asserting that the variables have distinct values, but rather distinct *names*. So for example we need something like that to know that y is free in "A. x x e. y", because if x and y had the same name then the theorem would be asserting "A. x x e. x" which has no free variables in it. One consequence of this is that for sorts which have binding syntax in them, like the "setvar x" used in "A. x ph", it is disastrous to allow constants in, in the sense of $a setvar 0 $., because then you could form the expression "A. 0 x = 0" which in addition to being nonsensical can be used to prove false by circumventing the $d check on a theorem that requires it - e.g. dtru says "-. A. x x = y" but if you substitute 0 for both x and y you get "-. A. 0 0 = 0", and you can similarly substitute 0 for x in a proof of "A. x x = x" to get "A. 0 0 = 0" and hence a contradiction. On Thursday, December 29, 2022 at 7:03:37 PM UTC-5 [email protected] wrote: > I'm working on a verifier for Metamath proofs, and I've reached the point > of implementing disjoint requirements. I tried to make a minimal example of > invalid use of disjoint variables, but the primary C metamath > implementation seems to accept it. I'm likely doing something wrong, but I > can't figure out what. > > AFAIU, this file should not verify, but it does: > > ``` > $c true num 0 1 != $. > $v x y $. > > num_x $f num x $. > num_y $f num y $. > > num_0 $a num 0 $. > num_1 $a num 1 $. > > num_zero $a num 0 $. > num_one $a num 1 $. > > ${ > $d x y $. > x_ne_y $a true x != y $. > $} > > the1 $p true 0 != 0 $= > num_zero num_zero x_ne_y $. > ``` > -- 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/80cb855b-cc66-4d67-9060-98913da6bd56n%40googlegroups.com.
