> 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
<https://github.com/metamath/set.mm/pull/3375#discussion_r1292485886>,
df-clab should be conservative, and according to this comment
<https://github.com/metamath/set.mm/pull/3199#issuecomment-1676095106>,
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?
--
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/9ec7a76e-b3e4-433a-bd96-05c03ad583b6n%40googlegroups.com.
