Regarding the new axioms:
ax-abidc should be derivable from df-cleq (it should not be expressible
prior to this anyway, since A = B as a wff is not introduced until then).
Specifically:
|- ( x = y -> ( y e.c A <-> x e.c A ) )
|- ( y e.c A <-> [ y / x ] x e.c A )
|- ( y e.c A <-> y e.c { x | x e.c A } )
|- A. y ( y e.c A <-> y e.c { x | x e.c A } )
|- A = { x | x e.c A }
We need ax-8c as an axiom to prove the first line, but abidc should be
derivable.
The second axiom, ( x e.c y <-> x e.s y ), is actually a definition: If we
indicate the coercion explicitly as ( x e.c cv y <-> x e.s y ), then it
should be clear that we can write it in definition form as
|- cv y = { x | x e.s y }
(which looks a lot like abidc but only because of the suggestive notation).
On Mon, Nov 1, 2021 at 11:34 AM Thierry Arnoux <[email protected]>
wrote:
> I was curious about the solution where we do not overload equality `=`
> and membership `e.`, but instead have different versions of those
> predicates for sets.
>
> For those interested, I've published the resulting experiment here:
> https://github.com/tirix/set-noov.mm
>
> One can examine the changes done on set.mm using GitHub's diff tool.
> I've also put a description of my changes in the README.
>
> In order to make that work, I had to introduce two new axioms. I wonder
> if anyone can eliminate any of them, or propose a cleverer approach.
>
> In any case, this approach involves duplicating many of the predicate
> calculus theorems, proving them once in their set-only version, and then
> again in their class version, so overall this method is not elegant and
> I agree it shall not be pursued.
>
> BR,
> _
> Thierry
>
>
> On 29/10/2021 07:19, Norman Megill wrote:
> > On 10/28/21 10:11 AM, Thierry Arnoux wrote:
> >
> > > A solution is mentioned in the comment for df-cleq, shall it be
> > > reconsidered?
> > ...
> >
> > A discussion about eliminating overloading of = and e. in
> > df-clab,cleq,clel, and why it isn't that simple, is here (from 2016):
> >
> > https://groups.google.com/g/metamath/c/IwlpCJVPSLY/m/f8H9lze_BQAJ
> >
> > I believe Mario correctly concludes (contrary to my initial
> > suggestion) that overloading of "e." can't be removed with this
> > method. Since the 3 definitions work together, it doesn't make sense
> > to half-fix it with the clumsiness and longer proofs that will result
> > from =_2 (always having to convert back and forth to make use of FOL
> > theorems).
> >
> > I have removed the comment you mention from df-cleq since it is
> > misleading in this way.
>
>
>
>
> --
> 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/f387c42a-ac19-3979-851b-d5b6fb8e2638%40gmx.net
> .
>
--
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/CAFXXJStBSE9M6s46eATnFoQgi%3Di0bOj3nC9k%2BdaBMdauQLrO2g%40mail.gmail.com.
