> One question for which I'm looking guidance is on using quantifiers or not.
That's a very important question, and I hope someone with more experience will be able to shed some insight. In particular, if one has a hypothesis, say, "E. x ph", then it is common to see in textbooks things like "Let y be such that ph(y). Then [subproof], so [conclusion which does not depend on y]. Therefore, [that conclusion]." I would formalize it in set.mm by using the "deduction style" and prepending "[. y / x ]. ph" as an antecedent to each line of the subproof. Maybe there are better strategies ? > As an example, I believe the following are all valid but presumably drastically influence the proof strategy? > $e |- ( ph -> -. A. z e. RR ( F ` z ) = 0 ) $. > $e |- ( ph -> E. z e. RR ( F ` z ) =/= 0 ) $. > $e |- ( ph -> C e. RR ) $. $e |- ( 0 < ( abs ` ( F ` C ) ) ) $. > $e |- ( ph -> C e. RR ) $. $e |- ( ( F ` C ) =/= 0 ) $. I believe the first version (the one I used) is closest to what we mean by "F is not identically 0". The equivalence (in classical logic) with the second version is direct, using ~rexnal. I think it would be easier but "cheating" to use the third or fourth version (see above). Benoît -- 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/957b9c68-04bf-414b-8149-07d0801ca962%40googlegroups.com.
