I'll speak mainly to the MM0 side of this. I noticed some time ago that using definitions allows you to switch out bound variables. I even considered adding it explicitly into the definitional equality rules: basically, you can prove that two expressions which are alpha-equivalent are definitionally equal by introducing a definition that hides all the bound variables. This is inherent in the concept of hiding bound variables to begin with - if you aren't tracking them, then you can perform alpha conversion when re-expanding the definition. As things stand currently, there is no primitive rule you can use in the checker (as it's a bit annoying to implement general alpha equivalence), but it's nevertheless considered to be part of the underlying logical system.
The place where I would point if you want to stop this mechanism is the "free" sort modifier, which prevents you from using a variable as a dummy variable. By not marking a sort as free, you are opting into a formal system which has bound variables, including alpha conversion. So as it relates to your diagnosis: it's not that the definition is not conservative -- there is a hidden axiom schema which says you can do alpha conversion, because definition unfolding is only sensible relative to an alpha-conversion-respecting congruence. So what's the metamath analog of this? The definition checking mechanism makes a bunch of assumptions about the general shape of the database, and also the provability of some structural theorems. The quest to determine exactly what those assumptions are is what led to the 'Models for Metamath' paper, and later to MM0. But the short answer is that the simple rule for definitions, that they don't drop variables from the RHS, is too strict for real world definitions in set.mm, so you need an analysis that accounts for bound variables, even though metamath has no built in concept of bound variables. That means the definition checker needs to be referring to some theorems about alpha conversion (this is the justification theorem). In your version of the checklist: > > Rule 1. It is a biconditional and the root symbol on the LHS is a new > token. > Rule 2. There are no expressions between the syntax axiom "whack" and the > definition "df-hack". > Rule 3. Variables on the LHS don't share DV conditions. > Rule 4. Dummy variables (in this case "t") are disjoint from all other > variables. > Rule 5. There are no non-setvar dummy variables. > Rule 6. Every setvar dummy variable is not free. You left out the part where steps 4-6 are one of two options, the other of which is to prove a justification theorem which says that the definition is equivalent to a version with all the bound variables renamed (the justification theorem). In fact, the purpose of steps 4-6 is to prove the justification theorem, relying on a metatheorem saying that these three steps are sufficient. However, the proof of that metatheorem relies on some axioms; mainly this is an application of the theorems from the df-cdeq section (https://us.metamath.org/mpeuni/mmtheorems38.html#df-cdeq). I believe if you look at the axioms required there, in particular cdeqal1, you will find the expected dependence on ax-7. On Sun, Jul 13, 2025 at 1:42 AM Gino Giotto <[email protected]> wrote: > My diagnosis is actually very close to what MM1 is already doing. In MM1, > the user has to prove the derivable "|-" version of the definition and > therefore the statement holds an axiom usage that will be inherited by its > descendants. The sole problem of MM1 is the proof itself: > > pub theorem df_inter {x: set} (A B: class): $ A i^i B = {x | x ec. A /\ x > ec. B} $= 'eqcid; ---> This proof should be rejected by the mm0-c > verifier, because eqcid is not the justification theorem of df_inter. > > pub theorem df_inter {x: set} (A B: class): $ A i^i B = {x | x ec. A /\ x > ec. B} $= '(! interjust y); ---> This is the correct proof. Notice that > it requires ax_8b, therefore solving the issue (source for complete proof > is in ax8bvv.mm1 > <https://github.com/GinoGiotto/mm1_test/blob/main/ax8bvv.mm1>). > There is a way to accomplish this behavior, which is to require that in a definition unfolding, you don't get to pick the bound variable names, or if you do they must be disjoint from everything in the statement. But in practice this was rather annoying, especially since definition unfolding turns out to be convenient in places other than just proving the definitional theorem. I am also not sure it works in general -- you can again prove the justification theorem by re-folding the definition twice instead of unfolding. So re-folding also has to be banned and at that point it's not really a congruence at all, it's just a magic theorem you have to prove with every definition which does not interact with regular proofs. That is, it would look more like: def Inter (A B: class) {.x: set}: class = $ {x | x ec. A /\ x ec. B} $ because '(! interjust x y); In MM0/MM1, I'm not sure whether this is a bug of mm0-c or a specification > issue. I just don't know the language well enough to make a judgment, but > the expected behaviour that prevents such exploit to happen seems clear. > > Regarding metamath, I see two ways to fix it. The first would be to add > the justification theorem as hypothesis on every definition that uses dummy > variables. The second would be to define definitions in the metamath > specification. This topic has been brought up several times in the past and > always ended up in a nothing burger, so my expectation for change is low. I > am more hopeful about MM0 tho. > > A simple specification change would be to add a new keyword, say "$k", > that formalizes our definitions. In the same way that every "$p" statement > must have a proof of its statment, every "$k" statement must have a proof > of its justification theorem (again, this is similar to MM1). > Adding definitions to metamath is not easy. In fact, if you try it you will basically land on the MM0 design, or something very similar, because you will also need to add definitional unfolding and a concept of bound variables (because you need to know how to construct the target theorem to be proved by the $k proof). Possibly you get something simpler if you require justification theorems for everything instead of baking in rules 4-6 as the checker, but I don't think it will be much simpler. > Even rule 1 could be removed. The expression doesn't have to be a > biconditional or an equality. This would allow us to consider df-bi as an > actual definition, and not include it in an exception list: > Doing this requires introducing the definitional equality congruence relation to replace it, as MM0 does. > In general, every statement has its own justification theorem. For > example, the justification theorem of: > > sstr2 <https://us.metamath.org/mpeuni/sstr2.html> $p |- ( A C_ B -> ( B > C_ C -> A C_ C ) ) $. > > is: > > ${ > $d A x $. $d B x $. $d B y $. $d C y $. $d A z $. $d C z $. > sstr2just $p |- ( A. x ( x e. A -> x e. B ) -> ( A. y ( y e. B -> y e. C > ) -> A. z ( z e. A -> z e. C ) ) ) $. > $} > > And here we can see another reason why the current system is flawed. The > current proof of sstr2 uses axioms up to ax-4, because it is proved with: > > sstr2just_wrong $p |- ( A. x ( x e. A -> x e. B ) -> ( A. x ( x e. B -> x > e. C ) -> A. x ( x e. A -> x e. C ) ) ) $. > > The incorrect justification can be proved from al2imi and imim1 alone. > However, the correct justification is sstr2just, because we can use sstr2 > to change bound variables and we can prove sstr2just from sstr2 using > propositional logic alone (while we cannot use sstr2just_wrong to change > bound vars). Therefore, sstr2 should hold the axiom usage of sstr2just, > which is higher than the one it currently has. > I don't agree with this. You can argue that every usage of df-ss is really an abbreviation for A. x ( x e. A -> x e. B ) where x is a fixed variable used regardless of A and B, and then sstr2just is a correct proof of it. You seem to presuppose here that the variables have to be used "generatively" i.e. every occurrence of the formula should be substituted for a different variable, but then you would not even be able to say that ( A C_ B -> A C_ B ) is an instance of id, which breaks the substitution property. Much better to just check in advance that the definition doesn't put any constraints on what variable you use, so that any unfolding is valid. This requires proving the justification theorem, one way or another. -- 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 visit https://groups.google.com/d/msgid/metamath/CAFXXJSsJ0ZvmTtKP30fy4UjsuaBmwDex%3DEBZfWHCzhhsokp-tA%40mail.gmail.com.
