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/9842449900f4e54636d0fcb70c641bffOn Sun, Jul 13, 2025 at 9:29 AM Ludwig Maes <[email protected]> wrote: > 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, <[email protected]> wrote: > >> [email protected] >> <https://groups.google.com/forum/?utm_source=digest&utm_medium=email#!forum/metamath/topics> >> Google >> Groups >> <https://groups.google.com/forum/?utm_source=digest&utm_medium=email/#!overview> >> [image: >> Google Groups Logo] >> <https://groups.google.com/forum/?utm_source=digest&utm_medium=email/#!overview> >> Topic digest >> View all topics >> <https://groups.google.com/forum/?utm_source=digest&utm_medium=email#!forum/metamath/topics> >> >> - A flaw in the metamath definition system? >> <#m_-5005903295455311652_m_3526486109382263806_group_thread_0> - 1 >> Update >> >> A flaw in the metamath definition system? >> <http://groups.google.com/group/metamath/t/597bcbf717da47d5?utm_source=digest&utm_medium=email> >> Gino Giotto <[email protected]>: 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 <#m_-5005903295455311652_m_3526486109382263806_digest_top> >> You received this digest because you're subscribed to updates for this >> group. You can change your settings on the group membership page >> <https://groups.google.com/forum/?utm_source=digest&utm_medium=email#!forum/metamath/join> >> . >> To unsubscribe from this group and stop receiving emails from it send an >> email to [email protected]. >> > -- > 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/CAJ8SgH%3DORQUXXHG%2BRdBUhBMtJv8FvvwurMX7jTGBW6Vm1Kzwiw%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CAJ8SgH%3DORQUXXHG%2BRdBUhBMtJv8FvvwurMX7jTGBW6Vm1Kzwiw%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/CAAfCLnic2HaRiAWO684cQ%2B1NW3rpSYGa-xd34rPGk_rVQn9Sqg%40mail.gmail.com.
