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.
On Wednesday, October 22, 2025 at 6:11:22 PM UTC-4 Matthew House wrote:
> 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/66ba47eb-e8e0-4bd0-a009-80aecf46480dn%40googlegroups.com.
