Thanks for the quick and thorough response.
How might I extend this example so it is impossible to prove `0 != 0`? I
don't know of anything other than distinct variables that would prevent
something like this.
On Thursday, December 29, 2022 at 7:21:12 PM UTC-5 [email protected] wrote:
> A variation on your example which should be rejected would be to use `x`
> twice, like so:
>
> $c true num != $.
>
> $v x y $.
>
> num_x $f num x $.
> num_y $f num y $.
>
> ${
> $d x y $.
> x_ne_y $a true x != y $.
> $}
>
> the1 $p true x != x $=
> num_x num_x x_ne_y $.
>
> On Thu, Dec 29, 2022 at 7:15 PM Mario Carneiro <[email protected]> wrote:
>
>> 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 a topic in the
>> Google Groups "Metamath" group.
>> To unsubscribe from this topic, visit
>> https://groups.google.com/d/topic/metamath/Ww0shheWk_U/unsubscribe.
>> To unsubscribe from this group and all its topics, 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
>>
>> <https://groups.google.com/d/msgid/metamath/80cb855b-cc66-4d67-9060-98913da6bd56n%40googlegroups.com?utm_medium=email&utm_source=footer>
>> .
>>
>
--
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/75cc3e29-1ff0-4769-8b6a-4ed2a332e3e9n%40googlegroups.com.
