I discuss the issue of whether to call df-clab,cleq,clel axioms at the end of the http://us.metamath.org/mpeuni/mmset.html#class section. Most authors call them definitions, and my feeling is that calling them axioms would be somewhat misleading since they can (in the presence of ax-ext) always be eliminated back to equivalent statements in the primitive language.
While I'm not sure what the correct terminology is, class notation as a "conservative extension" is not the same notion as calling NBG a "conservative extension" of ZFC: in the former case, any class expression can be converted back and forth to an equivalent expression in the native language, whereas in the latter case, there are statements such as global choice that cannot be expressed in the ZFC language and have no equivalent in ZFC. I don't see the fact that our definitional check algorithm can't check them as sufficient justification in itself to call them axioms. If we had adopted the usual textbook convention of using multipart recursive definitions for df-oadd etc. instead of our direct definitions with `rec`, would you want to call those axioms? Most importantly, though, I don't want to give the reader (who typically is not a set theorist or even a mathematician) the impression that the axioms of set theory aren't sufficient in principle for essentially all of math. I think that calling df-cleq an "axiom" simply due to limitations of Metamath is not necessarily helpful to the average person just wanting an overall understanding of the foundations of math. You have a somewhat different goal wrt formal verification, and for your purposes calling them ax-clab,cleq,clel (with a simple global label replacement in set.mm) may very well be preferred. Part of my goal has been to break down mathematics into the smallest possible steps that an average person can in principle verify for themselves (whether or not they are able to grasp the big picture), while also trying to communicate in more general terms the foundations of set theory and thus mathematics in mmset.html, in a way that doesn't confuse people with "if ZFC is sufficient, why do we need axioms beyond ZFC?" I think our goals have worked together synergistically. Aside from ax-9, some issues with definitions are not unique to df-cleq. 1. Let us temporarily add to our propositional calculus system the (redundant) axioms bitri and bicomi. From those two axioms, we cannot prove biid. Yet from those two axioms plus df-or, we can prove an instance of biid. So df-or implies something stronger than those two axioms. Since in our system we use ax-1,2,3 to prove biid, does this mean we should include ax-1,2,3 as additional hypotheses for df-or? 2. The cbvalv-type loophole applies to any definition with dummy variables, not just df-cleq. Fortunately the only two definitions with dummy variables before set theory are df-tru and df-eu. And fortunately df-eu comes after cbvalv, so this loophole doesn't add strength to the language in that case (although in theory it could disturb the "This theorem was proved from axioms" list). As for df-tru, well, it's had a long history of being problematic, and a purist might want to move it below cbvalv, but that would be ugly. Norm On Wednesday, October 27, 2021 at 8:33:17 AM UTC-4 di.... wrote: > 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 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/6237af1f-9c0c-423e-a2f8-cb9cd693a2c5n%40googlegroups.com.
