Personally, I think the easiest way to address the issues is to make df-cleq, df-clab, df-clel axioms instead of "definitions". They are not definitions according to the definition checker algorithm, they are not conservative as observed in this thread, and they significantly complicate the metatheoretic analysis of the axiom system. Even if we want to think that "class" is a conservative extension of ZFC, that is only when you introduce the whole set of axioms at once, and even then we must assume the full set of FOL axioms (like ax-9) to start with. Metamath does not have an adequate mechanism for introducing new conservative sorts, and I think we should just own up to this and admit these as axioms.
On Wed, Oct 27, 2021 at 8:04 AM Norman Megill <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/be783362-425b-4fb3-b07e-e04d87e756a4n%40googlegroups.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/CAFXXJSt8tBN6_aUAHnPz1PF0E-j9%3DOuQqVWyoyTGOhV2VECaKQ%40mail.gmail.com.
