On Tue, Jun 3, 2025 at 4:00 AM Gino Giotto <[email protected]> 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 > <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? > 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 > <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. > 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. -- 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/CAFXXJSunnXGyeHBJfMVRwpexkT279u4fw_Ayb%2B1qR-nwxFF4HA%40mail.gmail.com.
