Simple substitution in Metamath

[Alexandre Frechette]

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!

[Mario Carneiro]

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

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/dc1c7fd7-3f0a-4aa7-bb30-2287b37fbaa5n%40googlegroups.com.

[David A. Wheeler]

On Oct 7, 2020, at 5:11 PM, Mario Carneiro <di....@gmail.com> 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 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

[David A. Wheeler]

On Oct 7, 2020, at 5:11 PM, Mario Carneiro <di....@gmail.com> wrote: ...

On Oct 7, 2020, at 5:25 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:

This is a nice answer.

We do note this in: 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.

I tried to capture this discussion in this pull request:

https://github.com/metamath/set.mm/pull/1843

[Alexandre Frechette]

Thank you Mario, this reminded me that to find the substitution for an assertion, you have to process its mandatory hypotheses in order. I was disregarding the ordering.

--
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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/EF1ED7AC-55A0-499B-A104-7964FF5843B2%40dwheeler.com.