Issues about $d variables

[XiaoHLim]

Hi, David. I am developing an automated theorem prover on Metamath and this repo helps me a lot. However, I feel confused on the $d variables. Specifically, some theorems would not record its $d variables in MM.labels. The first theorem in set.mm that doesn't record the $d variables is exgen, whose assertion is:

(set(), [('wff', 'ph'), ('setvar', 'x')], [['|-', 'ph']], ['|-', 'E.', 'x', 'ph'])

and it's statement in set.mm is as below:

  ${
    $d x y $.
    exgen.1 $e |- ph $.
    $( Rule of existential generalization, ... $)
    exgen $p |- E. x ph $=
      ( vy weq idd speiv ) AABDBDEAFCG $.

    ...

  $}

The assertion is returned by make_assertion() in L264. This function only checks the variables in e_hyps and stmt and constructs $d, so it's an expected behavior to not have (x, y) as a $d pair (since y does not appear in either e_hyps or stmt). However, when I try to convert FullStmt to a theorem in set.mm and call the MM.read() method to verify, I pass in a string like this (all the necessary $c, $vs have been defined):

  ${
    $( No explicit declare: $d x y $. $) 
    exgen.1 $e |- ph $.
    exgen $p |- E. x ph $=
      ( vy weq idd speiv ) AABDBDEAFCG $.
  $}

and it raise a MMError: Disjoint variable violation: x , y.

I don't know how other languages' implementations of the metamath verifiers handle the above case, but I think the above theorem should pass the verification.

Here are my questions:

• For a theorem whose $d involves at least one variable that does not appear in its statement (e_hyps and stmt), does removing this $d restriction not change the semantics? (Personally, I think this is correct.)

• If the first thing is correct, should we introduce the concept of free $d and modify MM.verify() method? For theorems whose $d involves at least one variable that does not appear in its statement, even if the $d is not declared, the modified verifier would automatically derive and verify this restriction when proving the theorem. (I am honored to implement this feature and contribute to this repo!)

[tirix]

Hi Lin Xiaohan,

This is a valid question which has been raised in the past.
This discussion is probably relevant:

the Metamath spec requires that any disjoint variable conditions between dummies are required to be mentioned in the .mm file, although they are elided in the HTML proof display and they do not transfer to users of a theorem.

See also this note:

Sometimes new or "dummy" variables are used inside of a proof that do not appear in the theorem being proved. On the web pages we omit them from the "Distinct variable group(s)" list, which is intended to show only those distinct variable conditions that need to be satisfied by any proof that references the theorem.

Sometimes it is not strictly necessary for a dummy variable to be distinct from certain other variables, for example when those variables do not participate in the part of the proof using the dummy variable. In that case, it is optional whether or not we include those variables paired with the dummy variable in $d statements in the set.mm file. Sometimes you will see such optional $d statements omitted, depending on the preferences of the person who created the proof.

[XiaoHLim]

I see. Thank you for your timely reply!