How to do substitutions in Metamath?

[Tony]

I don't understand how to handle substitutions in Metamath. If I use

stdpc7 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑 → 𝜑)),

how do I then actually change y to x in 𝜑?

I don't see any suitable theorems to use.  Like for instance:

[𝑥 / 𝑦] (𝜑 ↔  𝜓) ↔ ( [𝑥 / 𝑦]𝜑 ↔ [𝑥 / 𝑦]𝜓 ),

[𝑥 / 𝑦] (𝜑 ∧  𝜓) ↔ ( [𝑥 / 𝑦]𝜑 ∧ [𝑥 / 𝑦]𝜓 ).

[Giovanni Mascellani]

Hi,

Il 02/06/19 12:44, Tony ha scritto:

> I don't see any suitable theorems to use.  Like for instance:
>
> [𝑥 / 𝑦] (𝜑 ↔  𝜓) ↔ ( [𝑥 / 𝑦]𝜑 ↔ [𝑥 / 𝑦]𝜓 ),
> [𝑥 / 𝑦] (𝜑 ∧  𝜓) ↔ ( [𝑥 / 𝑦]𝜑 ∧ [𝑥 / 𝑦]𝜓 ).

Look for sbcan and those that immediately follow:

http://us.metamath.org/mpeuni/mmtheorems33.html#sbcan

HTH, Giovanni.
--
Giovanni Mascellani <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles

[Tony]

On Sunday, June 2, 2019 at 1:06:54 PM UTC+2, Giovanni Mascellani wrote:

Look for sbcan and those that immediately follow:

  http://us.metamath.org/mpeuni/mmtheorems33.html#sbcan

Thank you! I couldn't find those by myself.

Is using those theorems the best way to do substitution? Seems like there can be a lot of steps for something you would normally do in a single step in an informal proof.

[Giovanni Mascellani]

Hi,

Il 02/06/19 13:37, Tony ha scritto:

> Thank you! I couldn't find those by myself.

They use class substitution (i.e., [. ].) instead of set substitution
(i.e., [ ]). My understanding is that class substitution is the one that
should be used in "higher-level" proof, with set substitution just being
used in turn to properly support class substitution. The "end-user"
theorems are probably easier to find for class substitution (although,
of course, in the end what you are going to substitute is a set anyway,
but not necessarily a set variable).

> Is using those theorems the best way to do substitution? Seems like
> there can be a lot of steps for something you would normally do in a
> single step in an informal proof.

I guess this is one of the prices you pay for having formal proofs (and
for having such a low level language like Metamath): you have to deal
with really boring and, to the extent one is normally used to, trivial
details. Ideally it would be nice to have some more help from tooling
here, and it is one of the things I am working on with my project mmpp
(but it is not yet ready).

This is BTW the reason why I knew the answer to your question
immediately! I also have variants of sbcan and a few others in inference
form in my mathbox:

http://us2.metamath.org/mpeuni/mmtheorems284.html#sbcani

With these variants you directly construct the substitution of a complex
formula without having to use a lot of mp* or syl* at each depth stage.

[Benoit]

They use class substitution (i.e., [. ].) instead of set substitution
(i.e., [ ]). My understanding is that class substitution is the one that
should be used in "higher-level" proof, with set substitution just being
used in turn to properly support class substitution. The "end-user"
theorems are probably easier to find for class substitution

My limited experience confirms this: sbc* theorems get more used than their sb* counterparts outside of FOL.

 

(although, of course, in the end what you are going to substitute is a set anyway,
but not necessarily a set variable).

I would rather think of it as: "In the end, what you are going to substitute is generally a term, not a variable"... which confirms that sbc* theorems are more useful than sb* theorems.

 

> Is using those theorems the best way to do substitution? Seems like
> there can be a lot of steps for something you would normally do in a
> single step in an informal proof.

I guess this is one of the prices you pay for having formal proofs (and
for having such a low level language like Metamath)

I think that it is often possible to avoid "[ / ]-substitutions" (are they the ones called "implicit substitutions"?) by modifying your proof a bit, and use "explicit substitution" instead (typically with steps like "x = A -> ( ph <-> ps )").  It would be interesting that someone with more practice confirms/infirms this.

 

Benoit

[Norman Megill]

On Sunday, June 2, 2019 at 6:44:56 AM UTC-4, Tony wrote:

I don't understand how to handle substitutions in Metamath. If I use

stdpc7 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑 → 𝜑)),

how do I then actually change y to x in 𝜑?

I don't see any suitable theorems to use.  Like for instance:

[𝑥 / 𝑦] (𝜑 ↔  𝜓) ↔ ( [𝑥 / 𝑦]𝜑 ↔ [𝑥 / 𝑦]𝜓 ),

[𝑥 / 𝑦] (𝜑 ∧  𝜓) ↔ ( [𝑥 / 𝑦]𝜑 ∧ [𝑥 / 𝑦]𝜓 ).

These are ~ sbbi and ~ sban resp.  There are also ~ sbim, ~ sbor, ~ sbal.

However, as mentioned below, unless you are working strictly in predicate calculus it is usually more useful to use the sbc* versions.  To connect sb* and sbc* versions, there is ~ sbsbc, although there is no sb* equivalent when class variables or class expressions (other than a setvar) are involved.

BTW stdpc7 is mostly for illustrating a traditional predicate calculus equivalent and is rarely is actually useful, as its limited uses show.  There's nothing wrong with using it, though, if it offers an advantage.  Overall, a good initial approach may be to study how some existing proofs are done to get a feel for what approaches work the best.

On Sunday, June 2, 2019 at 8:17:52 AM UTC-4, Benoit wrote:

They use class substitution (i.e., [. ].) instead of set substitution
(i.e., [ ]). My understanding is that class substitution is the one that
should be used in "higher-level" proof, with set substitution just being
used in turn to properly support class substitution. The "end-user"
theorems are probably easier to find for class substitution

My limited experience confirms this: sbc* theorems get more used than their sb* counterparts outside of FOL.

Correct.
 

 

(although, of course, in the end what you are going to substitute is a set anyway,
but not necessarily a set variable).

I would rather think of it as: "In the end, what you are going to substitute is generally a term, not a variable"... which confirms that sbc* theorems are more useful than sb* theorems.

Agree.
 

 

> Is using those theorems the best way to do substitution? Seems like
> there can be a lot of steps for something you would normally do in a
> single step in an informal proof.

I guess this is one of the prices you pay for having formal proofs (and
for having such a low level language like Metamath)

I think that it is often possible to avoid "[ / ]-substitutions" (are they the ones called "implicit substitutions"?)

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.
 

by modifying your proof a bit, and use "explicit substitution" instead (typically with steps like "x = A -> ( ph <-> ps )").  It would be interesting that someone with more practice confirms/infirms this.

While I don't have rigorous data, I think implicit substitution usually leads to shorter proofs than explicit.  That has almost always been the case when I've tried both ways.  One of the reasons is that implicit substitution can create a wff without a variable we want to avoid (e.g. by replacing an x in ph with a dummy variable y in ps, using a cbv* theorem), whereas with explicit substitution, the variable we want to avoid remains bound, as e.g. the x in [. y / x ]. ph.  That means we can't use a simple $d x ps but must build up a "not free in" condition using nf* theorems, sometimes making the proof significantly larger.

That said, I think explicit substitution has an advantage in most of the present uses, since otherwise it's likely we would have shortened the proof using implicit substitution.  However, it might be useful to revisit those uses someday to see if some proofs can be shortened with implicit substitution, especially when there are lots of nf* theorems used.

Norm

[Tony]

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.

[Thierry Arnoux]

"x = A -> ( ph <-> ps )"

would be the way to state with an implicit substitution the same thing as
“[. A / x ]. ph <-> ps”
states explicitly, that is
“ps is the result of taking all instances of ‘x’ in ph, and substituting them with ‘A’.”

My experience is that implicit substitution is more easy to work with.
_
Thierry

[Norman Megill]

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.

Norm

[Norman Megill]

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

[Benoit]

On Sunday, June 2, 2019 at 7:16:01 PM UTC+2, Thierry Arnoux wrote:

  "x = A -> ( ph <-> ps )"
would be the way to state with an implicit substitution the same thing as
   “[. A / x ]. ph <-> ps”
states explicitly, that is
   “ps is the result of taking all instances of ‘x’ in ph, and substituting them with ‘A’.”

For the record, this equivalence between implicit and explicit substitutions, back and forth, is expressed by the two theorems

  sbceq1a $p |- ( x = A -> ( ph <-> [. A / x ]. ph ) ) $=

and

    $d x A $.  $d x ps $. sbcie.1 $e |- A e. _V $.
    sbcie.2 $e |- ( x = A -> ( ph <-> ps ) ) $.
    sbcie $p |- ( [. A / x ]. ph <-> ps ) $=

Benoit

[Thierry Arnoux]

I believe one reason why implicit substitution is often preferred to explicit substitution is that MMJ2 is able to automatically prove the former.

If you have a formula like:

!10:: |- ( x = A -> ( ( x + 2 ) = ( B / x ) <-> ( A + 2 ) = ( B / A ) ) )

And choose “Unify” (CTRL-U), MMJ2 will normally fully resolve it.

I don’t think it is the case for the “explicit substitution“.

There’s probably a way to update MMJ2 (or its JS based rules) to do so, thought.
BR,

_

Thierry

--
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/d19c8ebd-2d9c-4924-b798-0b3c62ec6182%40googlegroups.com.