Re: [Metamath] Digest for metamath@googlegroups.com - 1 update in 1 topic

[Ludwig Maes]

1) Your message ends with an unfinished sentence, so I don't know how much more we are missing

2) Is it possible you simply eliminated an axiom (i.e. you discovered an axiom to be superfluous)?

3) I think 'exploit' is the correct term (since in the future people may wish to  build systems that rely on MM for verification of adversarial claims). Is there a log of previous 'exploits' that have been handled in MM?

On Sun, 13 Jul 2025 at 07:28, <meta...@googlegroups.com> wrote:

meta...@googlegroups.com

Google Groups

Topic digest
View all topics

• A flaw in the metamath definition system? - 1 Update

A flaw in the metamath definition system?

Gino Giotto <ginogiott...@gmail.com>: Jul 12 04:42PM -0700 This is a topic I have been wondering for a while, and it's the main motivation behind the question in this conversation <https://groups.google.com/g/metamath/c/ENg8Hdvlpn4>. 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 <https://github.com/GinoGiotto/set.mm/tree/ax8vv> (commit f03b065 <https://github.com/GinoGiotto/set.mm/commit/f03b065bb99d6f4582f24daeb00e6ecfe55dc9fe>), while the MM1 databases are available here <https://github.com/GinoGiotto/mm1_test>. 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 <https://us.metamath.org/mpeuni/df-in.html> 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 <https://github.com/metamath/set.mm/pull/3389> 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 <https://github.com/metamath/set.mm/pull/3199#issuecomment-1676095106>, 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 <https://github.com/metamath/set.mm/pull/3199#issuecomment-1676058428>). 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 <https://github.com/tirix/set-noov.mm>.   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

Back to top

You received this digest because you're subscribed to updates for this group. You can change your settings on the group membership page. To unsubscribe from this group and stop receiving emails from it send an email to metamath+u...@googlegroups.com.

[Steven Nguyen]

1. The message isn't cut off in the actual post, I think it's something with the digest
2. No. The exploit is that definitions provide a way to change bound variables without using certain axioms. For example, {x} = {y|y = x} provides {y|y=x} = {z|z=x}. This exploit is not achievable without the definitions + definitions that cause extra things to be provable are axioms.
3. Not really that I'm aware of, but I do happen to have a list of proofs of false: https://gist.github.com/icecream17/9842449900f4e54636d0fcb70c641bff

--
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/CAJ8SgH%3DORQUXXHG%2BRdBUhBMtJv8FvvwurMX7jTGBW6Vm1Kzwiw%40mail.gmail.com.