I will probably add a check to metamath.exe in "verify markup" to issue a warning if a $d statement has multiple wff and/or class variables (along with a qualifier to skip that check if it isn't desired for some reason). We probably don't want to have "verify proof" (or the initial syntax check done by "read") flag these as errors, since a purpose of metamath.exe is to make sure the spec is met, and $d ph ps $. is allowed by the spec. AFAIK this doesn't lead to any inconsistency, but it could be confusing for a human to follow and maybe create difficulties translating to another proof language.
Tarski uses only the concepts of two variables being distinct and of a variable not occurring in a wff, and we follow that convention in set.mm. The spec allows any combination of variables to be part of a $d for simplicity. Its "disjoint variable" concept unifies Tarski's two concepts and I believe simplifies proof verification by not requiring special cases for different variable types. Benoit's example (PR https://github.com/metamath/set.mm/pull/1957) is intriguing. I don't think we want to add it to the official set.mm (and in the future it will trigger the "verify markup" warning I mentioned), but I would suggest it remain in set.mm in commented-out form for people who want to explore the idea further in their local databases. Norm -- 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/bfba7969-362a-4d3c-bcc2-ce9a2923843bn%40googlegroups.com.
