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 recoverable from FOL= and df-clab, df-cleq,
df-clel (stated without hypotheses, so you also remove ax-ext). This is
not very satisfying since df-cleq appears to group two axioms (the two
directions). You could split it into two, to get the system:
$d x A $. $d x B $. [in all these axioms]
df-clab $a |- ( x e. { y | ph } <-> [ x / y ] ph ) $.
df-clel $a |- ( A e. B <-> E. x ( x = A /\ x e. B ) ) $.
ax-classext $a |- ( A. x ( x e. A <-> x e. B ) -> A = B ) $.
ax-9clbi $a |- ( A = B -> ( x e. A <-> x e. B ) ) $.
It would be better to state ax-9clbi without a biconditional, as
ax-9cl $a |- ( A = B -> ( x e. A -> x e. B ) ) $.
but then, you cannot prove anymore that = is an equivalence relation among
classes. So you have to strengthen ax-7 to
ax-7cl $p |- ( A = B -> ( A = C -> B = C ) ) $.
Finally, df-clel also appears to group two axioms, and it appears clearer
to split it into:
ax-8clbi $a |- ( x = A -> ( x e. B <-> A e. B ) ) $.
ax-elisset $a |- ( A e. B -> E. x x = A ) $. [this is the current
~bj-elissetv]
Note that ax-8clbi needs a biconditional in its consequent. You can remove
it if you put a class variable in place of x, that is,
ax-8cl $a |- ( A = B -> ( A e. C -> B e. C ) ) $.
Of course, you always have the syntactic axiom ~cv in all of these
systems. So to sum up, you can use the system
{ax-mp, ax-gen, ax-1--6, ax-7cl, ax-8cl, ax-9cl, ax-classext, ax-elisset,
df-clab}
where ax-8cl is replaceable by ax-8clbi, and ax-9cl could be strengthened
by replacing in it x with a class variable, although this is recoverable.
It has the advantage of having simpler axioms, each one stating a single
fact instead of grouping several facts. In particular, it states as an
axiom the fundamental bj-elissetv. It has the disadvantage of not singling
out FOL= (since ax-7 was replaced by ax-7cl) nor ax-ext in its textbook
form. They could be restored by adding the corresponding $e hypotheses to
these axioms (the $e hypotheses would have exactly the same form as the $a
conclusions, with class metavariables replaced by variable metavariables).
Benoît
On Tuesday, November 2, 2021 at 4:18:35 AM UTC+1 Thierry Arnoux wrote:
> Thank you very much, Mario and Benoît, I will update the repository.
>
>
> On 02/11/2021 00:01, Mario Carneiro wrote:
>
> Correction: the first line of the abidc proof should be
>
> |- ( x =s y -> ( y e.c A <-> x e.c A ) )
>
> with a set equality on the left (since class equality is not yet
> introduced yet). We also want ax-8c to reference only primitive term
> constructors, so it should also use =s .
>
> On Mon, Nov 1, 2021 at 11:55 AM Mario Carneiro <[email protected]> wrote:
>
>> 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/CAFXXJSutSTcXhDB_ucpWitfy3ej7TpMO8MHS%2B-0a7FVzy36TcQ%40mail.gmail.com
>
> <https://groups.google.com/d/msgid/metamath/CAFXXJSutSTcXhDB_ucpWitfy3ej7TpMO8MHS%2B-0a7FVzy36TcQ%40mail.gmail.com?utm_medium=email&utm_source=footer>
> .
>
>
--
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/04b1ad87-1b9b-4222-a598-245f1211bc9an%40googlegroups.com.
