On Thu, Oct 28, 2021 at 7:19 PM Norman Megill <[email protected]> wrote:
> So the scheme x e. A is equivalent i.e. represents the same set of object > language wffs as the scheme [ x / y ] ph. > > ZFC+classes is exactly equivalent to ZFC in terms of the object-language > theorems it can prove. This is true, but a metamath assertion is more than just its image on the object language. If you view a metamath assertion as simply a set of object language theorems then there is no distinction between logical completeness and metalogical completeness. > This is very different from NGB as a "conservative extension of ZFC", > which has statements stronger than what ZFC can prove such as global choice > (primarily because the class variables in ZFC+classes cannot be > existentially quantified). > It is possible to state global choice in ZFC+classes, and indeed this has been proposed for set.mm in the past. It is a conservative extension, so when you say it is "stronger" this is only as a theorem of NBG or ZFC+classes in the extended language; the base language is not strengthened by the presence of global choice. > In Shoenfield, section 4.6 starting p. 57 is titled "Extensions by > > definitions", covering definitions of new predicate symbols and > > definitions of new function symbols. He states (p. 60) that, "We say > > that T' is an /extension by definitions/ of T if T' is obtained from T > > by a finite number of extensions of the two types which we have > described." > > I don't have a copy of Shoenfield, but from what you quote he is still > calling them "definitions" rather than new axioms. > I think in this case "extension by definitions" is talking about definitions in the strict sense, i.e. the kind that can be checked by mmj2. As for Mendelson, he uses NBG which has class variables built in, so it > doesn't really apply to set.mm. > > Takeuti/Zaring has the same class theory as we do, and their versions of > df-clab,cleq,clel are all called "definitions". > > The only place I could find class theory definitions called "axioms" is in > Levy. But he calls them "extralogical axioms", whatever that means, > compared to what he calls the "logical axioms" of ZFC. Perhaps he doesn't > consider them "real" axioms? > The term "extralogical axioms" is usually applied to anything beyond (predicate) logic, e.g. the axioms of ZFC as distinct from pure FOL. Just to be clear, I am okay with the current state of affairs, this isn't a hill I am willing to die on. To the extent that we can, we should call these oddities out and clarify them for readers, but tools can work around this ( "$j not-really-a-definition "df-clel";" anyone?), and removing the notation overloading has a high cost for users and the library generally, so the tradeoff may not be worth 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/CAFXXJSs2w4HUEOJK3AFCHG%2BFGvmhOLuYhb9zSy3Yy3%2BRVZ_M3A%40mail.gmail.com.
