Can you remind me what the minimal positive calculus is?
On Friday, October 29, 2021 at 11:58:02 AM UTC-4 Benoit wrote:
> 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 metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/d6e3628d-8f02-4b72-9c1d-24809f11e78bn%40googlegroups.com.
