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. > > On Thu, Jun 6, 2019 at 7:33 PM 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/6e0f83a8-df65-4a1d-ae2d-01f7a74a1ff6%40googlegroups.com.
