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 On Thursday, June 6, 2019 at 10:33:41 PM UTC-4, Edward McCants wrote: > > 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? > -- 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/5674b447-3540-4cec-855d-9ccb17cf30ca%40googlegroups.com.
