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/f387c42a-ac19-3979-851b-d5b6fb8e2638%40gmx.net.
