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 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 <https://us.metamath.org/mpeuni/injust.html>. 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 <https://github.com/GinoGiotto/mm1_test/blob/main/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 <https://us.metamath.org/mpeuni/dfid3.html> 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 <https://us.metamath.org/mpeuni/df-id.html> (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 <https://us.metamath.org/mpeuni/sstr2.html> $p |- ( A C_ B -> ( B C_ C -> A C_ C ) ) $. is: ${ $d A x $. $d B x $. $d B y $. $d C y $. $d A z $. $d C z $. sstr2just $p |- ( A. x ( x e. A -> x e. B ) -> ( A. y ( y e. B -> y e. C ) -> A. z ( z e. A -> z e. C ) ) ) $. $} And here we can see another reason why the current system is flawed. The current proof of sstr2 uses axioms up to ax-4, because it is proved with: sstr2just_wrong $p |- ( A. x ( x e. A -> x e. B ) -> ( A. x ( x e. B -> x e. C ) -> A. x ( x e. A -> x e. C ) ) ) $. The incorrect justification can be proved from al2imi and imim1 alone. However, the correct justification is sstr2just, because we can use sstr2 to change bound variables and we can prove sstr2just from sstr2 using propositional logic alone (while we cannot use sstr2just_wrong to change bound vars). Therefore, sstr2 should hold the axiom usage of sstr2just, which is higher than the one it currently has. 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. -- 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/f334fc81-8ea4-496e-92b2-b6b8be9b43fen%40googlegroups.com.
