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/d610f66b-4dbc-46d3-8600-2402bca30390n%40googlegroups.com.
