Which comment of Benoît you are referring to? Anyway, he has brought this up before; see bj-ax9, which derives ax-9 from df-cleq (with the help of additional axioms ax-1 through ax-7, ax-12, and ax-ext), and bj-df-cleq, which is proposed as a replacement for df-cleq. See also my comment at https://github.com/metamath/set.mm/pull/965#issuecomment-506578377 . Basically, once we are in set theory, we no longer care about the details of the underlying classical FOL with equality.
set.mm already goes much further than almost all textbooks, which state df-cleq without an explicit ax-ext hypothesis like we do (although they may mention it in passing). I myself have wondered if that was going too far in set.mm. I don't think I have ever seen in any book a concern about which FOL axioms are needed to justify a set theory definition; indeed, many set theory textbooks don't even show an FOL axiomatization but assume the reader will use their favorite. It would be fine to add to the df-cleq comment an explanation of these things, with links to bj-ax9 and bj-df-cleq, but I am not in favor of changing the existing df-cleq itself. Norm On Tuesday, October 26, 2021 at 10:05:22 AM UTC-4 ookami wrote: > I think Benoit Jubin is right when stating, that df-cleq need not only > ax-ext as its prerequisite, but also ax-9. > > This issue recently surfaced when KP noticed in a commit comment, that a > dependency on ax-9 was unexpectedly removed from his proof, too. > > The reason why ax-ext is referred to in df-cleq is explained in its > comment. The same logic holds also for ax-9. Consequently, one should > adapt the definition df-cleq accordingly. Apart from dfcleq, no other > proof should be affected by this move. > > Are there objection to this extension? > > Wolf Lammen > -- 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/f7a32c28-61fe-4a48-9ca9-a3aa7249d605n%40googlegroups.com.
