> 1. Implicit substitution. These are theorems that say `( ph -> F(x1, ..., xn) = F(y1, ..., yn) )` given `( ph -> x1 = y1 )`, ..., `( ph -> xn = yn )`. > 2. Not free: These are theorems that say `F/ z F(x1, ..., xn)` given `F/ z x1`, ..., `F/ z xn`. > 3. Explicit substitution: These are theorems that say [ a / b ] F(x1, ..., xn) = F([ a / b ] x1, ..., [ a / b ] xn).
> These are to be interpreted with `=` being used to mean either `<->` or `=` as appropriate. The statements for binders are also somewhat different; this is the prototypical form for regular class or wff operators. Thanks! This info is helpful. It is the relationship between theorems of type 1 and 3 that has me somewhat confused. It seems like allowing bundled variables is what causes a lot of complexity in a few proofs. My philosophy would be to keep variables distinct except for special cases where it might be necessary or helpul ( not quite sure what all those cases are, but they mostly seem to involve substitution and axioms 12 and 13 from my partial understanding ). I understand that allowing bunded variables makes proof checking faster, but I'd rather avoid it wherever that is the *only* reason, mainly because it just seems less intuitive to me than distinct variables. > Your theorem is most similar to (3), but it is also the least well supported in terms of theorems for every constructor. (That is, you aren't going to find a theorem saying that a random non-foundational definition like df-lly commutes with explicit substitution.) However, (1) has essentially full support in the library - there is a theorem of the described form for basically every definition, so if you can rewrite the goal such that it is in terms of implicit substitution, then you can apply that metatheorem and it all works. I'm pretty confident I can figure this part out. > In this case, you want to say that `[ y / x ] P(x)` is equivalent to `P(y)`, where `P(x)` represents any propositional formula containing free occurrences of `x`. To do this, we would apply theorem https://us.metamath.org/mpeuni/sbie.html , which reduces the goal to a case of (1) and a case of (2). (It is possible to avoid a dependence on metatheorem (2) as well, by alpha renaming all bound occurrences of x in P(y) to something else, so that P(y) syntactically contains no occurrences of x and theorem ~nfv applies. Proving that such an alpha rename is legal is a recursive application of (1).) This is the part I need to study more. Thanks again. -- 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/cdb8d6b4-9c04-4424-bf43-8f2ae227476dn%40googlegroups.com.
