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