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 <[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/CAB0L6P0PK%2BdyFRP3yRXeXoJkoByTq-x0tRGZzUM7%2BNe88kCZ8Q%40mail.gmail.com.
