Norman Megill wrote Tuesday, 26. Oktober 2021 at 21:46:35 UTC+2:
> Which comment of Benoît you are referring to? > > In PR #2267 he described the phenomenon of the vanishing ax-9 as an artifact of df-cleq and further hinted to his bj-ax9 theorem. If, as you write, ax-9 is not important any more once you arrive at df-cleq, you may as well include it to the axiom list unconditionally. >From my point of view the following aspects were important to trigger my initial post: 1. Does the axiom list appear to be trustworthy? And does it follow a consistent pattern? 2. While adding complexity to df-cleq may puzzle readers, vanishing axioms after a proof change is not better. And we have a concrete incident here. 3. df-cleq, and even more so df-clel, seem to be no ordinary definition anyway, as the right hand side does not always explain the definiendum in simpler terms, for example in case set variables are involved. It once took me quite some time to get over their recursive nature, and their implicit consequences. One is that you can restate 2 axioms directly, but only one is taken care of. I am at a loss how text books handle these issues; I never read one on logic. I am willing to believe that Metamath outperforms a majority of them. But this should be no reason for missing out an improvement, right? So far I think there is unusual complexity inherent to df-cleq, and since you cannot avoid people possibly be overwhelmed by it, you can at least syntactically take a clean stance. Wolf -- 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/34ea47c9-0b57-4b1c-8cc4-6e81617a3fefn%40googlegroups.com.
