On Wed, Oct 27, 2021 at 11:40 AM Norman Megill <[email protected]> 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, especially if you pay attention to metalogical completeness. 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. 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. 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 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 *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 axioms then readers might think that ZFC isn't enough for mathematics (which I actually think is mostly true - 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). -- 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/CAFXXJSsW8U7mtdSqz7r37Tp6peVhqtKeAqdPZWLr1hfkp5SuMQ%40mail.gmail.com.
