On Sunday, June 2, 2019 at 6:44:56 AM UTC-4, Tony wrote: > > I don't understand how to handle substitutions in Metamath. If I use > > stdpc7 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑 → 𝜑)), > > how do I then actually change y to x in 𝜑? > > I don't see any suitable theorems to use. Like for instance: > > [𝑥 / 𝑦] (𝜑 ↔ 𝜓) ↔ ( [𝑥 / 𝑦]𝜑 ↔ [𝑥 / 𝑦]𝜓 ), > [𝑥 / 𝑦] (𝜑 ∧ 𝜓) ↔ ( [𝑥 / 𝑦]𝜑 ∧ [𝑥 / 𝑦]𝜓 ). >
These are ~ sbbi and ~ sban resp. There are also ~ sbim, ~ sbor, ~ sbal. However, as mentioned below, unless you are working strictly in predicate calculus it is usually more useful to use the sbc* versions. To connect sb* and sbc* versions, there is ~ sbsbc, although there is no sb* equivalent when class variables or class expressions (other than a setvar) are involved. BTW stdpc7 is mostly for illustrating a traditional predicate calculus equivalent and is rarely is actually useful, as its limited uses show. There's nothing wrong with using it, though, if it offers an advantage. Overall, a good initial approach may be to study how some existing proofs are done to get a feel for what approaches work the best. On Sunday, June 2, 2019 at 8:17:52 AM UTC-4, Benoit wrote: > > They use class substitution (i.e., [. ].) instead of set substitution >> (i.e., [ ]). My understanding is that class substitution is the one that >> should be used in "higher-level" proof, with set substitution just being >> used in turn to properly support class substitution. The "end-user" >> theorems are probably easier to find for class substitution > > > My limited experience confirms this: sbc* theorems get more used than > their sb* counterparts outside of FOL. > Correct. > > >> (although, of course, in the end what you are going to substitute is a >> set anyway, >> but not necessarily a set variable). > > > I would rather think of it as: "In the end, what you are going to > substitute is generally a term, not a variable"... which confirms that sbc* > theorems are more useful than sb* theorems. > Agree. > > >> > Is using those theorems the best way to do substitution? Seems like >> > there can be a lot of steps for something you would normally do in a >> > single step in an informal proof. >> >> I guess this is one of the prices you pay for having formal proofs (and >> for having such a low level language like Metamath) > > > I think that it is often possible to avoid "[ / ]-substitutions" (are they > the ones called "implicit substitutions"?) > We have been calling [. A / x ]. ph "explicit" (because it has an explicit substitution symbol) and "x = A -> ( ph <-> ps )" "implicit". See the descriptions of ~ sbie and ~ sbcie. > by modifying your proof a bit, and use "explicit substitution" instead > (typically with steps like "x = A -> ( ph <-> ps )"). It would be > interesting that someone with more practice confirms/infirms this. > While I don't have rigorous data, I think implicit substitution usually leads to shorter proofs than explicit. That has almost always been the case when I've tried both ways. One of the reasons is that implicit substitution can create a wff without a variable we want to avoid (e.g. by replacing an x in ph with a dummy variable y in ps, using a cbv* theorem), whereas with explicit substitution, the variable we want to avoid remains bound, as e.g. the x in [. y / x ]. ph. That means we can't use a simple $d x ps but must build up a "not free in" condition using nf* theorems, sometimes making the proof significantly larger. That said, I think explicit substitution has an advantage in most of the present uses, since otherwise it's likely we would have shortened the proof using implicit substitution. However, it might be useful to revisit those uses someday to see if some proofs can be shortened with implicit substitution, especially when there are lots of nf* theorems used. Norm -- 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/c706aad7-5d73-4bdd-b502-8dec1e698150%40googlegroups.com.
