Recent partial unbundling of ax-7, ax-8, ax-9

[Benoit]

Hi everyone,

I recently added to set.mm some weakenings of ax-7, ax-8, ax-9 in order to partially unbundle them.  I wrote a short note which is included in http://us2.metamath.org/mpeuni/mmnotes.txt (entry dated 7-Dec-2020) to explain these changes.  I'm copying it below for convenience (best viewed in fixed-width font).

Benoît

(7-Dec-2020) Partial unbundling of ax-7, ax-8, ax-9 (notes by Benoit Jubin)
---------------------------------------------------------------------------

This note discusses the recent partial unbundling of the axiom of
equality ax-7 and the predicate axioms ax-8 and ax-9 in set.mm.

The axiom of equality asserts that equality is a right-Euclidean binary relation
on variables:
  ax-7 |- ( x = y -> ( x = z -> y = z ) )

It can be weakened by adding a DV (disjoint variable) condition on x and y:
  ax7v |- ( x = y -> ( x = z -> y = z ) ) , DV(x,y)

and this scheme can itself be weakened by adding extra DV conditions:
  ax7v1 |- ( x = y -> ( x = z -> y = z ) ) , DV(x,y) , DV(x,z)
  ax7v2 |- ( x = y -> ( x = z -> y = z ) ) , DV(x,y) , DV(y,z)

We prove, in ax7, that either ax7v or the conjunction of ax7v1 and ax7v2
(together with earlier axioms) suffices to recover ax-7.  The proofs are
represented in the following simplified diagram (equid is reflexivity and
equcomiv is unbundled symmetry):

                 --> ax7v1 --> equid --
                /                      \
ax-7 --> ax7v --                        --> equcomiv --> ax7
                \                      /
                 --> ax7v2 ------------

The predicate axioms ax-8 and ax-9 can be similarly weakened, and the proofs are
actually simpler, now that the equality predicate has been proved to be an
equivalence relation on variables.  This is a general result.  If an n-ary
predicate P is added to the langugage, then one has to add the following n
predicate axioms for P:
  ax-P1 |- ( x = y -> ( P(x, z_2, ..., z_n) -> P(y, z_2, ..., z_n) ) )
  ...
  ax-Pn |- ( x = y -> ( P(z_1, ..., z_{n-1}, x) -> P(z_1, ..., z_{n-1}, y) ) )

Any of these axioms can be weakened by adding the DV condition DV(x,y), and it
is also sufficient to replace it by the conjunction of the two schemes:
  ax-Piv1 |- ( x = y ->
         ( P(z_1, ..., x, ..., z_n) -> P(z_1, ..., y, ..., z_n) ) ) , x fresh
  ax-Piv2 |- ( x = y ->
         ( P(z_1, ..., x, ..., z_n) -> P(z_1, ..., y, ..., z_n) ) ) , y fresh

where "fresh" means "disjoint from all other variables".  The proof is similar
to ax8 and ax9 and simply consists in introducing a fresh variable, say t, and
from
  |- ( x = t -> ( P(z_1, ..., x, ..., z_n) -> P(z_1, ..., t, ..., z_n) ) )
  |- ( t = y -> ( P(z_1, ..., t, ..., z_n) -> P(z_1, ..., y, ..., z_n) ) )
  |- ( x = y -> E. t ( x = t /\ t = y ) )
one can prove axPi.

Note that ax-7 can also be seen as the first predicate axiom for the binary
predicate of equality.  This is why it does not appear in Tarski's FOL system,
being a special case of his scheme ( x = y -> ( ph -> ps ) ) where ph is an
atomic formula and ps is obtained from ph by substituting an occurrence of x
for y.  The above paragraphs prove that this scheme can be weakened by adding
the DV condition DV(x,y).

[Mario Carneiro]

Does this affect the statement of any axioms? This may affect the MM -> MM0 translation, which is assuming that ax-7 is stated with no DV conditions.

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/c630d5bc-487b-45b2-981e-1e7df1cfe929n%40googlegroups.com.

[Benoit]

On Thursday, December 24, 2020 at 12:26:53 AM UTC+1 di....@gmail.com wrote:

Does this affect the statement of any axioms? This may affect the MM -> MM0 translation, which is assuming that ax-7 is stated with no DV conditions.

No, the axioms are unchanged.  For instance for ax-7, I introduced a weakened form ax7v (it is simply ax-7 with an extra DV condition), which is the only statement referencing ax-7, and I proved back ax-7 from it and earlier axioms (theorem ~ax7).  All later theorems should reference ax7 instead of ax-7.  I added the usage discouragement tag to the comment of ax-7, indicating to use ax7 instead.

Benoît