Your answer made me read the comment of http://us.metamath.org/mpeuni/ax6v.html It is written there that the DV condition was introduced "out of the blue, with no apparent justification". I am not in Tarski's head, but here is a possible justification. In a logic with terms, the analog axiom scheme would be \exists x x = t , DV(x,t) where t is a term metavariable. In this case, the DV condition is necessary (the axiom scheme would be false without it --- for instance, take t={x} in a well-founded set theory). Therefore, returning to our logic without terms, the sufficiency of the axiom scheme \exists x x = y , DV(x,y) (ax6v) is noteworthy, even though the more general axiom scheme \exists x x = y (ax6) does hold. (The analog axiom schemes for a logic with terms were given in Kalish--Montague).
Benoit -- 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/79b19ceb-0b83-4cba-ad6c-ad51fc6b20ccn%40googlegroups.com.
