Replacing $d with F/ and F/_

[Giovanni Mascellani]

Hi! I think there is a general trick to replace a $d x A or $d x ph$
condition in a theorem with the corresponding F/_ x A or F/ x ph, but I
do not remember it. Can anybody help me?

(in this specific case, I would like to do that for sbcex2 and its
universal counterpart)

Thanks, Giovanni.

PS. I already asked the same question on the Metamath Gitter channel[1],
but I believe it is not very active at the moment!

[1] https://gitter.im/metamath/Lobby
--
Giovanni Mascellani <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles

[Benoit]

On Tuesday, May 28, 2019 at 9:25:47 PM UTC+2, Giovanni Mascellani wrote:

Hi! I think there is a general trick to replace a $d x A or $d x ph$
condition in a theorem with the corresponding F/_ x A or F/ x ph, but I
do not remember it. Can anybody help me?

(in this specific case, I would like to do that for sbcex2 and its
universal counterpart)

Hi Giovanni.  I think that by now, most utility theorems with dv conditions have an analogous "nf-version" where the dv conditions are replaced with non-freeness $e-hypotheses.  In your example sbcex2, it looks like it is sufficient to replace:

exlimiv with exlimi,

exbidv with exbid,

vtoclbg with vtoclbgf.

Generally, the labels are found by adding a suffixed "f" or removing a suffixed "v".

I'm not sure there is a completely automatizable method to find the nf-proof from a dv-proof, but there are certainly recurring patterns.

 

PS. I already asked the same question on the Metamath Gitter channel[1],
but I believe it is not very active at the moment!

 [1] https://gitter.im/metamath/Lobby

I did not know of this channel.  Maybe it would be nice to centralize discussions on this group and forget/close the other ones?

 

Benoît

[Mario Carneiro]

On Tue, May 28, 2019 at 3:25 PM Giovanni Mascellani <g.masc...@gmail.com> wrote:

Hi! I think there is a general trick to replace a $d x A or $d x ph$
condition in a theorem with the corresponding F/_ x A or F/ x ph, but I
do not remember it. Can anybody help me?

The technique is the following. Suppose you have |- T[x, A] where $d x A, and you wish to prove |- F/_ x A => |- T[x, A]. You apply the theorem substituting y for x and A for A, where y is a new dummy variable, so that $d y A is satisfied. You obtain |- T[y, A], and apply chvar to obtain |- T[x, A] (or just use mpbir if T[x, A] binds x). The side goal is |- ( x = y -> ( T[y, A] <-> T[x, A] ) ), where you can use equality theorems, except that when you get to a bound variable you use a non-dv bound variable renamer theorem like cbval. The section us2.metamath.org/mpeuni/mmtheorems32.html#mm3146s also describes the metatheorem that underlies this.

 

PS. I already asked the same question on the Metamath Gitter channel[1],
but I believe it is not very active at the moment!

 [1] https://gitter.im/metamath/Lobby

As you probably noticed, the gitter lobby gets one post a year or so. I thought it might be helpful for people who like the chat style, but gitter doesn't notify me when something comes in so given the tiny traffic it's pretty hard to get a quick response, and your post might just sit there for months before someone notices. The google group is definitely the best way to get attention from the metamath community right now.

Mario

[Benoit]

Using the replacements I gave above yielded the proof:

  ${
    $d z A $.  $d x y z $.  $d z ph $.
    sbcex2f.1 $e |- F/_ x A $.
    $( Move existential quantifier in and out of class substitution.
       (Contributed by NM, 21-May-2004.)  (Revised by NM, 18-Aug-2018.) $)
    sbcex2f $p |- ( [. A / y ]. E. x ph <-> E. x [. A / y ]. ph ) $=
              ( vz wex wsbc cvv wcel sbcex nfel1 exlimi wsb dfsbcq2 nfeq2 exbid
              cv wceq sbex vtoclbg pm5.21nii ) ABGZCDHZDIJZACDHZBGZUCCDKUFUEBBD
              IELACDKMUCCFNACFNZBGUDUGFDIUCCFDOFRZDSUHUFBBUIDEPACFDOQABCFTUAUB
              $.
  $}

The technique is the following. Suppose you have |- T[x, A] where $d x A, and you wish to prove |- F/_ x A => |- T[x, A]. You apply the theorem substituting y for x and A for A, where y is a new dummy variable, so that $d y A is satisfied. You obtain |- T[y, A], and apply chvar to obtain |- T[x, A] (or just use mpbir if T[x, A] binds x). The side goal is |- ( x = y -> ( T[y, A] <-> T[x, A] ) ), where you can use equality theorems, except that when you get to a bound variable you use a non-dv bound variable renamer theorem like cbval. The section us2.metamath.org/mpeuni/mmtheorems32.html#mm3146s also describes the metatheorem that underlies this.

That's a nice general technique.  It is illustrated by a proof from today!  Look at the proof of mo2 from mo2v; it uses cbvex.