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 <[email protected]> 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 [email protected].
> 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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAFXXJSvD7qJD4hJu0x6Jt4uxzFw0sdOj4PFZxo%2Biwo6CUkSL_A%40mail.gmail.com.
