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. Mario On Wed, Oct 7, 2020 at 4:58 PM 'Alexandre Frechette' via Metamath < [email protected]> wrote: > I am not sure I understand how metamath guarantees a unique substitution > at all times. For example, in the proof of `th1` in `demo0.mm`, the two > following expressions need to be matched in step 32: > > `|- ( P -> Q )` > `|- ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) )` > > This can be done with two naive substitutions: > > P := `( t + 0 ) = t` > Q := `( ( t + 0 ) = t -> t = t )` > > or > > P := `( t + 0 ) = t -> ( ( t + 0 ) = t` > Q := `t = t )` > > Is there a rule / principle in Metamath I am missing that precludes the > second ill-defined substitution? > > Thank you! > > -- > 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/dc1c7fd7-3f0a-4aa7-bb30-2287b37fbaa5n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/dc1c7fd7-3f0a-4aa7-bb30-2287b37fbaa5n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSsCdAqWO7u1bL3p7OAdZ8Ud5RiGy_LPJPSq%3DA09ebNtbA%40mail.gmail.com.
