This has turned out to be a much harder problem than I'd initially imagined. In an attempt to obtain a negative result, I've written up a countermodel generator that's able to prove that most of the set.mm axioms are mutually independent: in particular, it proves ax-mp, ax-1 to ax-3, ax-gen, ax-4 to ax-9, and ax-12 are each independent from the rest of ax-mp to ax-13. But it can't fully prove the independence of ax-10, ax-11, and ax-13, nor can it prove the independence of ax-11 from ax11v.
At least it's gotten me a few partial results. Suppose that ax-11 is provable from ax11v + the rest of the axioms. Then: - The proof requires all of ax-mp, ax-1, ax-2, ax-3, ax-gen, ax-4, ax-6, and ax-12. - Either the proof requires ax-5, or the proof requires both ax-10 and ax11v. - The proof might be able to avoid all of ax-5, ax-7, and ax-13. - The proof might be able to avoid all of ax-5, ax-10, ax11v, and ax-13. The existence of alcomimw <https://us.metamath.org/mpeuni/alcomimw.html> makes it tricky to find a countermodel in general, but it's odd that I can't even prove that ax-5 is necessary. On Tuesday, October 14, 2025 at 1:00:28 PM UTC-4 Matthew House wrote: > Actually, I'm not even sure if the ax11v → ax-11 rederivation can be > performed with access to ax-13. The usual approach with distinctors runs > into |- ( -. A. y y = x -> F/ y A. x A. y ph ), which isn't trivial with > ax11v. The obvious idea would be to use a proper substitution to change the > variable and then apply ax11v, but the proper substitution itself would > require the full ax-11 to move through the quantifier. Perhaps there's a > more clever kind of substitution that would work? > > On Tuesday, October 14, 2025 at 11:00:29 AM UTC-4 Matthew House wrote: > >> In set.mm, ax-11 <https://us.metamath.org/mpeuni/ax-11.html> is written >> as |- ( A. x A. y ph -> A. y A. x ph ), with no DV restrictions between x >> and y. Can it be derived as a theorem from the weaker form with the >> additional restriction $d x y, without using ax-13 >> <https://us.metamath.org/mpeuni/ax-13.html>? If not, it would seem like >> we should create a new ax11v and have everything go through that, the same >> as ax6v <https://us.metamath.org/mpeuni/ax6v.html> and ax12v >> <https://us.metamath.org/mpeuni/ax12v.html>. >> >> Matthew House >> > -- 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/b7cef914-4cc0-4866-9a00-8b4a668a08d2n%40googlegroups.com.
