On Sunday, June 2, 2019 at 1:31:34 PM UTC-4, Norman Megill wrote: > > On Sunday, June 2, 2019 at 12:52:21 PM UTC-4, Tony wrote: >> >> On Sunday, June 2, 2019 at 6:02:30 PM UTC+2, Norman Megill wrote: >> >> 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. >>> >> >> I have no idea what "implicit substitution" means. I don't understand >> what any of the theorems containing constructions like x = A -> ( ph <-> >> ps ) is about. >> > > Compare the explicit substitution version of finite induction (on ordinals) > http://us.metamath.org/mpeuni/findes.html > with the implicit substitution version > http://us.metamath.org/mpeuni/finds.html > Note that the implicit version has found more uses, although that may be > partly because the implicit version has an additional hypothesis to give us > a more useful class variable rather than a setvar variable in the > conclusion. > > Here is a little project if anyone is interested: If we enhance ~ findes (and ~ tfindes) to use a class variable in the conclusion, that would be nicer for direct comparisons like this as well as for possible future use. The hypotheses would remain the same, and the conclusion would be changed from
|- ( x e. om -> ph ) to |- ( A e. om -> [. A / x ]. ph ) Ideally, it would not require $d x A $ in order. to make it easier to work with, e.g. sbcid could be used to easily recover the existing version if it's ever needed. 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/1a073a06-2e53-4b57-bff4-00c94c38437f%40googlegroups.com.
