Can ax-11 be rederived from its DV form without ax-13?

[Matthew House]

In set.mm, ax-11 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? If not, it would seem like we should create a new ax11v and have everything go through that, the same as ax6v and ax12v.

Matthew House

[Matthew House]

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?

[Matthew House]

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 makes it tricky to find a countermodel in general, but it's odd that I can't even prove that ax-5 is necessary.

[Matthew House]

I made a typo on that last bullet point: it should read that the proof could avoid all of ax-7, ax-10, ax11v, and ax-13.

Also, I mentioned alcomimw, but as written, it's not any stronger than ax11v. With ax11v + axc11r + ax-13, it's possible to come up with a similar "weak version" that suffices for all wff-free instances of ax-11, without needing the DV condition of alcomimw:

  ${
    $d x z w $.  $d y z w $.
    alcomfw2.1 $e |- F/ z ph $.
    alcomfw2.2 $e |- F/ w ph $.
    alcomfw2.3 $e |- F/ x ps $.
    alcomfw2.4 $e |- F/ y ps $.
    alcomfw2.5 $e |- ( ( x = z /\ y = w ) -> ( ph <-> ps ) ) $.
    $( Weak version of ~ alcom based on ~ ax11v and a double substitution. $)
    alcomfw2 $p |- ( A. x A. y ph <-> A. y A. x ph ) $= ? $.
  $}

The proof is to transform ( A. x A. y ph <-> A. z A. w ps ), swap the quantifiers with ax11v, and transform it back.