I think we should keep the "overloading" of equality and membership. The assumption is not hidden in set.mm, but explicit: it is ~cv (http://us2.metamath.org/mpeuni/cv.html). I still favor the forms bj-df-cleq/bj-dfclel, which imply minimal changes over the current set.mm, and which fix the concrete problem of having later theorems which misleadingly do not indicate ax-8 or ax-9 as a dependency (which is the problem which started this thread). And Wolf, who started the thread, seems to agree.
Then, we can think about calling them definitions or axioms. For the moment, I do not have an opinion: what's important is that they are $a-statements, and the distinction axiom/definition, apart from a matter of taste, has implications on other tools (mmj, mm0) which I do not know enough yet. To put what Mario wrote differently, and a bit roughly: they are more like definitions at the object level (eliminable and conservative), and more like axioms at the meta level (eliminable, see the section beginning with http://us2.metamath.org/mpeuni/eliminable1.html, but not conservative). This is similar to ax-10, ax-11, ax-13 being redundant at the object level, but not (conjecturally for all, and at least for ax-13) at the meta level. Finally, there is the possible further step I mentioned at https://github.com/metamath/set.mm/pull/965#issue-461788828 of splitting bj-df-cleq/bj-df-clel in two halves to study more precisely their implications (in which case, they would be axioms, not definitions). Benoît On Thursday, October 28, 2021 at 6:39:28 PM UTC+2 Scott Fenton wrote: > So, to me, the whole point of doing Metamath is to lay out assumptions as > explicitly as possible. We work in logic that requires us to state every > single assumption we make along the way. This is one of the things I love > about Metamath as compared to other theorem proving systems. We seem to be > embedding an assumption in making class and set equality the same thing. > This overloading leads to subtle assumptions that are not always obvious. > We can see that by the proof of ax-9 from df-cleq. This defeats the whole > point of Metamath to me. If we no longer overload equality, say by making > set equality be "==" insead of "=", we can eliminate this ambiguity. This > brings us back closer to the foundations of Metamath, so I propose we do it. > > On Thu, Oct 28, 2021 at 10:11 AM Thierry Arnoux <[email protected]> > wrote: > >> A solution is mentioned in the comment for df-cleq, shall it be >> reconsidered? >> >> * We could avoid this complication by introducing a new symbol, say >> =_2,* >> * in place of ` = ` . This would also have the advantage of making* >> * elimination of the definition straightforward, so that we could* >> * eliminate Extensionality as a hypothesis. We would then also >> have the* >> * advantage of being able to identify in various proofs exactly >> where* >> * Extensionality truly comes into play rather than just being an >> artifact* >> * of a definition. One of our theorems would then be ` x ` =_2* >> * ` y <-> x = y ` by invoking Extensionality.* >> >> * However, to conform to literature usage, we retain this >> overloaded* >> * definition. This also makes some proofs shorter and probably >> easier to* >> * read, without the constant switching between two kinds of >> equality.* >> >> As far as I understand Mario has chosen this in MM0. >> >> On 28/10/2021 18:57, 'ookami' via Metamath wrote: >> >> I am going to read carefully through all this during weekend, or whenever >> I have more time to focus on details particularly about where are the >> limits of a proof scheme like Metamath. For now I would like to remind of >> the starting point of this thread. >> And this is a problem pertaining to the current version of Metamath. The >> thread started from the observed fact, that the axiom list is somewhat >> flaky, "a good estimate of what should be in it, nothing more". This is >> something I am personally less content with. One reason is that I use this >> list on regular base to separate the regions of concern of any axiom. It is >> a source of incentives for proof modification, and I hate the idea, it >> cannot be used thoughtlessly. Actually the list seem to be very close to >> perfect, and I cannot see a good reason to leave the final gap open. >> >> The analysis has lead to df-clel and df-cleq as the culprits for the >> observed shortcoming. To my understanding they bear unnecessary >> complexity, and despite their name, they are not laid out according to the >> rules of pure doctrine, requiring definitions to be conservative (one >> downside of never having read a text book on logic is that I developed a >> language on my own, and now have to adapt to common usage). What I sense >> in this thread is some reluctance to address this defect, and I still >> havent't grasped the reason behind it. Is it habits? Is it some >> superficial imitation of concept of other sources? I don't know. I like to >> urge getting back on the track of rigor, that convinced me some ten years >> ago. >> >> I initially asked permission to add ax-9 to the list of covered axioms by >> df-cleq. This is likely not the best solution, because it does not address >> the observed lack of conservaty. What about the solution of Benoit then? >> Or develeping an intermediate stage between set theory and class theory? Or >> something else experimental. >> >> Is it possible to make some progress in this direction? Or come up with >> a (hopefully) convincing reason to stop where we are. >> >> Wolf >> [email protected] schrieb am Donnerstag, 28. Oktober 2021 um 03:55:56 >> UTC+2: >> >>> On Wed, Oct 27, 2021 at 7:22 PM Norman Megill <[email protected]> wrote: >>> >>>> 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. >>>> >>> >>> An example of a ZFC+classes expression containing class variables that >>> has no equivalent without class variables is "x e. A". Any expression >>> equivalent to this must contain the variable "A". (More on this below.) >>> >>> A more substantive observation about ZFC+classes is that it provides a >>> proof speedup, just like ACA_0 over PA (ACA_0 is a conservative extension >>> of PA that adds second order variables). Or at least it would, in a >>> traditional axiomatization; in metamath the advantage is largely nullified >>> because you can prove schemes over wff variables, which normal ZFC can't >>> do. I suspect there is still some speedup in the metamath setting because >>> being able to hide the bound variables involved in a class abstraction >>> means you don't have to substitute and alpha-rename them in deeply nested >>> situations. >>> >>> 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? >>>> >>> >>> I am talking about scheme completeness. This is very important to >>> understand because it is the crux of the argument that the textbook proofs >>> fall short of a true proof of conservativity in the metamath setting. >>> >>> 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. >>>> >>> >>> An inhabitant just means an object of that type. Here I am referring to >>> the terms that can be considered as valid things of type "class": in the >>> traditional setting, every class is either a class abstraction, i.e. >>> literally {x | ph} for some ph, or is defined to be something that >>> ultimately boils down to a class abstraction (and when traditional logics >>> talk about definition they usually mean an abbreviation at the meta-level, >>> so it is still syntactically a class abstraction). In metamath there are >>> other things of type "class", that I am calling "generic variables", by >>> which I mean "A", "B" and so on. These are not class abstractions, they are >>> variables; if you ask what syntax makes them up "cab" is nowhere to be >>> found. >>> >>> >>>> 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. >>>> >>> >>> eleq1 is a consequence of df-cleq though, which as we have already >>> established makes ax-9c derivable. If you drop df-cleq and df-clel, keeping >>> only df-clab, the mentioned theorem is true for class abstractions but not >>> for arbitrary classes (even though x = y -> (x e. A -> y e. A) involves >>> neither wceq or wcel, at least if we ignore the notation overloading and >>> read it as "weq x y -> (wvel x A -> wvel y A)"). >>> >>> >>>> 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? >>>> >>> >>> Perhaps this is not the most intuitive picture for you, but the way I >>> internalize metalogical completeness as a concept is that in the model of >>> metamath every sort contains additional things beyond the regular things. >>> The space "wff" contains more than just object level formulas, it also >>> contains "variables" which are uninterpreted / generic predicates. It is a >>> consequence of this that just because a fact is true (say by induction on >>> formulas) for every object level formula, it may not be true at these >>> "generic points" (points because we are thinking of "wff" as a space of >>> things, with the points being formulas of the object language but also >>> these uninterpreted variable things), which is another way of saying that a >>> logically complete schema may not be metalogically complete. >>> >>> Applied to the sort "class", we get that the regular points of the space >>> are the class abstractions (those are the things we put there >>> deliberately), and the generic points are the variables "A", "B" (those >>> come along for the ride because of how metamath works). And now to the >>> point: the theorem in the textbooks that reduces every theorem in the >>> object language using classes to an equivalent theorem without classes is >>> performed by induction on formulas and terms, and so it does not apply to >>> the generic points. For any metamath theorem about classes, you can always >>> make a special case of the theorem by substituting class abstractions for >>> everything and then run the elimination proof, but a plain variable "A" is >>> not eliminable: you can replace it with { x | x e. A } but you are no >>> closer to eliminating A by doing so. >>> >>> >>>> 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. >>>> >>> >>> The new mathematics is kind of fringe stuff, so I can understand why you >>> might think this, but I think this conversation started exactly because >>> Wolf has been exploring the mathematics of subsystems of set.mm's axiom >>> system where you can't take equivalence to the textbooks for granted, and >>> it is in this light that the conservativity proof starts to break down. >>> >>> Regarding my position on axioms, the issue is not that they haven't been >>> verified formally. I think I am probably more willing to accept new axioms >>> than you because I see theorems vs axioms as the difference between >>> "correct by internal reasoning" and "correct by external reasoning". In MM0 >>> of course I am planning to verify the metalogic in addition to proving >>> theorems in the logic, so making a theorem into an axiom is not cheating, >>> it is merely moving the work from one part to another. Some things are best >>> verified internally, these are the theorems; and some things are easier to >>> verify by a metatheoretic proof, and these are the axioms. From such a >>> description it should be clear why I consider df-cleq et al. axioms, and it >>> has nothing to do with believing the conservativity result to be false or >>> unverified. >>> >>> >>>> 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? >>>> >>> >>> Not a perfect match for the situation, but see >>> https://en.wikipedia.org/wiki/Type_I_and_type_II_errors . I mean that >>> we have roughly two choices, and both choices have some probability of >>> leading readers astray, in different directions. >>> >>> Mario >>> >> -- >> 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/879eb864-f2b1-40a3-9018-c5a698ad5ac8n%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/879eb864-f2b1-40a3-9018-c5a698ad5ac8n%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/28471da3-9ad8-a648-d251-258af55f22e9%40gmx.net >> >> <https://groups.google.com/d/msgid/metamath/28471da3-9ad8-a648-d251-258af55f22e9%40gmx.net?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/8225adb0-ed5c-419b-9416-390bb6c335f3n%40googlegroups.com.
