I wonder whether one can derive df-cleq and df-clel from more class
centered axioms in a separate section. In the manner complex numbers are
implemented using dedicated definitions like Kuratowski style pairs. And
then introduce the results as axioms, abstracting from the details of
On Saturday, November 27, 2021 at 11:21:49 AM UTC-5 Benoit wrote:
> Here is a complement to Mario's, Thierry's, and Wolf's proposals, as Wolf
> is beginning to formalize his in his mathbox.
>
> If you do not want to overload the membership predicate, then the most
> sensible thing to do in my
Here is a complement to Mario's, Thierry's, and Wolf's proposals, as Wolf
is beginning to formalize his in his mathbox.
If you do not want to overload the membership predicate, then the most
sensible thing to do in my opinion is to simply remove ax-8 and ax-9. By
bj-ax8 and bj-ax9-2, they are
