What is ax-9c? It isn't an axiom in set.mm.
Norm
On Friday, October 29, 2021 at 1:46:46 PM UTC-4 di....@gmail.com wrote:
> Here's a sketch of the proof of conservativity of the class axioms. We
> remove them one at a time: first removing df-clel, then df-cleq, and
> finally ax-9c, df-clab and class all at once.
>
> Assume that the base theory S has enough to move equivalences through the
> logical connectives, and prove alpha renaming of FOL= formulas. Suppose we
> have a proof of Phi from S \cup \{df-clab, bj-df-cleq\} where Phi does not
> use any occurrences of A = B except on set variables; we will eliminate
> bj-df-cleq. If bj-df-cleq is not used in the proof then we are done,
> otherwise consider the first occurrence of bj-df-cleq in the proof. By
> minimality, the hypothesis to bj-df-cleq must not be proven using
> bj-df-cleq, so ax-ext is a theorem of S \cup \{df-clab\}. Now, pick a
> variable z not appearing in the proof, and replace all occurrences of A = B
> with A. z (z e. A <-> z e. B). At the leaves, we have transformed instances
> of axioms like ax-8': (A. z (z e. a <-> z e. b) -> (a e. c -> b e. c)), and
> we can prove this from ax-8 by replacing A. z (z e. a <-> z e. b) with a =
> b using ax-ext and equality theorems. Thus Phi' is provable from S \cup
> \{df-clab\}, and Phi differs from Phi' only in the replacement of some a =
> b with A. z (z e. a <-> z e. b), so we can use ax-ext and equality theorems
> to prove Phi as well.
>
> The situation with df-clel is more complicated, and here is a failed proof
> of a similar reduction to replace A e. B with x e. A. Suppose S \cup
> \{df-clab, bj-df-cleq, bj-df-clel\} proves Phi, and Phi does not mention A
> e. B except as x e. A. If bj-df-clel is not used then we are done, else a
> minimal application of it shows that cleljust is provable from S \cup
> \{df-clab, bj-df-cleq\}. Now replace all instances of A e. B with E. z (z =
> A /\ z e. B) where z is a variable not occurring in the proof, and use
> cleljust (!!!) to replace each transformed E. z (z = x /\ z e. A) in axioms
> with x e. A, so that the original axiom + equality theorems proves the
> transformed axiom. Similarly, we prove Phi' <-> Phi and thus Phi is
> provable from S \cup \{df-clab, bj-df-cleq\}.
>
> This proof fails at the (!!!), because we need to know that x e. A <-> E.
> z (z = x /\ z e. A), and cleljust is not good enough to cover this
> situation. We can repair the proof with a variation on bj-df-clel that
> looks like this:
>
> mc-df-clel.1 $e |- ( u e. B <-> E. v ( v = u /\ v e. B ) )
> mc-df-clel $p |- ( A e. B <-> E. x ( x = A /\ x e. B ) )
>
> We have to be more careful about uses of cleljust now because class
> variables in a hypothesis can't be substituted. Let cleljust[A] refer to
> the theorem |- ( u e. A <-> E. v ( v = u /\ v e. A ) ) for fixed A. We need
> to know that this is equivalent to |- ( x e. A <-> E. y ( y = x /\ y e. A )
> ) (where u,v,x,y,A are all distinct), and I don't think this comes for
> free, so let us assume ax-9c is derivable from the base theory S. Now, for
> each application of mc-df-clel[A, B], there is a minimal one for each fixed
> B, and hence we get that cleljust[B] is derivable from S. For each such B
> we replace all occurrences of A e. B (for any A) with E. x ( x = A /\ x e.
> B ), then back substitute E. v ( v = u /\ v e. B ) to u e. B in transformed
> axioms and Phi to conclude (using cleljust[B] to validate the substitution).
>
> Now this is interesting, because even if you have ax-9c directly as a
> premise to mc-df-clel, it's still not good enough to derive variations on
> ax-9c with different set variables, because you need (different
> substitution instances of) ax-9c itself to prove the equivalence. So this
> trick with adding hypotheses to axioms is not sufficient in general, you
> can't just stick all of FOL as a hypothesis and hope that solves the
> situation.
>
> Finally, we want to eliminate x e. A, which is the hardest part because it
> comes together with "class" and { x | ph } as a unit. Suppose Phi derives
> from S \cup \{df-clab\}, and Phi does not contain any class variables, any
> use of { x | ph }, any use of A e. B except as x e. y, and any use of A = B
> except as x = y. By substituting all dummy class variables B in the proof
> by { x | F. }, we get that Phi is derivable without any class variables in
> the proof. By the previous two transformations we can ensure that the proof
> also does not use A = B or A e. B except as x e. A. For the latter part, we
> need cleljust[B] to be derivable for various B, but because all class
> variables are eliminated from the proof, we only need cleljust[{x | ph}]
> for various choices of x,ph and this is derivable using df-clab. Thus we
> get a simplified proof of Phi from S \cup \{df-clab\} which only uses x e.
> A and { x | ph }. Now, since there are no class variables, every subformula
> of the form x e. A must have the form x e. {y | ph}, and so we can replace
> all instances of x e. {y | ph} with [x / y] ph. The transformed df-clab and
> ax-9c instances are theorems of S, and none of the other axioms mention cab
> or wvel. Since Phi is not changed by the transformation, Phi is derivable
> from S.
>
> On Fri, Oct 29, 2021 at 12:24 PM Benoit <benoit...@gmail.com> wrote:
>
>> On Friday, October 29, 2021 at 6:05:19 PM UTC+2 Norman Megill wrote:
>>
>>> Can you remind me what the minimal positive calculus is?
>>>
>>
>> What I had in mind was {ax-mp, ax-1, ax-2, impbi, biimp, biimpr, simpl,
>> simpr, pm3.2}, or really anything that suffices to move the equivalences
>> through the other connectives. I realize one may also need ~alim and ~exim
>> since these quantifiers occur in dfcleq/clel. But actually, that part of
>> my proof sketch is too sketchy... I should ponder a bit more on this, but
>> it seems that the special form of bj-df-cleq/clel could permit to simplify
>> Levy's proof in the appendix of Basic Set Theory.
>>
>> Benoît
>>
>> --
>> 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/063cda68-5e30-45a8-8397-b694093b2924n%40googlegroups.com
>>
>> <https://groups.google.com/d/msgid/metamath/063cda68-5e30-45a8-8397-b694093b2924n%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 metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/1618d8c9-a300-4b5a-9a73-1d751bf55aaan%40googlegroups.com.
