On Tuesday, October 26, 2021 at 6:07:19 PM UTC-4 ookami wrote: > 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. >
ax-9 is not the only problem. Note that with bitri+bicomi+df-cleq we can prove an instance of cbvalv, which requires ax-4-7,10-13 for its proof. If a future set theory proof needed that exact instance of cbvalv, we could "cheat" and use df-cleq instead to bypass all those axioms. I think Benoit's result that df-cleq implies ax-9 is nice and should be documented in the comment for df-cleq, but I think it would be weird and confusing to add ax-9 as a hypothesis. And if we do that, we should also add ax-4-7,10-13 to be consistent. We have ax-ext as a hypothesis of df-cleq because which ZFC axioms are needed for a result is considered important in the development of set theory. But we ordinarily don't care about which FOL= (FOL+equality) axioms are used after we get into set theory. In the development of FOL= itself, it is useful to derive results using the fewest axioms possible. It can help towards proving independence of the axioms and possibly finding weaker or alternate versions of axioms in the future. I appreciate the work you have done towards that. Once we get to interesting results in set theory, all of the FOL= axioms will pretty much be used anyway. Effort spent to eliminate the use of this or that FOL= axiom in the set theory development doesn't seem productive to me, and it may even be confusing to the reader to see longer proofs that may result just to avoid using a certain FOL= axiom in a set theory 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? > > The "This theorem was proved from axioms" axiom list on the web pages is generated as a convenience for the reader. As noted, df-cleq can distort this, so in principle the "This theorem depends on definitions" list must also be considered. I suppose that once into set theory, I could replace the FOL= axiom list with just a fixed phrase meaning "you might as well assume that all FOL= axioms are used", but that would require messy metamath.exe code customized to set.mm to detect the set theory section, and I really don't want to do that. A partial fix (without changing df-cleq itself) is to insert an artificial application of ax-9 in the proof of dfcleq (in a way that doesn't 'minimize' out, or make its proof modification discouraged) for the cosmetic reason of making the axiom list include ax-9 when dfcleq is used, since ax-9 seems to be the main concern here. Could you do that? That should address most cases that we see in practice. > > 1. > 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. > > Yes, these are not ordinary definitions. They are discussed in some detail at http://us.metamath.org/mpeuni/mmset.html#class. I am at a loss how text books handle these issues; I never read one on > logic. > Textbooks don't handle these issues. Which axioms of FOL= are needed for a set theory proof aren't considered important or even discussed. Norm -- 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/be783362-425b-4fb3-b07e-e04d87e756a4n%40googlegroups.com.
