> 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
On Thursday, June 5, 2025 at 10:33:17 AM UTC+2 [email protected] wrote:
> > 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/f1636dac-35b4-4aa2-aa46-8ccd5d5ebe71n%40googlegroups.com.
