>
> The hypothesis of bj-df-cleq corresponds to setvar substitutions into A
> and B. Do we know that other substitutions into A and B can't generate FOL=
> statements that are stronger than the hypothesis? Perhaps we are safe since
> we may need df-cleq itself to eliminate the resulting class notation, but I
> haven't thought it through completely to be sure there aren't tricks that
> can be done with the other two class definitions. What do you think?
If I understand your question correctly, then the following result might
answer your concerns:
Theorem: Let S be any set of schemes. Assume that we can prove a scheme
Phi which contains no class terms or class variables from S \cup \{df-clab,
bj-df-cleq, bj-df-clel\}. Then, we can prove it from S \cup {minimal
positive calculus}.
Proof: Consider a proof of Phi from S \cup \{df-clab, bj-df-cleq,
bj-df-clel\}. Using \{df-clab, bj-df-cleq, bj-df-clel, minimal positive
calculus\}, eliminate class abstractions from the proof. There may also be
dummy class variables; replace them with fresh dummy setvar variables.
Now, the proof contains no class abstraction so does not use df-clab, and
for the lines using bj-df-cleq or bj-df-clel, they can be "removed" since
the conclusion is an alpha-renaming of the hypthesis (more precisely, you
prove their conclusion directly using the corresponding alpha-renaming of
the proof of its hypothesis in the original proof). QED
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/e45608f8-3d53-42c1-a84c-a0cd5f7fd314n%40googlegroups.com.
