When to use a "ph ->" antecedent in a deduction form

[Norman Megill]

(This continues the thread "question about fsumshft" https://groups.google.com/d/msg/metamath/vt6SqLrxEfo/t8WbKnW4DgAJ but is more general, so I am starting a new thread.)

A general issue raised by the previous thread  is our convention for when we should or shouldn't use "ph ->" as an antecedent for hypotheses in theorems expressed in deduction form.

There are four types of hypotheses (at least that I can think of right now) where we usually do not use a "ph ->" antecedent in a theorem's deduction form.  Although it may weaken the theorem slightly, omitting this antecedent where it is not needed can make proofs using the theorem slightly shorter by not having to apply ~ a1i in order to match its hypotheses.  In the occasional situation where we need to strengthen the deduction form with "ph ->" on one of these hypotheses, I indicate a possible method.

1. Existence (sethood) hypothesis e.g.:

$e ... |- A e. _V $.

To add "ph ->", first turn the "A e. _V" into an antecedent using ~ vtoclg and friends as in e.g.  ~ unisng, then convert from this (semi-)closed form back to deduction form.


2. Not-free-in hypothesis e.g.:

$e ... |- F/ x ps $.
$e ... |- F/_ x A $.

I don't know of a good way to add "ph ->" in general.  Worst case, the theorem may have to be reproved back through a number of previous theorems.  We do have many "nf*d" theorems that will assist this.  (If anyone knows of a better method, let me know.)  I think the need for "ph -> F/ x ps" is pretty rare, though.

The special case where ps is ph is given by ~ nfdi.


3. Definitional hypothesis e.g.:

$e ... |- ( ps <-> ( ch /\ th ) )
$e ... |- A = ( B + C ) $.

To add "ph ->", eliminate the original hypothesis with ~ biid or ~ eqid, then rewrite the proof where the steps are simplified with the new "ph ->" form of the definitional hypotheses.  See also Mario's discussion at
https://groups.google.com/d/msg/metamath/V6QPBWzqvu4/jmY9kwLWCgAJ


4. Implicit substitution hypothesis e.g.:

$e ... |- ( x = y -> ( ps <-> ch ) ) $.
$e ... |- ( x = y -> A = B ) $.

To add "ph ->", convert theorem to explicit substitution form, then convert back to implicit substitution form.  This can be somewhat tedious, but at least it can be done in principle.  See ~ fsumshftd for an example, discussed at https://groups.google.com/d/msg/metamath/vt6SqLrxEfo/yEWda79jEgAJ

[Olivier Binda]

Many thanks for this post. It will really help me a lot (and others too). :)

Olivier

Le vendredi 1 novembre 2019 22:00:24 UTC+1, Norman Megill a écrit :

(This continues the thread "question about fsumshft" https://groups.google.com/d/msg/metamath/vt6SqLrxEfo/t8WbKnW4DgAJ but is more general, so I am starting a new thread.)

A general issue raised by the previous thread  is our convention for when we should or shouldn't use "ph ->" as an antecedent for hypotheses in theorems expressed in deduction form.

There are four types of hypotheses (at least that I can think of right now) where we usually do not use a "ph ->" antecedent in a theorem's deduction form.  Although it may weaken the theorem slightly, omitting this antecedent where it is not needed can make proofs using the theorem slightly shorter by not having to apply ~ a1i in order to match its hypotheses.  In the occasional situation where we need to strengthen the deduction form with "ph ->" on one of these hypotheses, I indicate a possible method.

1. Existence (sethood) hypothesis e.g.:

$e ... |- A e. _V $.

To add "ph ->", first turn the "A e. _V" into an antecedent using ~ vtoclg and friends as in e.g.  ~ unisng, then convert from this (semi-)closed form back to deduction form.


2. Not-free-in hypothesis e.g.:

$e ... |- F/ x ps $.
$e ... |- F/_ x A $.

I don't know of a good way to add "ph ->" in general.  Worst case, the theorem may have to be reproved back through a number of previous theorems.  We do have many "nf*d" theorems that will assist this.  (If anyone knows of a better method, let me know.)  I think the need for "ph -> F/ x ps" is pretty rare, though.

The special case where ps is ph is given by ~ nfdi.


3. Definitional hypothesis e.g.:

$e ... |- ( ps <-> ( ch /\ th ) )
$e ... |- A = ( B + C ) $.

To add "ph ->", eliminate the original hypothesis with ~ biid or ~ eqid, then rewrite the proof where the steps are simplified with the new "ph ->" form of the definitional hypotheses.  See also Mario's discussion at
https://groups.google.com/d/msg/metamath/V6QPBWzqvu4/jmY9kwLWCgAJ


4. Implicit substitution hypothesis e.g.:

$e ... |- ( x = y -> ( ph <-> ps ) ) $.

$e ... |- ( x = y -> A = B ) $.

To add "ph ->", convert theorem to explicit substitution form, then convert back to implicit substitution form.  This can be somewhat tedious, but at least it can be done in principle.  See ~ fsumshftd for an example, discussed at

https://groups.google.com/d/msg/metamath/vt6SqLrxEfo/tmogkcRPEgAJ

[Mario Carneiro]

On Fri, Nov 1, 2019 at 5:00 PM Norman Megill <n...@alum.mit.edu> wrote:

2. Not-free-in hypothesis e.g.:

$e ... |- F/ x ps $.
$e ... |- F/_ x A $.

I don't know of a good way to add "ph ->" in general.  Worst case, the theorem may have to be reproved back through a number of previous theorems.  We do have many "nf*d" theorems that will assist this.  (If anyone knows of a better method, let me know.)  I think the need for "ph -> F/ x ps" is pretty rare, though.

As I discovered in nfnlem of peano.mm1 (https://github.com/digama0/mm0/blob/master/examples/peano.mm1#L1019-L1024), it is possible to prove the not-free theorem for a term constructor given the equality theorem, provided you can substitute the terms for variables.

Suppose I have a constructor "foo ( A , B )" and I want to prove ( A e. V /\ B e. V /\ F/_ x A /\ F/_ x B ) -> F/_ x foo ( A , B ). I let y = A and z = B be new dummies, then F/_ x foo ( A , B ) <-> F/_ x foo ( y , z ), but the latter is true by nfv. The F/_ x A and F/_ B theorems come up when I want to prove ( y = A /\ z = B ) -> ( F/_ x foo ( y , z ) <-> F/_ x foo ( A , B ) ); the nf equality step here requires that the context be free from x, so you need a special version of the theorem so that this can be given as a hypothesis.

That said, it's not very useful for set.mm, because of the A e. V, B e. V assumptions that are needed in order to substitute a variable for a class. (You can substitute a wff for a variable, if the universe has at least two elements; for example you can use (/) e. x as a substitute for variable ph, where we take x to be the set { y e. 1o | ph }.) This theorem is usually provable without the assumption, but you have to work your way up through the whole definitional stack to prove it.

 

4. Implicit substitution hypothesis e.g.:

$e ... |- ( x = y -> ( ph <-> ps ) ) $.

$e ... |- ( x = y -> A = B ) $.

To add "ph ->", convert theorem to explicit substitution form, then convert back to implicit substitution form.  This can be somewhat tedious, but at least it can be done in principle.  See ~ fsumshftd for an example, discussed at

https://groups.google.com/d/msg/metamath/vt6SqLrxEfo/tmogkcRPEgAJ

I want to point out that this is considerably less tedious if "A" and "B" are closed terms already, i.e. you are applying the theorem in some context rather than just trying to prove fsumshftd itself (which doesn't know what A and B are). For instance, if you want to prove

 

|- sum_ x e. ( 1 ... 3 ) ( ( x + 1 ) ^ 2 ) = sum_ y e. ( 2 ... 4 ) ( y ^ 2 )

by shifting the left sum to the right, you first apply fsumshft without any funny business in the substitution to prove

|- sum_ x e. ( 1 ... 3 ) ( ( x + 1 ) ^ 2 ) = sum_ y e. ( 2 ... 4 ) ( ( ( y - 1 ) + 1 ) ^ 2 ),

then use sumeq2dva and equality theorems to prove ( ( ( y - 1 ) + 1 ) ^ 2 ) = ( y ^ 2 ) in the current context.

[David A. Wheeler]

> On Fri, 1 Nov 2019 20:17:56 -0400, Mario Carneiro <di....@gmail.com> wrote:
> On Fri, Nov 1, 2019 at 5:00 PM Norman Megill <n...@alum.mit.edu> wrote:

These are useful tips. I've tried to add a summary of these tips to mmnatded.raw.html
in this pull request: https://github.com/metamath/set.mm/pull/1236

There is no label sumeq2dva ; I presume esumeq12dva was intended
(if not, please let me know).

--- David A. Wheeler

[Mario Carneiro]

Looks like it is sumeq2dv; I guess our usage of the "a" suffix in these circumstances is inconsistent (compare mpteq2dv / mpteq2dva vs sumeq2sdv / sumeq2dv).

 

--- David A. Wheeler

--
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/E1iQwtl-00015C-Ef%40rmmprod07.runbox.

[David A. Wheeler]

> On Sat, Nov 2, 2019 at 1:09 PM David A. Wheeler <dwhe...@dwheeler.com>
> wrote:
> > There is no label sumeq2dva ; I presume esumeq12dva was intended
> > (if not, please let me know).

On Sat, 2 Nov 2019 20:35:48 -0400, Mario Carneiro <di....@gmail.com> wrote:
> Looks like it is sumeq2dv; I guess our usage of the "a" suffix in these
> circumstances is inconsistent (compare mpteq2dv / mpteq2dva vs sumeq2sdv /
> sumeq2dv).

I'm happy to fix it, but should we rename sumeq2dv to sumeqdva first,
and then change the text to match? Or should we just use sumeqdv ?

--- David A. Wheeler

[Mario Carneiro]

I suggest just changing your note for now. The suffix usage thing requires a more systematic study (it's about consistency, after all), which is a separate issue.

--
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/E1iR3yx-0004yh-UC%40rmmprod07.runbox.