Interestingly, it passed all the gitlab tests (metamath.c, rust, python, c++, java, and the additional checks of mmj2 --- thanks DAW for having put them in the continuous integration process). I then commented out this example in my mathbox. (To answer Norm's question: it does not lead to any inconsistency; I proved the system sound and the axioms are true in my semantics... I'll write up my notes and share them.)
I think it could be banned (trigger an error) by a verifier of set.mm-like databases (like mmj2), but not by a general-purpose verifier (like metamath.c). But actually, metamath.c also has a part for set-mm-like databases. So you option-based proposal sounds good. Indeed, for general databases, one can define any type of variables so there is no notion of "setvar variable". Maybe, in Mario's Metamath Zero, the restriction would be to have no DV conditions among non-pure sorts. (?) Benoit On Sunday, March 21, 2021 at 1:59:43 AM UTC+1 Norman Megill wrote: > 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/5ed3dcfc-cf62-4a37-9b08-2915312b06c7n%40googlegroups.com.
