A flaw in the metamath definition system?
157 views
Skip to first unread message
Gino Giotto
Jul 12, 2025, 7:42:43 PMJul 12
to Metamath
This is a topic I have been wondering for a while, and it's the main motivation behind the question in this conversation. I believe there is a soundness issue in the way metamath-like systems handle definitions. Note that this is a different topic from the one brought up in https://github.com/metamath/set.mm/pull/4909. That PR was about unsound definitions, while this mailing thread is about sound ones.
The metamath proofs contained in this email are available in my mathbox here (commit f03b065), while the MM1 databases are available here. Therefore, the correctness of every discussed theorem can be verified.
Consider the following definition:
$c H. $.
$( Add defininition syntax. $)
whack $a wff [ H. x y ] $.
${
$d t x $. $d t y $.
$( Add a definition that does not violate the conventions rules.
(Contributed by GG, 1-Jul-2025.) $)
df-hack $a |- ( [ H. x y ] <-> A. t ( t = x -> t e. y ) ) $.
$}
The statement df-hack is "sound", in the sense that it does not violate any of the rules on the conventions page:
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.
So the definition df-hack would be acceptable based solely on the conventions. Of course, definitions usually have to go through a human review as well, which is stricter, but that doesn't matter for the point of this mailing thread.
The idea behind those conventions is to provide conservativity and eliminability, which are the two main properties people agree on regarding what rules sound definitions should follow. So the question is: Does df-hack obey conservativity and eliminability?
We can make the first observation by using df-hack to prove the following statement:
${
$d u x y $. $d v x y $.
hack1 $p |- ( A. u ( u = x -> u e. y ) -> A. v ( v = x -> v e. y ) ) $=
( whack weq wel wi wal df-hack sylbb1 ) ABEDAFDBGHDICAFCBGHCIABDJABCJK $.
$}
Now, hack1 doesn't look particularly remarkable. It's simply a theorem about changing bound variables. What's unusual is its axiom usage:
MM> sh tr hack1 /ax /ma ax-*
Statement "hack1" assumes the following axioms ($a statements):
ax-mp ax-1 ax-2 ax-3
We proved a theorem about changing bound variables from propositional logic alone, which shouldn't be possible. This observation led me to investigate further. The immediate line of thought was: "Well, df-hack is conservative over a larger set of axioms, it's obviously not conservative over propositional logic alone". Not so fast. If we follow this reasoning then there are more results that go wrong.
First of all, this means that any definition is potentially not conservative, and we should be really careful in determining which definition is conservative over which axiom system. If we expand our axiom system to include predicate logic with equality and ax-12 then we can prove:
${
$d t x z $. $d t y z $.
$( Proof of ~ ax-8 with DV conditions, without using ~ ax-8 . (Contributed
by GG, 1-Jul-2025.) $)
ax8vv $p |- ( x = y -> ( x e. z -> y e. z ) ) $=
( vt weq wel equtr wal ax12v hack1 19.21bi syl6 com3r equcoms com12 ax6ev
wi syld exlimiiv ) DAEZABEZACFZBCFZQZQDTUADBEZUDDABGUEUDQADUEADEZUDUFUDQB
DUFUBBDEZUCUFUBUFUBQAHZUGUCQZUBADIUHUIBDCBAJKLMNONRDAPS $.
$}
MM> sh tr ax8vv /ax /ma ax-*
Statement "ax8vv" assumes the following axioms ($a statements):
ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-12
The statement ax8vv is a version of ax-8 with DV conditions. As confirmed by Mario and Benoît in https://groups.google.com/g/metamath/c/ENg8Hdvlpn4 ax8vv is independent from the axioms listed by above, so this proves that df-hack is not even conservative over predicate logic (to be precise, the proof uses the weaker ax6v and ax12v, which don't require ax-13).
The other relevant observation is that df-hack is not eliminable either. If you unwrap the definition then the proof of ax8vv will break, and of course it must break because ax8vv cannot be proved from the listed set of axioms.
-------------------------------------------------------------------------------------------------------------------------------------------
Above, I provided a soundess issue by adding a new definition, not present in the database. However, the issue should hold for pretty much any definition with dummy variables, so we should be able to find a hack using an already existing one. There are many definitions we can choose from. I'm going to pick df-in because it's simple and it's probably one of the least controversial ones in mathematics (most school textbooks have it).
Long story short, from df-in we can prove:
${
$d x B $. $d y B $.
$( One direction of ~ eleq1w with DV conditions. This proof does not use
~ ax-8 . (Contributed by GG, 1-Jul-2025.) $)
ax8bvv $p |- ( x = y -> ( x e. B -> y e. B ) ) $=
( cv wcel wa wi weq ax8bvv-lem9 anidm wn pm2.24 com3l sylnbi simp1r mpcom
3exp ja ) ADCEZSFZBDCEZUAFZGABHZSUAGZABCCITUBUCUDGZTSUESJSSKUCUASUCUAGLMN
UBUCSUAUAUAUCSOQRP $.
$}
MM> sh tr ax8bvv /ax /ma ax-*
Statement "ax8bvv" assumes the following axioms ($a statements):
ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-12 ax-ext
Theorem ax8bvv is a version of ax8vv that replaces a setvar with a class variable. The axiom usage is higher than the one of ax8vv, since we have to unwrap class abstractions, which adds ax-9 and ax-ext. My understanding it that the addition of those axioms shouldn't be sufficient to prove ax8bvv, because ax-9 is already proved to not be so and ax-ext has equality as consequent, which is interpreted as the always true relation in Benoit's paper (therefore proving that it exists a model where all of listed axioms are true and ax8bvv is false).
I should mention that ax8bvv uses also df-clab and df-cleq (note that it does not use df-clel, which was the historically guilty definition to prove ax-8). However, df-cleq has been revised in 2023 to solve the known conservativity issues and the topic has been put to bed ever since. If df-cleq and df-clab are responsable for the proof of ax8bvv, it means they are still not conservative despite the revision. According to this comment, the update provideded conservativity of {df-clab, df-cleq, df-clel} over {ax-mp, ax-gen, ax-1--ax-7, ax-ext}.
These results suggest that there might be a flaw in the metamath definition system, since the known issues regarding definitions of class abstractions are applicable even to more standard ones.
----------------------------------------------------------------------------------------------------------------------------------------
Before talking about the diganosis and a proposed solution, there is more information that I would like to share. After noticing the issue, I thought: "Does this hack work in MM1?". The examination of this topic becomes more interesting in light of MM0 premises and mechanisms. First of all, MM0 has definitions in the specification, which means that it has fewer "excuses". The MM0 language is supposed to provide conservativity and eliminability by design. There is no "well, technically every definition is an axiom in the MM specification" or "a definition might be conservative over a set of axioms, but not another", no no, definitions in MM0 should not affect the user's capability of proving statements in the primitive language because that's the job of the axioms (as stated here). Definitions should serve the purpose of making expressions shorter and practical to use. The MM0 language promises users to be able to study any kind of logical system and subsytem that can be expressed in the form of axioms and rules of inferences (source: youtube tutorial). Therefore, for any given axiomatic system that I choose in MM0, I should be guaranteed that definitions do not affect my capability of proving statements in the primitive language. Moreover, the MM0 environment is supposed to have a mechanism to verify the verifier, so an exploit of that mechanism would be informationally valuable.
It was agreed that the system discussed in https://groups.google.com/g/metamath/c/ENg8Hdvlpn4/m/9NSC1Sk9AgAJ and https://github.com/digama0/mm0/pull/149 is a fair translation of the set.mm system. It is very similar to the one used in peano.mm0 (with only essential differences, like using "set" instead of "nat") and it's identical to the set.mm formalization without overloading.
To prove ax8vvv, I used:
I added the definition:
Which allowed me to derive:
In practice, ax8vvv is a version of ax-8 with all setvars disjoint from one another. This database doesn't use df-clel, df-cleq or any historically controversial definition. It's a clean proof of ax8vvv from predicate logic with equality and ax12v (the ax_12 version used in MM0 translates to ax12v in metamath, because of the MM0 DV rules with bound variables). As stated above, the creation of such proof shouldn't be possible.
----------------------------------------------------------------------------------------------------------------------------------------------
Now the second proof. The derivation of ax8bvv from df-in. The axiomatic setting makes this case even more interesting.
To the above system, I added the following definition:
Inter is the same definition used in peano.mm0. There is the minor notation difference about using "ec." instead of "e.", because peano.mm0 uses "e." in elab, while set.mm0 uses "ec." in ax_clab, so our notation should follow set.mm0 (also "e." is used for df_clel in set.mm0, while peano.mm0 does not define it).
From the above setting, we can prove:
The resulting ax8bvv has a class replacing a setvar. Interestingly, ax8bvv looks very similar to ax_8b, which is stated as an axiom in set.mm0:
The fact that ax8bvv uses neither ax_8 nor ax_8b is a sign that something is wrong. The axioms needed for ax8bvv are: ax_1, ax_2, ax_3, ax_4, ax_gen, ax_5, ax_6 (which is ax6v), ax_7, ax_12 (which is ax12v), ax_clab. The latter is identical to the df-clab in set.mm and we could even argue that the MM0 version is "safer" because it does not overload the membership relation.
Both databases have been verified with the following commands:
./mm0-rs compile -W ax8vvv.mm1 ax8vvv.mmb
./mm0-c ax8vvv.mmb < ax8vvv.mm0
./mm0-rs compile -W ax8bvv.mm1 ax8bvv.mmb
./mm0-c ax8bvv.mmb < ax8bvv.mm0
These are exactly the CI commands of the MM0 repository, used to verify the correctness of peano.mm1 and others. The verification yields no errors and no warnings for both of my databses. So I believe we have an exploit.
---------------------------------------------------------------------------------------------------------------------------------------------
Diagnosis and approach towards a fix.
The metamath proofs contained in this email are available in my mathbox here (commit f03b065), while the MM1 databases are available here. Therefore, the correctness of every discussed theorem can be verified.
Consider the following definition:
$c H. $.
$( Add defininition syntax. $)
whack $a wff [ H. x y ] $.
${
$d t x $. $d t y $.
$( Add a definition that does not violate the conventions rules.
(Contributed by GG, 1-Jul-2025.) $)
df-hack $a |- ( [ H. x y ] <-> A. t ( t = x -> t e. y ) ) $.
$}
The statement df-hack is "sound", in the sense that it does not violate any of the rules on the conventions page:
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.
So the definition df-hack would be acceptable based solely on the conventions. Of course, definitions usually have to go through a human review as well, which is stricter, but that doesn't matter for the point of this mailing thread.
The idea behind those conventions is to provide conservativity and eliminability, which are the two main properties people agree on regarding what rules sound definitions should follow. So the question is: Does df-hack obey conservativity and eliminability?
We can make the first observation by using df-hack to prove the following statement:
${
$d u x y $. $d v x y $.
hack1 $p |- ( A. u ( u = x -> u e. y ) -> A. v ( v = x -> v e. y ) ) $=
( whack weq wel wi wal df-hack sylbb1 ) ABEDAFDBGHDICAFCBGHCIABDJABCJK $.
$}
Now, hack1 doesn't look particularly remarkable. It's simply a theorem about changing bound variables. What's unusual is its axiom usage:
MM> sh tr hack1 /ax /ma ax-*
Statement "hack1" assumes the following axioms ($a statements):
ax-mp ax-1 ax-2 ax-3
We proved a theorem about changing bound variables from propositional logic alone, which shouldn't be possible. This observation led me to investigate further. The immediate line of thought was: "Well, df-hack is conservative over a larger set of axioms, it's obviously not conservative over propositional logic alone". Not so fast. If we follow this reasoning then there are more results that go wrong.
First of all, this means that any definition is potentially not conservative, and we should be really careful in determining which definition is conservative over which axiom system. If we expand our axiom system to include predicate logic with equality and ax-12 then we can prove:
${
$d t x z $. $d t y z $.
$( Proof of ~ ax-8 with DV conditions, without using ~ ax-8 . (Contributed
by GG, 1-Jul-2025.) $)
ax8vv $p |- ( x = y -> ( x e. z -> y e. z ) ) $=
( vt weq wel equtr wal ax12v hack1 19.21bi syl6 com3r equcoms com12 ax6ev
wi syld exlimiiv ) DAEZABEZACFZBCFZQZQDTUADBEZUDDABGUEUDQADUEADEZUDUFUDQB
DUFUBBDEZUCUFUBUFUBQAHZUGUCQZUBADIUHUIBDCBAJKLMNONRDAPS $.
$}
MM> sh tr ax8vv /ax /ma ax-*
Statement "ax8vv" assumes the following axioms ($a statements):
ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-12
The statement ax8vv is a version of ax-8 with DV conditions. As confirmed by Mario and Benoît in https://groups.google.com/g/metamath/c/ENg8Hdvlpn4 ax8vv is independent from the axioms listed by above, so this proves that df-hack is not even conservative over predicate logic (to be precise, the proof uses the weaker ax6v and ax12v, which don't require ax-13).
The other relevant observation is that df-hack is not eliminable either. If you unwrap the definition then the proof of ax8vv will break, and of course it must break because ax8vv cannot be proved from the listed set of axioms.
-------------------------------------------------------------------------------------------------------------------------------------------
Above, I provided a soundess issue by adding a new definition, not present in the database. However, the issue should hold for pretty much any definition with dummy variables, so we should be able to find a hack using an already existing one. There are many definitions we can choose from. I'm going to pick df-in because it's simple and it's probably one of the least controversial ones in mathematics (most school textbooks have it).
Long story short, from df-in we can prove:
${
$d x B $. $d y B $.
$( One direction of ~ eleq1w with DV conditions. This proof does not use
~ ax-8 . (Contributed by GG, 1-Jul-2025.) $)
ax8bvv $p |- ( x = y -> ( x e. B -> y e. B ) ) $=
( cv wcel wa wi weq ax8bvv-lem9 anidm wn pm2.24 com3l sylnbi simp1r mpcom
3exp ja ) ADCEZSFZBDCEZUAFZGABHZSUAGZABCCITUBUCUDGZTSUESJSSKUCUASUCUAGLMN
UBUCSUAUAUAUCSOQRP $.
$}
MM> sh tr ax8bvv /ax /ma ax-*
Statement "ax8bvv" assumes the following axioms ($a statements):
ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-12 ax-ext
Theorem ax8bvv is a version of ax8vv that replaces a setvar with a class variable. The axiom usage is higher than the one of ax8vv, since we have to unwrap class abstractions, which adds ax-9 and ax-ext. My understanding it that the addition of those axioms shouldn't be sufficient to prove ax8bvv, because ax-9 is already proved to not be so and ax-ext has equality as consequent, which is interpreted as the always true relation in Benoit's paper (therefore proving that it exists a model where all of listed axioms are true and ax8bvv is false).
I should mention that ax8bvv uses also df-clab and df-cleq (note that it does not use df-clel, which was the historically guilty definition to prove ax-8). However, df-cleq has been revised in 2023 to solve the known conservativity issues and the topic has been put to bed ever since. If df-cleq and df-clab are responsable for the proof of ax8bvv, it means they are still not conservative despite the revision. According to this comment, the update provideded conservativity of {df-clab, df-cleq, df-clel} over {ax-mp, ax-gen, ax-1--ax-7, ax-ext}.
These results suggest that there might be a flaw in the metamath definition system, since the known issues regarding definitions of class abstractions are applicable even to more standard ones.
----------------------------------------------------------------------------------------------------------------------------------------
Before talking about the diganosis and a proposed solution, there is more information that I would like to share. After noticing the issue, I thought: "Does this hack work in MM1?". The examination of this topic becomes more interesting in light of MM0 premises and mechanisms. First of all, MM0 has definitions in the specification, which means that it has fewer "excuses". The MM0 language is supposed to provide conservativity and eliminability by design. There is no "well, technically every definition is an axiom in the MM specification" or "a definition might be conservative over a set of axioms, but not another", no no, definitions in MM0 should not affect the user's capability of proving statements in the primitive language because that's the job of the axioms (as stated here). Definitions should serve the purpose of making expressions shorter and practical to use. The MM0 language promises users to be able to study any kind of logical system and subsytem that can be expressed in the form of axioms and rules of inferences (source: youtube tutorial). Therefore, for any given axiomatic system that I choose in MM0, I should be guaranteed that definitions do not affect my capability of proving statements in the primitive language. Moreover, the MM0 environment is supposed to have a mechanism to verify the verifier, so an exploit of that mechanism would be informationally valuable.
It was agreed that the system discussed in https://groups.google.com/g/metamath/c/ENg8Hdvlpn4/m/9NSC1Sk9AgAJ and https://github.com/digama0/mm0/pull/149 is a fair translation of the set.mm system. It is very similar to the one used in peano.mm0 (with only essential differences, like using "set" instead of "nat") and it's identical to the set.mm formalization without overloading.
To prove ax8vvv, I used:
delimiter $ ( ) ~ { } $;
strict provable sort wff;
term wi (ph ps: wff): wff; infixr wi: $->$ prec 25;
term wn (ph: wff): wff; prefix wn: $~$ prec 41;
axiom ax_1 (ph ps: wff): $ ph -> ps -> ph $;
axiom ax_2 (ph ps ch: wff): $ (ph -> ps -> ch) -> (ph -> ps) -> ph -> ch $;
axiom ax_3 (ph ps: wff): $ (~ph -> ~ps) -> ps -> ph $;
axiom ax_mp (ph ps: wff): $ ph $ > $ ph -> ps $ > $ ps $;
def wb (ph ps: wff): wff = $ ~((ph -> ps) -> ~(ps -> ph)) $;
infixl wb: $<->$ prec 20;
pure sort set;
term wal {x: set} (ph: wff x): wff; prefix wal: $A.$ prec 41;
def wex {x: set} (ph: wff x): wff = $ ~(A. x ~ph) $;
prefix wex: $E.$ prec 41;
axiom ax_gen {x: set} (ph: wff x): $ ph $ > $ A. x ph $;
axiom ax_4 {x: set} (ph ps: wff x): $ A. x (ph -> ps) -> A. x ph -> A. x ps $;
axiom ax_5 {x: set} (ph: wff): $ ph -> A. x ph $;
term weq (a b: set): wff; infixl weq: $=s$ prec 50;
term wel (a b: set): wff; infixl wel: $es.$ prec 50;
axiom ax_6 {x: set} (a: set): $ E. x x =s a $;
axiom ax_7 (a b c: set): $ a =s b -> a =s c -> b =s c $;
axiom ax_12 {x: set} (a: set) (ph: wff x): $ x =s a -> ph -> A. x (x =s a -> ph) $;
I added the definition:
def hack (x y: set) {.t: set}: wff = $ A. t (t =s x -> t es. y) $;
prefix hack: $H.$ prec 41;
Which allowed me to derive:
pub theorem ax8vvv {a b: set} (c: set): $ a =s b -> a es. c -> b es. c $=
'(exlimiiv (syl (com12 ax8vvv_lem6) eqcom) (! ax_6 x));
In practice, ax8vvv is a version of ax-8 with all setvars disjoint from one another. This database doesn't use df-clel, df-cleq or any historically controversial definition. It's a clean proof of ax8vvv from predicate logic with equality and ax12v (the ax_12 version used in MM0 translates to ax12v in metamath, because of the MM0 DV rules with bound variables). As stated above, the creation of such proof shouldn't be possible.
----------------------------------------------------------------------------------------------------------------------------------------------
Now the second proof. The derivation of ax8bvv from df-in. The axiomatic setting makes this case even more interesting.
delimiter $ ( [ { ~ $ $ } ] ) $;
strict provable sort wff;
term wi (ph ps: wff): wff; infixr wi: $->$ prec 25;
term wn (ph: wff): wff; prefix wn: $~$ prec 41;
axiom ax_1 (ph ps: wff): $ ph -> ps -> ph $;
axiom ax_2 (ph ps ch: wff): $ (ph -> ps -> ch) -> (ph -> ps) -> ph -> ch $;
axiom ax_3 (ph ps: wff): $ (~ph -> ~ps) -> ps -> ph $;
axiom ax_mp (ph ps: wff): $ ph $ > $ ph -> ps $ > $ ps $;
def wb (ph ps: wff): wff = $ ~((ph -> ps) -> ~(ps -> ph)) $;
infixl wb: $<->$ prec 20;
def wa (ph ps: wff): wff = $ ~(ph -> ~ps) $;
infixl wa: $/\$ prec 34;
pure sort set;
term wal {x: set} (ph: wff x): wff; prefix wal: $A.$ prec 41;
def wex {x: set} (ph: wff x): wff = $ ~(A. x ~ph) $;
prefix wex: $E.$ prec 41;
axiom ax_gen {x: set} (ph: wff x): $ ph $ > $ A. x ph $;
axiom ax_4 {x: set} (ph ps: wff x): $ A. x (ph -> ps) -> A. x ph -> A. x ps $;
axiom ax_5 {x: set} (ph: wff): $ ph -> A. x ph $;
term weq (a b: set): wff; infixl weq: $=s$ prec 50;
term wel (a b: set): wff; infixl wel: $es.$ prec 50;
axiom ax_6 {x: set} (a: set): $ E. x x =s a $;
axiom ax_7 (a b c: set): $ a =s b -> a =s c -> b =s c $;
axiom ax_12 {x: set} (a: set) (ph: wff x): $ x =s a -> ph -> A. x (x =s a -> ph) $;
def sb (a: set) {x .y: set} (ph: wff x): wff = $ A. y (y =s a -> A. x (x =s y -> ph)) $;
notation sb (a: set) {x: set} (ph: wff x): wff = ($[$:41) a ($/$:0) x ($]$:0) ph;
strict sort class;
term cab {x: set} (ph: wff x): class;
term welc (a: set) (A: class): wff; infixl welc: $ec.$ prec 50;
notation cab {x: set} (ph: wff x): class = (${$:max) x ($|$:0) ph ($}$:0);
axiom ax_clab (a: set) {x: set} (ph: wff x): $ a ec. {x | ph} <-> [a / x] ph $;
def wceq {.x: set} (A B: class): wff = $ A. x (x ec. A <-> x ec. B) $;
infixl wceq: $=$ prec 50;
To the above system, I added the following definition:
--| `A i^i B` is the intersection of sets `A` and `B`.
def Inter (A B: class) {.x: set}: class = $ {x | x ec. A /\ x ec. B} $;
infixl Inter: $i^i$ prec 70;
Inter is the same definition used in peano.mm0. There is the minor notation difference about using "ec." instead of "e.", because peano.mm0 uses "e." in elab, while set.mm0 uses "ec." in ax_clab, so our notation should follow set.mm0 (also "e." is used for df_clel in set.mm0, while peano.mm0 does not define it).
From the above setting, we can prove:
pub theorem ax8bvv {a b: set} (A: class): $ a =s b -> a ec. A -> b ec. A $=
'(syld (syld (a1i anr) ax8bvv_lem8) (a1i anl));
The resulting ax8bvv has a class replacing a setvar. Interestingly, ax8bvv looks very similar to ax_8b, which is stated as an axiom in set.mm0:
axiom ax_8b (a b: set) (A: class): $ a =s b -> a ec. A -> b ec. A $;
The fact that ax8bvv uses neither ax_8 nor ax_8b is a sign that something is wrong. The axioms needed for ax8bvv are: ax_1, ax_2, ax_3, ax_4, ax_gen, ax_5, ax_6 (which is ax6v), ax_7, ax_12 (which is ax12v), ax_clab. The latter is identical to the df-clab in set.mm and we could even argue that the MM0 version is "safer" because it does not overload the membership relation.
Both databases have been verified with the following commands:
./mm0-rs compile -W ax8vvv.mm1 ax8vvv.mmb
./mm0-c ax8vvv.mmb < ax8vvv.mm0
./mm0-rs compile -W ax8bvv.mm1 ax8bvv.mmb
./mm0-c ax8bvv.mmb < ax8bvv.mm0
These are exactly the CI commands of the MM0 repository, used to verify the correctness of peano.mm1 and others. The verification yields no errors and no warnings for both of my databses. So I believe we have an exploit.
---------------------------------------------------------------------------------------------------------------------------------------------
Diagnosis and approach towards a fix.
I'd like to start from an observation. The property of being a definition is not an absolute property, it is a relative property. It is relative to the axiomatic system we're using. This is true for theorems as well. In Łukasiewicz (L₁)-system the expression "ψ→(¬ψ→φ)" is an axiom, while it's a theorem in Łukasiewicz (L₃)-system. Similarly, df-or is a definition in classical logic, but it's an axiom in intuitionistic one. In this sense, theorems and definitions have a similar nature, and I believe we should reflect that on the proof language we're using.
My diagnosis for the exploit is the following: every provable statement (statements starting with "|-") should be seen either as an axiom or as a theorem, no exception. What I mean is that definitions should be viewed as "theorems in disguise" that hold an axiom usage. When we write df-in, we should ask: "How does this definition translate to the primitive language?". The answer is that it translates to its own justification theorem, which in this case is injust. In fact, within the system, their behaviour is the same. We can use both statements to change bound variables and we can use both statements to prove the same results. I would argue that not only the justification theorem provides a soundness argument for the corresponding definition, but in a sense, a definition is its own justification theorem. Therefore, if we ask which axiom usage should a definition hold, I believe the answer is that it should hold the one of its justification theorem.
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).
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).
So for df-in, a proposal might look like this:
${
$d x A $. $d x B $. $d y A $. $d y B $. $d z x $. $d z y $. $d z A $.
$d z B $.
$( Define the intersection of two classes. (Contributed by NM, 29-Apr-1994.) $)
df-in $k |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) } $=
( vz cv wcel wa cab weq eleq1w anbi12d cbvabv eqtri ) AFZCGZODGZHZAIEFZCG
ZSDGZHZEIBFZCGZUCDGZHZBIRUBAEAEJPTQUAAECKAEDKLMUBUFEBEBJTUDUAUEEBCKEBDKLM
N $.
$}
Where the proof object is the proof of injust.
I'm sure people more knowledgeable than me will be able to point out flaws in this proposal. In reality, this is meant to be an indication towards what I believe to be the right direction, rather than a carefully crafted solution.
You might be skeptical of "providing a proof that does not conclude the statement itself", but this is already done in metamath. If you think about it, every axiom in set.mm is accompanied by a proof that is well formed, and such proof is shown in the metamath web pages. There is no specification difference between a "Detailed syntax breakdown" and a proof of a theorem, they are both just proofs from a metamath point of view.
So we could generalize metamath statements as follows:
axiom $a = statement with a proof that it is well formed.
theorem $p = statment with a proof of its expression.
definition $k = statement with a proof of its justification.
The proposed system would also help to verify definition correctness. The current rules for definitions are:
''''''''''
1. The expression must be a biconditional or an equality (i.e. its root-symbol must be ↔ or =). If the proposed definition passes this first rule, we then define its definiendum as its left hand side (LHS) and its definiens as its right hand side (RHS). We define the *defined symbol* as the root-symbol of the LHS. We define a *dummy variable* as a variable occurring in the RHS but not in the LHS. Note that the "root-symbol" is the root of the considered tree; it need not correspond to a single token in the database (e.g., see w3o 1083 or wsb 2060).
2. The defined expression must not appear in any statement between its syntax axiom ($a wff ) and its definition, and the defined expression must not be used in its definiens. See df-3an 1086 for an example where the same symbol is used in different ways (this is allowed).
3. No two variables occurring in the LHS may share a disjoint variable (DV) condition.
4. All dummy variables are required to be disjoint from any other (dummy or not) variable occurring in this labeled expression.
5. Either
(a) there must be no non-setvar dummy variables, or
(b) there must be a justification theorem.
6. One of the following must be true:
(a) there must be no setvar dummy variables,
(b) there must be a justification theorem as described in rule 5, or
(c) if there are setvar dummy variables, every one must not be free.
''''''''''
These rules are quite complex and a verifier checking them is indeed prone to bugs, as already shown in mmj2. The revised system would simplify them as follows:
''''''''''
1. The expression must be a biconditional or an equality (i.e. its root-symbol must be ↔ or =). If the proposed definition passes this first rule, we then define its definiendum as its left hand side (LHS) and its definiens as its right hand side (RHS). We define the *defined symbol* as the root-symbol of the LHS. We define a *dummy variable* as a variable occurring in the RHS but not in the LHS. Note that the "root-symbol" is the root of the considered tree; it need not correspond to a single token in the database (e.g., see w3o 1083 or wsb 2060).
2. The defined expression must not appear in any statement between its syntax axiom ($a wff ) and its definition, and the defined expression must not be used in its definiens. See df-3an 1086 for an example where the same symbol is used in different ways (this is allowed).
3. No two variables occurring in the LHS may share a disjoint variable (DV) condition.
4. The definition must have a provable justification theorem.
''''''''''
This removes all rules about free and bound variables, which aligns with the metamath philosophy of not having any notion of what a bound variable is in the first place. We could still keep some additional rules, but they would become stylistic rather than correctness critical. For example, rule 4 about DV conditions is not necessary (in my system), the DV conditions of the definition are inherited from the DV conditions of the justification theorem. So, one could add dfid3 as a definition of the identity relation and it would be technically fine. The caveat is that the justification of dfid3 uses ax-13 and therefore every theorem depending on it would also use ax-13. Therefore it's better to define the identity relation with df-id (which has DVs between x and y) simply because we want to reduce axiom usage as much as possible. But the point is that correcness would be no longer at risk. Lack of DVs in a definition wouldn't imply proofs of false, as long as the justification theorem is provable.
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:
$( Define biconditional. (Contributed by NM, 27-Dec-1992.) $)
df-bi $k |- -. ( ( ( ph <-> ps ) -> -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) )
-> -. ( -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) -> ( ph <-> ps ) ) ) $= ( bijust ) ABC $.
In general, every statement has its own justification theorem. For example, the justification theorem of:
sstr2 $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.
In practice, this also means that the creator of a definition could verify in advance the correctness of its expression directly with the metamath.exe proof verification. Adding a definition would be no more risky than adding a theorem, and episodes like https://github.com/metamath/set.mm/pull/3334 would never happen.
In my opinion, viewing definitions in this light is very elegant and it solves multiple issues in one shot. I'm looking forward to hear your replies. If I am wrong (and I might be), be kind to me.
My diagnosis for the exploit is the following: every provable statement (statements starting with "|-") should be seen either as an axiom or as a theorem, no exception. What I mean is that definitions should be viewed as "theorems in disguise" that hold an axiom usage. When we write df-in, we should ask: "How does this definition translate to the primitive language?". The answer is that it translates to its own justification theorem, which in this case is injust. In fact, within the system, their behaviour is the same. We can use both statements to change bound variables and we can use both statements to prove the same results. I would argue that not only the justification theorem provides a soundness argument for the corresponding definition, but in a sense, a definition is its own justification theorem. Therefore, if we ask which axiom usage should a definition hold, I believe the answer is that it should hold the one of its justification theorem.
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).
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).
So for df-in, a proposal might look like this:
${
$d x A $. $d x B $. $d y A $. $d y B $. $d z x $. $d z y $. $d z A $.
$d z B $.
$( Define the intersection of two classes. (Contributed by NM, 29-Apr-1994.) $)
df-in $k |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) } $=
( vz cv wcel wa cab weq eleq1w anbi12d cbvabv eqtri ) AFZCGZODGZHZAIEFZCG
ZSDGZHZEIBFZCGZUCDGZHZBIRUBAEAEJPTQUAAECKAEDKLMUBUFEBEBJTUDUAUEEBCKEBDKLM
N $.
$}
Where the proof object is the proof of injust.
I'm sure people more knowledgeable than me will be able to point out flaws in this proposal. In reality, this is meant to be an indication towards what I believe to be the right direction, rather than a carefully crafted solution.
You might be skeptical of "providing a proof that does not conclude the statement itself", but this is already done in metamath. If you think about it, every axiom in set.mm is accompanied by a proof that is well formed, and such proof is shown in the metamath web pages. There is no specification difference between a "Detailed syntax breakdown" and a proof of a theorem, they are both just proofs from a metamath point of view.
So we could generalize metamath statements as follows:
axiom $a = statement with a proof that it is well formed.
theorem $p = statment with a proof of its expression.
definition $k = statement with a proof of its justification.
The proposed system would also help to verify definition correctness. The current rules for definitions are:
''''''''''
1. The expression must be a biconditional or an equality (i.e. its root-symbol must be ↔ or =). If the proposed definition passes this first rule, we then define its definiendum as its left hand side (LHS) and its definiens as its right hand side (RHS). We define the *defined symbol* as the root-symbol of the LHS. We define a *dummy variable* as a variable occurring in the RHS but not in the LHS. Note that the "root-symbol" is the root of the considered tree; it need not correspond to a single token in the database (e.g., see w3o 1083 or wsb 2060).
2. The defined expression must not appear in any statement between its syntax axiom ($a wff ) and its definition, and the defined expression must not be used in its definiens. See df-3an 1086 for an example where the same symbol is used in different ways (this is allowed).
3. No two variables occurring in the LHS may share a disjoint variable (DV) condition.
4. All dummy variables are required to be disjoint from any other (dummy or not) variable occurring in this labeled expression.
5. Either
(a) there must be no non-setvar dummy variables, or
(b) there must be a justification theorem.
6. One of the following must be true:
(a) there must be no setvar dummy variables,
(b) there must be a justification theorem as described in rule 5, or
(c) if there are setvar dummy variables, every one must not be free.
''''''''''
These rules are quite complex and a verifier checking them is indeed prone to bugs, as already shown in mmj2. The revised system would simplify them as follows:
''''''''''
1. The expression must be a biconditional or an equality (i.e. its root-symbol must be ↔ or =). If the proposed definition passes this first rule, we then define its definiendum as its left hand side (LHS) and its definiens as its right hand side (RHS). We define the *defined symbol* as the root-symbol of the LHS. We define a *dummy variable* as a variable occurring in the RHS but not in the LHS. Note that the "root-symbol" is the root of the considered tree; it need not correspond to a single token in the database (e.g., see w3o 1083 or wsb 2060).
2. The defined expression must not appear in any statement between its syntax axiom ($a wff ) and its definition, and the defined expression must not be used in its definiens. See df-3an 1086 for an example where the same symbol is used in different ways (this is allowed).
3. No two variables occurring in the LHS may share a disjoint variable (DV) condition.
4. The definition must have a provable justification theorem.
''''''''''
This removes all rules about free and bound variables, which aligns with the metamath philosophy of not having any notion of what a bound variable is in the first place. We could still keep some additional rules, but they would become stylistic rather than correctness critical. For example, rule 4 about DV conditions is not necessary (in my system), the DV conditions of the definition are inherited from the DV conditions of the justification theorem. So, one could add dfid3 as a definition of the identity relation and it would be technically fine. The caveat is that the justification of dfid3 uses ax-13 and therefore every theorem depending on it would also use ax-13. Therefore it's better to define the identity relation with df-id (which has DVs between x and y) simply because we want to reduce axiom usage as much as possible. But the point is that correcness would be no longer at risk. Lack of DVs in a definition wouldn't imply proofs of false, as long as the justification theorem is provable.
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:
$( Define biconditional. (Contributed by NM, 27-Dec-1992.) $)
df-bi $k |- -. ( ( ( ph <-> ps ) -> -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) )
-> -. ( -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) -> ( ph <-> ps ) ) ) $= ( bijust ) ABC $.
In general, every statement has its own justification theorem. For example, the justification theorem of:
sstr2 $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.
In practice, this also means that the creator of a definition could verify in advance the correctness of its expression directly with the metamath.exe proof verification. Adding a definition would be no more risky than adding a theorem, and episodes like https://github.com/metamath/set.mm/pull/3334 would never happen.
In my opinion, viewing definitions in this light is very elegant and it solves multiple issues in one shot. I'm looking forward to hear your replies. If I am wrong (and I might be), be kind to me.
savask
Jul 13, 2025, 4:34:26 AMJul 13
to Metamath
A really interesting post. All the intricacies of the above examples are way over my head, so sorry if this is a dumb question: can you prove False with your method? Or our definitions conventions guarantee that the extended axiom system is consistent, given that the original system was? If the latter is the case, does that mean that the flaw you found will mainly influence the work on trying to minimize axiom usage, especially predicate calculus axioms?
It would be nice if this could be resolved by leaving metamath standard as is, and, for instance, improving the definition checker in mmj2 or metamath-knife. Seems like adding the $k token would make all the verifiers we wrote over the years obsolete.
Gino Giotto
Jul 13, 2025, 5:35:51 AMJul 13
to Metamath
>
can you prove False with your method?
I think the answer is no, you cannot prove False from sound definitions. The reason I think so is because definitions that follow the convention rules always have a provable justification theorem inside the full axiomatic system of set.mm. To prove false, you have to show that your definition has a justification theorem that is stronger than what set.mm allows. This is the way proofs of false have been produced historically so far, like I did in https://github.com/metamath/set.mm/pull/4909. So, if you only care about set.mm as a whole, then this is an axiom usage issue, but if you care about subsystems of set.mm (or non-set.mm systems) then it becomes a bigger problem.
>
It would be nice if this could be resolved by leaving metamath standard as is, and, for instance, improving the definition checker in mmj2 or metamath-knife. Seems like adding the $k token would make all the verifiers we wrote over the years obsolete.
Yeah , this is a problem. I guess the simplest solution is the first option then, which is to add the justification theorems as definition hypotheses. It's not super elegant, and in my eyes it fails the promise of absolute rigour of the metamath book, but it should work in practice.
Steven Nguyen
Jul 13, 2025, 9:35:04 AMJul 13
to meta...@googlegroups.com
This would be a really good idea if there weren't historical reasons.
I think ideally this is how it would go:
1. the definition checker generates $k proofs for all relevant definitions
2. the axioms of the $k proofs are propagated forward to theorems
3. $j usage would also check for axioms that would be used in $k proofs
This would be more elegant and rigorous than hypotheses
> --
> 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 metamath+u...@googlegroups.com.
> To view this discussion visit https://groups.google.com/d/msgid/metamath/1cabdb6f-4afe-49c9-bf17-b3eeeea40f7fn%40googlegroups.com.
I think ideally this is how it would go:
1. the definition checker generates $k proofs for all relevant definitions
2. the axioms of the $k proofs are propagated forward to theorems
3. $j usage would also check for axioms that would be used in $k proofs
This would be more elegant and rigorous than hypotheses
> 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 metamath+u...@googlegroups.com.
> To view this discussion visit https://groups.google.com/d/msgid/metamath/1cabdb6f-4afe-49c9-bf17-b3eeeea40f7fn%40googlegroups.com.
Jim Kingdon
Jul 13, 2025, 10:40:50 AMJul 13
to meta...@googlegroups.com
If I correctly understand the issue here, seems like the request is to
carry the axiom tracking from the justification theorem to usages of the
definition.
It doesn't appear to affect what we can prove, but given that we do seem
to often care about axiom usage, it seems like a plausible thing to
want. (I'm not sure I have an opinion about *how* this tracking would
work, but I'm not sure we would have to change a lot of things to make
it possible).
carry the axiom tracking from the justification theorem to usages of the
definition.
It doesn't appear to affect what we can prove, but given that we do seem
to often care about axiom usage, it seems like a plausible thing to
want. (I'm not sure I have an opinion about *how* this tracking would
work, but I'm not sure we would have to change a lot of things to make
it possible).
Mario Carneiro
Jul 17, 2025, 3:18:33 PMJul 17
to meta...@googlegroups.com
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:
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 <ginogiott...@gmail.com> 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).
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 $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.
Reply all
Reply to author
Forward
0 new messages