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
<https://us.metamath.org/mpeuni/ax-8.html> 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
<https://groups.google.com/g/metamath/c/um0Z6o9A1hg/m/w6qa5JC2AwAJ> showing
that
the full ax-8 <https://us.metamath.org/mpeuni/ax-8.html> (without DV
conditions) is independent of the above axioms, and that the weaker ax8v
<https://us.metamath.org/mpeuni/ax8v.html> is independent as well (appendix
B.9). We know that ax-8 <https://us.metamath.org/mpeuni/ax-8.html> can be
recovered from ax8v1 <https://us.metamath.org/mpeuni/ax8v1.html> and ax8v2
<https://us.metamath.org/mpeuni/ax8v2.html>, as shown in the proof of ax8
<https://us.metamath.org/mpeuni/ax8.html>.
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
<https://us.metamath.org/mpeuni/ax12v.html> 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
<https://us.metamath.org/mpeuni/ax12v.html>, so I guess either one can be
used?
--
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/2d9ea442-5519-465e-b234-3affa86e248an%40googlegroups.com.
