On Friday, October 29, 2021 at 6:05:19 PM UTC+2 Norman Megill wrote:
> Can you remind me what the minimal positive calculus is?
>
What I had in mind was {ax-mp, ax-1, ax-2, impbi, biimp, biimpr, simpl,
simpr, pm3.2}, or really anything that suffices to move the equivalences
through the other connectives. I realize one may also need ~alim and ~exim
since these quantifiers occur in dfcleq/clel. But actually, that part of
my proof sketch is too sketchy... I should ponder a bit more on this, but
it seems that the special form of bj-df-cleq/clel could permit to simplify
Levy's proof in the appendix of Basic Set Theory.
Benoît
--
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/063cda68-5e30-45a8-8397-b694093b2924n%40googlegroups.com.
