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 <http://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] <mailto:metamath%[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/17a79325-e521-1175-f04e-81d318737324%40gmx.net.
