On Sat, Jun 15, 2019 at 12:11 PM Norman Megill <[email protected]> wrote:
> On Saturday, June 15, 2019 at 7:05:57 AM UTC-4, Mario Carneiro wrote: > > Also the existing definition checker has hardcoded names all over the >> place, which has already caused problems on one occasion; adding a $j >> parser would fix this issue. >> > > BTW if the checker is going to be rewritten, is this a good time to change > the definition of T. to be A. x x = x <-> A. x x = x? You mentioned that > there is a special section for df-tru, and it could be eliminated if we > make this change. > Yes, that would work. On Fri, Jun 14, 2019 at 1:30 PM Norman Megill wrote: >> > The four definitions df-bi, df-clab, df-cleq, and df-clel are excluded >>> from the current definition check. Any new software will have to treat >>> these 4 as special cases, for example by treating them as additional >>> axioms. Hopefully these 4 are the only ones that will ever need special >>> treatment. >>> >> >> I would like to renew my suggestion that we change these to ax-bi, >> ax-clab, ax-cleq, ax-clel. It adds complexity to the tooling to have an >> inconsistent naming convention, since we are signaling that these are >> definitions when they don't meet the criteria, and it's also a lie to the >> reader because these look like definitions and claim to be definitions and >> the user may even know that we check definitions for soundness, yet these >> definitions each have extremely subtle problems that make them invalid as >> definitions. >> > > I'm pretty sure these meet the literature criteria of being valid > definitions. They are eliminable and don't add any new theorems when > eliminated down to the primitive language. The class definitions have > detailed soundness proofs in the literature. In what sense do you see them > as invalid? > > The problem with calling them axioms is primarily psychological, implying > that the real axioms aren't sufficient to express ZFC. It sends the wrong > message. Also, they will show up in the "This theorem was proved from > axioms" list unless I hard-code them into metamath.exe to exclude them from > that list. > > The issue is that the tools to check them aren't sufficiently > sophisticated (and probably will never be) to check that they are valid > definitions, so we make them exceptions for the purpose of those tools. (I > think an early version of Ghilbert checked the soundness of df-bi using its > justification theorem, but I don't recall the details. @raph may wish to > comment if he is listening.) As far as I can tell, there will only be > these 4 exceptions and no others in the future. Tools could recognize an > exceptions list like the mmj2 definition check does now. Or perhaps add a > special $j statement? I think you already mentioned that checking tools > shouldn't depend on labeling conventions. > Metamath is a formal verifier. When it says that something is true, we believe it because it's checking everything down to the axioms. If we take that spirit to definitions, it means that when we claim something is conservative, that should mean that we've checked that it is conservative, again down to axioms, down to some system that we can check generally for soundness. So that means that when faced with an unusual definition, we are faced with a choice: Either we formalize a generic checking process that can verify the definitional scheme in use, or we assert it as a fact and leave verification to the meta level, i.e. call it an axiom. It's not sufficient that the definition be true or conservative; we have good reasons to believe that the real numbers are constructible in ZFC but we do the construction anyway, because we want to demonstrate it such that the computer can check it. I've gone to some trouble to come up with a valid definition schema, both in the mmj2 definition checker and again in MM0, and I think Raph also has a definition schema in Ghilbert. If we apply such a schema to metamath, we can justify most of the current definitions, but it's not exactly a check for conservativity so much as a syntactic check that implies conservativity as a metatheorem. The definitions that fail the MM0 definition schema are df-tru, df-bi, df-clab, df-cleq, df-clel. For each of these, we have some reason to think that the definitions are conservative but something about the definition makes the standard analysis fail. So we need to either make the schema more complicated to accomodate them, or call them axioms (which is not a cop-out - it's communicating that the tool is not capable of validating the axiom, but we have reasons to believe it anyway and punt on verification to the meta level). Note that in the MM -> MM0 -> Lean translation, all axioms become proof obligations, so it's actually important that things are marked as axiom when we expect a meta level proof. * df-tru is problematic for reasons I've discussed in another thread (the lack of existential quantification over wffs). But a resolution is proposed so I will skip this. * df-bi is not written as an iff. It has a definition but df-bi itself doesn't make it obvious what that definition is. The theorem is more like a consequence of the definition than the definition itself. This can be addressed by a $j that points to dfbi1 to indicate the definition of wb, and to bijust to indicate how to prove the unfolded statement. So I think this is addressable. * df-clab is definitely not an axiom. It is a way to relate two primitive constructors. Metamath, and MM0, have no way to introduce new sorts by other than axiomatic means. HOL has function types and subset types, but these are in general not conservative extensions. We could have a definition schema that creates new sorts; in general, the admissible sorts would be a subclass of the collection of n-ary predicates on V. This is doable, but would be a pretty significant addition to the metatheory. * df-clel and df-cleq are tricky because of the overloaded notation. At the very least there is a claim that weq x y <-> wceq (cv x) (cv y) that has been smuggled in without proof. Set theory is not required to justify the class sort, so perhaps it could be moved up and wceq and weq could be untangled. This would also avoid the need to have df-cleq depend on ax-ext. > If the goal is to be open and straightforward, I think it is a more honest >> approach to call them axioms and explain in detail why they are >> conservative. >> > > But if they are conservative, then they aren't really new axioms. We have > very detailed explanations of df-clab, df-cleq, and df-clel on the MPE home > page in the Theory of Classes section, and df-bi has a long explanation in > its comment. We could enhance the explanations if that would help. > Things which we think are correct but for which we have an informal justification rather than a formal proof are exactly what axioms are for. Obviously we prefer formal proofs over axioms when possible, but for the most part with definitions it's pretty obvious that we can't just remove the axiom or prove it from what precedes it. (In fact, df-cleq is not even conservative!) >> > > In the context of ZFC it is, if what you mean is that it depends on > ax-ext. That is also explained in the Theory of Classes. And the > definition has ax-ext as a hypothesis, so it doesn't actually depend on > ax-ext until we eliminate that hypothesis. > It is conservative in the same sense that ax-17 is redundant. The classical theory doesn't have metavariables, so there are certain statements that metamath can express that aren't in the traditional accounting, and this slightly changes the meaning of "conservative" because the language is larger. To be more precise, the theorem |- ( A = B -> ( x e. A -> x e. B ) ) is expressible but not provable until df-cleq is introduced. As mentioned above, the introduction order of = and e. on classes is muddled up with the version for sets, and so as things stand today I can't call df-cleq and df-clel anything but axioms. If there were a few more variations on = and e. in the prelude, eliminated straight away similar to <RR, we could have these be plain definitions. 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/CAFXXJStQvOC%3DTpCJ3G0aqjNGwt%2B5qCkLokQr2yf4gAJD91Xzng%40mail.gmail.com.
