On Monday, November 29, 2021 at 6:11:32 PM UTC-5 Benoit wrote:
> 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
Why do you think universal closures are easier to understand? Personally I
don't find them easier, if nothing else because the formula is longer and
thus takes slightly more effort to parse mentally.
Moreover, instantiating the $e from the $a in your ax-cleq is an immediate
and obvious substitution, whereas with universal closure in bj-df-cleq we
also need applications of ax-gen.
Also, if we require the universal closures of the hypotheses, for
consistency shouldn't we also require the universal closure of the
conclusion? That would be awkward: for bj-df-clel we would have to prefix
the $p with "A. x1 ... A. xn" along with the side condition "where
x1,...,xn are the free variables in A and B", and of course the current
set.mm doesn't even have a notation that allows us to express that.
I'm not saying you are wrong, only that I don't understand the reasoning or
advantage and need to be educated. :) I know that many books show ZFC
axioms and even FOL axiomatizations with universal closures, and I've never
understood why. Requiring all proof steps to be universally closed (as some
FOL axiomatizations do) can make them quite tedious to work with. There are
"Quine closures" and "Berry closures", each with a set of rules to add,
drop, and reorder the quantifiers in universal closures as we apply ax-mp
etc. These seem like a major distraction and complication vs. using simple
open formulas, particularly when schemes are involved.
Maybe there are advantages to universal closures (sentences) for some
theoretical purposes, but I don't see any advantage for set.mm.
> (and the problem of having specific instances as hypotheses creeps up in
> the conservativity theorem, it seems).
>
Where do you see this? In any case, can't we just apply ax-gen as needed
if open formulas are problematic?
Norm
>
> 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 metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/d59b4ba0-98bf-4f30-ac10-d2d3af0e78fen%40googlegroups.com.
