On Fri, Nov 1, 2019 at 5:00 PM Norman Megill <[email protected]> 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. -- 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/CAFXXJSsvPDzCWCXEFieVj99o7WBvPMXs49rnaz9c0pA5MHByNw%40mail.gmail.com.
