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/84d84d58-82a7-4076-a0cc-6db12ef7d801n%40googlegroups.com.
