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.
On Thu, Jun 6, 2019 at 10:33 PM Edward McCants <[email protected]> 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/d4ce66a2-e2aa-4791-b10e-f39d0dff7f3e%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/d4ce66a2-e2aa-4791-b10e-f39d0dff7f3e%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/CAFXXJSu55RDviJYCf0kQN2qHmb1PEUMW7cL8Np48BeGuuG%2BGWA%40mail.gmail.com.
