> On Oct 7, 2020, at 5:11 PM, Mario Carneiro <[email protected]> wrote: > > The theorem mp actually has 4 arguments. The first two are the substitutions, > which are usually suppressed. That is, you first have to prove wff P, then > wff Q, then |- P, then |- ( P -> Q ), and then theorem mp applies to derive > |- Q. If you use metamath.exe, "show proof th1" will list only 5 steps, but > with suspicious gaps in the numbering; "show proof th1 /full" will show all > the substitution steps (which in fact make up the majority of the actual > proof on disk). > > A proof of "wff P" is equivalent to a proof that P is a well formed formula, > and it is this that prevents invalid substitutions like Q := `t = t )`; you > will not be able to prove `wff t = t )` so that proof will not work. But in > any case the verifier isn't being asked to come up with the substitution > (although most metamath proof assistants will, using unification), so no > matching algorithm is necessary, only a substitution and an equality check.
This is a nice answer. We do note this in: http://us.metamath.org/mpeuni/mmset.html#proofs <http://us.metamath.org/mpeuni/mmset.html#proofs> under “legal syntax”. However, it’s probably too abstract as it’s currently written. I plan to tweak this question & answer as a proposed extension to the “legal syntax” part, because this specific answer may make it much clearer. --- David A. Wheeler -- 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/DF5A8E56-348A-45B6-A1E8-3FA0949FBC5B%40dwheeler.com.
