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_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_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.
