I agree that the FOL= part should remain well-separated from the rest. And
if one wants to keep proximity with textbooks, then ax-8, ax-9, ax-ext
should remain untouched as well (actually ax-ext should be the universal
closure of what it currently is). This would give:
ax-mp, ax-gen, ax-1--13, cv, wceq, wcel: unchanged
${
$d x y z A $. $d x y z B $. $d x y z C $.
ax-7cl.v $e |- ( x = y -> ( x = z -> y = z ) ) $.
ax-7cl $a |- ( A = B -> ( A = C -> B = C ) ) $.
$}
${
$d x y z A $. $d x y z B $. $d x y z C $.
ax-8cl.v $e |- ( x = y -> ( x e. z -> y e. z ) ) $.
ax-8cl $a |- ( A = B -> ( A e. C -> B e. C ) ) $.
$}
${
$d u v w x A $. $d u v w x B $.
ax-9cl.v $e |- ( u = v -> ( w e. u -> w e. v ) ) $.
ax-9cl $a |- ( A = B -> ( x e. A -> x e. B ) ) $.
$}
${
$d u v w x A $. $d u v w x B $.
ax-classext.v $e |- ( A. u ( u e. v <-> u e. w ) -> v = w ) $.
ax-classext $a |- ( A. x ( x e. A <-> x e. B ) -> A = B ) $.
$}
${
$d x A $. $d x B $.
ax-elisset $a |- ( A e. B -> E. x x = A ) $.
$}
df-clab $a |- ( x e. { y | ph } <-> [ x / y ] ph ) $.
ax-ext: unchanged
...
Note the maximal unbundlings.
One more thing: in order to prove that equality of classes is an
equivalence relation, one needs Euclideanness (ax-7cl), and one also needs
reflexivity, proved for instance using ax-classext (hence ax-ext). That's
not necessarily a problem, but it would be nice to be able to prove that
equality of classes is an equivalence relation without these less basic
axioms. (Note that in addition to Euclideanness, left-seriality (ax6ev) is
enough to prove that the relation is an equivalence relation, so one could
be tempted to use ax-elisset, but sethood hypotheses would stay, like ( A
e. V -> A = A ) for reflexivity, and similar sethood hypotheses for
symmetry and transitivity.) Therefore, it may be better to replace ax-7cl
with a single axiom (single in order to keep independence) asserting
directly the wanted result that equality of classes is an equivalence
relation. This could be the less elegant
${
$d x y z t A $. $d x y z t B $. $d x y z t C $. $d x y z t D $.
ax-cleq.v $e |- ( ( x = y -> ( x = z -> y = z ) ) /\ t = t ) $.
ax-cleq $a |- ( ( A = B -> ( A = C -> B = C ) ) /\ D = D ) $.
$}
Another more thing: it may be more correct to use the universal closures of
the $e hypotheses above (as I did in the current bj-df-clel and
bj-df-cleq). This does not change much, since one can go back and forth
between them by ax-gen/sp, but sentences (closed formulas) are easier to
understand than open formulas (and the problem of having specific instances
as hypotheses creeps up in the conservativity theorem, it seems).
That is not necessarily a proposal to change the axiomatic, and certainly
not in a hurried way. At least it's here for future reference. I looked a
bit at these questions a few years ago, and even with the current
axiomatization, one can remove many usages of ax-ext, df-cleq, df-clel (see
the subsection titled "Classes without extensionality" in my mathbox).
Benoît
On Monday, November 29, 2021 at 4:52:16 AM UTC+1 Norman Megill wrote:
> I would be happy to see this idea explored in a mathbox. Even if we don't
> import it and change our "official" FOL= axiom system on the MPE home page
> (which is the result of a lot of fine tuning over many years and admittedly
> somewhat biased by my personal preferences), it can still exist as an
> important stand-alone study that can be referenced in the main set.mm and
> the MPE home page. We do keep some permanent important things in mathboxes,
> such as the old FOL= axiomatization in my mathbox that is referenced in
> many places.
>
> On Saturday, November 27, 2021 at 4:20:21 PM UTC-5 ookami wrote:
>
>> 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
>> construction.
>>
>> Wolf
>>
>> Norman Megill schrieb am Samstag, 27. November 2021 um 20:36:18 UTC+1:
>>
>>> 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 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.
>>>>
>>>
>>> I am traveling and haven't had time to study this carefully, but here
>>> are some general comments.
>>>
>>> I would prefer not to mess with FOL=. ax-8 and ax-9 are part of
>>> Tarski's FOL= system, and removing ax-8 and ax-9 would make it incomplete
>>> as a stand-alone system. Mixing up FOL= and class theory with some new
>>> axioms seems inelegant and confusing, probably more so to beginners.
>>>
>>> There is nothing mathematically wrong with adding new definitions that
>>> depend on previously introduced axioms for their justification; books do
>>> this all the time. We have mostly avoided this in set.mm, with the
>>> exceptions df-cleq and df-clel that need to justified "outside" of Metamath
>>> and whose justification needs some earlier axioms (ax-ext and some mild
>>> FOL=).
>>>
>>> Adding new axioms for class theory sends the message that FOL= + ZFC is
>>> not sufficient for mathematics, when in fact all uses of df-cleq and
>>> df-clel can be eliminated by converting the notation back to the the native
>>> ZFC language (or more accurately to our scheme language, since class
>>> variables map to wff variables). It's just not a "direct" substitution of
>>> definiens for definiendum like the other definitions in set.mm. No new
>>> mathematics results from df-cleq and df-clel; they just provide a
>>> convenient notational device that makes set theory much more practical to
>>> work with.
>>>
>>>
>>>> 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).
>>>>
>>>
>>> I am more open to this, as long as it will put this to rest once and for
>>> all. Do we know that other substitutions into A and B of df-cleq and
>>> df-clel can't generate FOL= statements that are stronger than these
>>> hypotheses?
>>>
>>> Norm
>>>
>>>
>>>
>>>>
>>>> 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 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 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/e2504c5d-b095-4a04-913e-e34dafa1f749n%40googlegroups.com.
