Question about the independence of a statement

[Gino Giotto]

Consider the following set.mm axioms:

${
    min $e |- ph $.
    maj $e |- ( ph -> ps ) $.
    ax-mp $a |- ps $.
$}

ax-1 $a |- ( ph -> ( ps -> ph ) ) $.

ax-2 $a |- ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) $.

ax-3 $a |- ( ( -. ph -> -. ps ) -> ( ps -> ph ) ) $.

${
    ax-gen.1 $e |- ph $.
    ax-gen $a |- A. x ph $.
$}

ax-4 $a |- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) ) $.

${
    $d x ph $.
    ax-5 $a |- ( ph -> A. x ph ) $.
$}

${

    $d x y $.
    ax6v $a |- -. A. x -. x = y $.
$}

ax-7 $a |- ( x = y -> ( x = z -> y = z ) ) $.

${

    $d x y $.  $d y ph $.
    ax12v $a |- ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) $.

$}

The question is whether the following statement can be proved from the above axioms:

${
    $d x y z $.

    ax8vvv $p |- ( x = y -> ( x e. z -> y e. z ) ) $= ? $.
$}

I named the statement ax8vvv since it's just a version of ax-8 with all setvars disjoint from one another. Of course, we are allowed to use the syntactic statement wel $a wff x e. y $.

A few years ago, Benoît published a paper showing that the full ax-8 (without DV conditions) is independent of the above axioms, and that the weaker ax8v is independent as well (appendix B.9). We know that ax-8 can be recovered from ax8v1 and ax8v2, as shown in the proof of ax8.

However, the question of whether ax8vvv is provable in set.mm is not mentioned. This made me wonder whether the reason is that the answer is obvious (and I missed it), or not known.  

---------------------------------------------------------------------------------------------------------------------------------------------

Since I'm trying to get familiar with MM0/MM1, I'm going to restate the question in that language and ask whether it's formalized correctly:

delimiter $ ( ) ~ { } $;

strict provable sort wff;

term wi (ph ps: wff): wff; infixr wi: $->$ prec 25;

term wn (ph: wff): wff; prefix wn: $~$ prec 40;

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 $;

pure sort set;

term wal {x: set} (ph: wff x): wff; prefix wal: $A.$ prec 30;

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 40;

def wex {x: set} (ph: wff x): wff = $ ~(A. x ~ph) $;

prefix wex: $E.$ prec 30;

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 y: set} (ph: wff y): $ A. y ph -> A. x (x =s y -> ph) $;

theorem ax8vv {a b c: set}: $ a =s b -> a es. c -> b es. c $= '( _ );

Most of the above formalization is borrowed from set.mm0. I noticed that ax_12 in set.mm0 differs from ax12v in set.mm, which I assume is by design. I haven't checked whether the two versions are equivalent, but I see that peano.mm0 uses the set.mm version of ax12v, so I guess either one can be used?

[Mario Carneiro]

On Tue, Jun 3, 2025 at 4:00 AM Gino Giotto <ginogiott...@gmail.com> wrote: 

Since I'm trying to get familiar with MM0/MM1, I'm going to restate the question in that language and ask whether it's formalized correctly:

 

LGTM
 

Most of the above formalization is borrowed from set.mm0. I noticed that ax_12 in set.mm0 differs from ax12v in set.mm, which I assume is by design. I haven't checked whether the two versions are equivalent, but I see that peano.mm0 uses the set.mm version of ax12v, so I guess either one can be used?

I wouldn't assume it's by design. Unfortunately I forget the details of why there is a difference but I think there was some discussion about changing ax-12 (in set.mm) during this time period. The fact that MM0 has a different approach to distinctness than metamath (in particular: it doesn't care about bundled axioms and all theorems are always unbundled) means that some distinctions that matter for metamath are not relevant for MM0, so this may have been an attempt at simplification. I'm not sure I could say which one is better... But I'm reasonably confident in the one in peano.mm0 since that's the one that is actually in practical use, and one can say likewise for the one in set.mm (which can be verbatim translated to MM0 with equivalent consequences).

The question is whether the following statement can be proved from the above axioms:

${
    $d x y z $.

    ax8vvv $p |- ( x = y -> ( x e. z -> y e. z ) ) $= ? $.
$}

 

I named the statement ax8vvv since it's just a version of ax-8 with all setvars disjoint from one another. Of course, we are allowed to use the syntactic statement wel $a wff x e. y $.

A few years ago, Benoît published a paper showing that the full ax-8 (without DV conditions) is independent of the above axioms, and that the weaker ax8v is independent as well (appendix B.9). We know that ax-8 can be recovered from ax8v1 and ax8v2, as shown in the proof of ax8.

However, the question of whether ax8vvv is provable in set.mm is not mentioned. This made me wonder whether the reason is that the answer is obvious (and I missed it), or not known.  

The proof of independence of this statement is more or less in Benoit's paper. Appendix B.9 isn't the proof, the proof is done in section 3.1.7. In particular, all of the proofs in 3.1 are "object level" independence proofs, meaning that one may ignore the subtleties of metavariables substituting for variables substituting for values and collapse the metavariable layer. That means that one can feel free to assume DV conditions between any two set variables, because the countermodel will work even if we interpret the expression as a simple FOL statement, which validates all DV conditions on variables.

But now that I reread the proof I'm no longer sure this proof is correct. It uses a model of FOL without equality, and interprets equality instead as the always true relation, which clearly invalidates ax-8 or ax8vvv if the predicate is any non-constant function (e.g. x e. z iff x = 0 when the domain is {0,1}). But the trouble comes up in ax-12 (also known as subst in the paper), which is "A. x ( ph -> A. x ph )" after simplifying the equality away. Unlike ax-5 this has no DV conditions (the ones on y are gone because it's an arbitrary fresh variable), so the only way we could interpret this is if "A. x" is doing something weird. I believe it can be repaired by taking A. x to simply do nothing at all, "A. x ph" is interpreted as just "ph". This still satisfies all the modal axioms and subst; denot and genEq are trivial, and ALLEq is trivialized as well. So ax8vvv is independent.

[Gino Giotto]

>   I'm not sure I could say which one is better... But I'm reasonably confident in the one in peano.mm0 since that's the one that is actually in practical use, and one can say likewise for the one in set.mm (which can be verbatim translated to MM0 with equivalent consequences).

Perfect. I'm going to use the ax_12 version in peano.mm0 since it's the version I'm also more confident with (compared to the one in set.mm0). For my database, "nat" has to be changed to "set" and "=" becomes "=s" so:

axiom ax_12 {x: set} (a: set) (ph: wff x): $ x =s a -> ph -> A. x (x =s a -> ph) $;

> But now that I reread the proof I'm no longer sure this proof is correct. It uses a model of FOL without equality, and interprets equality instead as the always true relation, which clearly invalidates ax-8 or ax8vvv if the predicate is any non-constant function (e.g. x e. z iff x = 0 when the domain is {0,1}). But the trouble comes up in ax-12 (also known as subst in the paper), which is "A. x ( ph -> A. x ph )" after simplifying the equality away. Unlike ax-5 this has no DV conditions (the ones on y are gone because it's an arbitrary fresh variable), so the only way we could interpret this is if "A. x" is doing something weird. I believe it can be repaired by taking A. x to simply do nothing at all, "A. x ph" is interpreted as just "ph". This still satisfies all the modal axioms and subst; denot and genEq are trivial, and ALLEq is trivialized as well. So ax8vvv is independent.

Thank you so much for answering the question! The independence of ax8vvv is an important piece of information that I needed (btw I made a typo, I wrote "ax8vv" instead of "ax8vvv" when I translated it into MM1, sorry for that).

I'm going to elaborate the reason for this question soon...ish in a separate thread (spoiler: it's about definitions).

--------------------------------------------------------------------------------------------------------------------------------------------------------

It would also be useful to know whether ax8vvv is independent of the following set.mm axioms:

ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax6v ax-7 ax-9 ax12v ax-ext df-clab df-cleq

According to this comment, df-clab should be conservative, and according to this comment, df-cleq should be as well. So, I the question would be whether the addition of ax-9 and ax-ext changes the answer. The axiom of right equality ax-9 is already addressed in Benoît's paper, and since ax-ext has an equality relation as consequent, I guess it would evaluate to true, thus making the proof trivial?

[Benoit]

> But now that I reread the proof I'm no longer sure this proof is correct. It uses a model of FOL without equality, and interprets equality instead as the always true relation, which clearly invalidates ax-8 or ax8vvv if the predicate is any non-constant function (e.g. x e. z iff x = 0 when the domain is {0,1}). But the trouble comes up in ax-12 (also known as subst in the paper), which is "A. x ( ph -> A. x ph )" after simplifying the equality away. Unlike ax-5 this has no DV conditions (the ones on y are gone because it's an arbitrary fresh variable), so the only way we could interpret this is if "A. x" is doing something weird. I believe it can be repaired by taking A. x to simply do nothing at all, "A. x ph" is interpreted as just "ph". This still satisfies all the modal axioms and subst; denot and genEq are trivial, and ALLEq is trivialized as well. So ax8vvv is independent.

Mario: you're right about the problem and the fix: this was also noticed by the reviewer, and I gave basically the fix you propose (this was last year but I haven't updated the arXiv version yet, waiting for the final acceptance).

Benoît