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.
On Wed, Dec 23, 2020 at 5:48 PM Benoit <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/c630d5bc-487b-45b2-981e-1e7df1cfe929n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSsd30%3D0QgD1DT_90ebtRMVHSbxhMqcRu%2BN2JnKqg3eWFw%40mail.gmail.com.
