The recent commits to set.mm resolve the issue starting this thread (or are
at least a major step forward). I would like to thank all participants
here for their input. In the end that helped getting this done.
For the side considerations regarding df-cleq/df-clel: I had not time
enough to think the topic over. My first impulse after the discussion with
Mario was a rigorous bottom-up design starting from x e. A , avoiding
df-clab altogether, and axiomatize this term in a way that df-cleq /
df-clel become true definitions. Later one can introduce df-clab and note
that its interpretation of x e. A is a perfect match and hence a valid
option (but no requirement!). I am looking forward to have a look at the
other suggestions as well. Its too early for me to say I made up my mind.
Wolf
Benoit schrieb am Freitag, 29. Oktober 2021 um 18:24:01 UTC+2:
> 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/b393bab8-2bbd-43bd-97ff-f56c36b2719fn%40googlegroups.com.
