The distinctness of dummy variables

[Edward McCants]

Greetings, Metamath-ers,

As a hobbyist of set theory, logic, and the programing language Julia, I've been refactoring the Metamath Julia implementation to provide better interactive usefulness (in addition to using an old version of Julia, the previous incarnation could only load in .mm files and verify them).  This has been a learning experience about the nuances in the details of the Metamath specification (i.e. the pdf file that will be printed soon).

I've run into a roadblock where I can't find anywhere in the specification (section 4.1 of metamath.pdf) where dummy variables are to be treated as distinct; there's no mention of it in 4.1.4.  In the frames section (4.2.4, page 131), I see a definition of "optional disjoint-variable restriction", but I don't see anywhere that actually says to treat them as disjoint.  I also see the "Dummy variables <list> are mutually distinct and distinct from all other variables" comment on the webpages for the set.mm theorems.

Am I missing something?

[Mario Carneiro]

By the specification, dummy variables are not treated as distinct unless they appear in a $d statement. However, there are some verifiers that will always treat dummy variables as distinct. This is technically nonconforming, but a mm database that passes such a verifier can easily be modified to pass a conforming verifier by the addition of appropriate $d statements.

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/d4ce66a2-e2aa-4791-b10e-f39d0dff7f3e%40googlegroups.com.

[Sauer, Andrew Jacob]

I don't believe it is required by the specification, but it is conventional to make the dummy variables distinct. After all, since those variables are not in the theorem statement, making them distinct does not limit the theorem's applicability, and it can't hurt, in the sense that theorems can't become non-applicable because the theorem being proven has too many distinct variable statements, only if it has too few.

--

[Norman Megill]

In Sec. 4.1.4 under "Verifying Disjoint Variable Restrictions", it says: "Second, each possible pair of variables,
one from each expression, must exist in an active $d statement of the $p statement containing the proof."  The word "active" in "active $d statement" means either a "mandatory" or "optional" (dummy) $d statement.  We don't use the word "dummy" in the spec, but normally an optional $d is used for dummy variables in the proof.  (There can also be redundant optional $d's that don't reference a dummy variable in the proof, but they do no harm.)

To get a better feel for $d's, you may find it helpful to experiment with some $d statements in set.mm, i.e. commenting one out and seeing what the error message results when you do "verify proof" in metamath.exe.  The error messages for $d violations give a lot of detail about what's going on.

Norm

[Norman Megill]

It is required by the spec, in the place I mentioned in my previous post.  If you comment out a $d with a dummy variable, it will cause proof verification to fail in metamath.exe and most others.  Hmm is the only one I recall that assumes implicit $d's for dummy variables, but as Mario says it's non-conforming.

Norm

On Thursday, June 6, 2019 at 10:46:28 PM UTC-4, Sauer, Andrew Jacob wrote:

I don't believe it is required by the specification, but it is conventional to make the dummy variables distinct. After all, since those variables are not in the theorem statement, making them distinct does not limit the theorem's applicability, and it can't hurt, in the sense that theorems can't become non-applicable because the theorem being proven has too many distinct variable statements, only if it has too few.

[Edward McCants]

Ah, so the $d statement is required.  In the testcase that I was using, I failed to notice the $d statement above the block of lemmas that shared a ${ frame, and the updated code also failed to store the $d variable pairs where it was supposed to; so I have a different type of bug that I thought I did.