The definition df-bust-verifier is not per se "crazy", it becomes so in the presence of ax-5. Should you ever strive for a set.mm without distinct variable constraints, usage of df-bust-verifier is at your discretion. Distinct variable constraints are in FOL (without sets) a convenience extension, because requiring two variables be distinct can be achieved by a distinctor hypothesis -. A. x x x = y, and x be distinct from ph is replaceable with a F/ x ph hypothesis (I leave out the boring special case of a one-object universe).
This gives rise to the question, how the definitionChecker works: Does it assume the current axiomatic foundation in place, or does it really do a semantic check of axioms it finds in the file and individually derives requirements for soundness? In other words: If I remove ax-5 from set.mm and discard theorems based on it, is df-bust-verifier accepted then? I am curious, and don't have the time to look at the sources. I am not too disappointed, if I receive no answer. Wolf -- 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/6040ba57-6b94-4b49-9cdc-2f11f2b8b11f%40googlegroups.com.
