(The us2 server was down most of the afternoon due to a power failure caused by a storm. It should be back up now.)
On Wednesday, October 27, 2021 at 1:18:17 PM UTC-4 di.... wrote: > On Wed, Oct 27, 2021 at 11:40 AM Norman Megill wrote: > >> 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 think that this is true. > In fact, ZFC + classes is a conservative extension in exactly the same way > that NBG is, > There is a fundamental difference. NBG has global choice, which has no ZFC equivalent. From the wikip page on NBG, "the axiom of global choice ... is stronger than ZFC's axiom of choice". On the other hand, any ZFC+classes expression containing class variables can be converted to an equivalent expression with wff variables, and vice-versa. They are just two different notations for the same thing. See Takeuti/Zaring Ch. 4 or Levy Appendix X or Quine pp. 15-21. Class variables can be considered wff (meta)variables in disguise. See also the comments in ~abeq2. > especially if you pay attention to metalogical completeness. > What does this have to do with our metalogical (scheme) completeness - or do you mean something else? > As far as I can tell, the standard argument that classes are a > definitional extension only applies if we think that the only inhabitants > of "class" are class abstractions, but in metamath there are always > variables living in every sort, and you can't prove properties about > generic variables even if the property holds for all class abstractions. > Sorry, I don't understand what this sentence means. :) What is an inhabitant, "living in every sort", generic variable, property? There are no "generic" variables (as I understand that word) in set.mm; there are only wff, setvar, and class variables. > A simple example of this is axiom ax-9c, which is true for class > abstractions > because of df-clab (i.e. x = y -> (x e. { z | ph } -> y e. { z | ph }) is > true by properties of substitution) but cannot be proven for arbitrary > classes. > This is an instance of eleq1+biimpd, which holds for arbitrary classes. > > Traditional textbooks don't cover this, because of course metalogical > completeness isn't a thing. But I think it is impossible for metamath to > introduce a new sort without letting these extra variable terms sneak in, > so metalogical completeness is always relevant to us. I believe that > conservativity in the traditional sense still applies to the set.mm > formulation of "class" over the set-only part of , but nothing stronger > than that. > I don't understand what you mean. What is an example of extra variable terms that sneak in? > > >> 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? >> > > What it amounts to is that all our tools are saying it's not a definition, > and the only reason it is considered a definition is because we are > explicitly overriding the tool and declaring them definitions by fiat. > Furthermore, because of the notational overloading situation, these > definitions are > There is no new mathematics that results from the class theory definitions, and as a practical matter I have chosen to trust the multiple proofs of conservation and eliminability in the literature. In principle they could be proved formally. Class theory is simply a different notation for the same thing that is often more practical to work with. Since no new mathematics results from the class theory definitions, it's hard for me to justify calling them axioms. I understand that these literature proofs may not qualify as a "trusted base" from your point of view since they haven't been verified formally. In which case it would make sense for you to rename/treat them as ax-* in your copy of set.mm. > *actually* proving new lemmas, it's not merely a theoretical concern. If > ax-9c at least existed as an axiom, then we could at least say that the > definitions are not load-bearing, they only prove theorems that were > already true beforehand, but it's not that way in the current setup. I > think this weakens the trust in the overall distinction between definition > and axiom, so users can't just ignore the "This theorem depends on > definitions" list, which is much larger than the axioms list. > > 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. >> > > For a careful reader, it is not clear to me what the relative > probabilities of the "type I and type II errors" here are. As you say, if > we mark them as > What are type i and type II errors? > axioms then readers might think that ZFC isn't enough for mathematics > (which I actually think is mostly true > Whether or not ZFC is enough for mathematics, class notation does not strengthen it. - the class extension exists in metamath for a very good reason), and if we > mark them as definitions then people (like Wolf in this very thread) might > get confused about by what standard we judge axioms to be "definitions", > which is a question of high importance considering that it forms part of > the trusted base of metamath (since verifiers don't check it). > The standard is that a definition must be conservative and eliminable. 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/d29be18b-0ee3-4421-a341-5f608821aeb3n%40googlegroups.com.
