Verifying Disjoint Variable Restrictions

[Alexandre Frechette]

My quest to understanding the details of metamath continues.

I found a proof step for a result in set.mm where two mandatory variables are constrained to be disjoint, but mapped to two variables that are not constrained to be disjoint.

In the context of statement `2alimdv`, variables `x` and `ph` are disjoint. However, in that statement's proof,  `x` and `ph` get substituted for `y` and `ps` respectively. But there is no disjoint constraint between `y` and `ps`. This seems to violate disjoint variable restrictions (as per my reading for the end of Section 4.1.4 in the metamath book).

Is there something about `ps` not being mandatory? Am I misunderstanding disjoint variable restrictions?

Thank you!

Details below:

MM> show statement alimdv /full

Statement 4613 is located on line 25887 of the file "set.mm".  Its statement

number for HTML pages is 1756.

"Deduction form of Theorem 19.20 of [Margaris] p. 90, see ~ alim .

       (Contributed by NM, 3-Apr-1994.)"

4613 alimdv $p |- ( ph -> ( A. x ps -> A. x ch ) ) $= ... $.

Its mandatory hypotheses in RPN order are:

  wph $f wff ph $.

  wps $f wff ps $.

  wch $f wff ch $.

  vx $f setvar x $.

  alimdv.1 $e |- ( ph -> ( ps -> ch ) ) $.

Its mandatory disjoint variable pairs are:  <ph,x>

Its optional hypotheses are:  wth wta wet wze wsi wrh wmu wla wka vy vz vw vv

      vu vt

The statement and its hypotheses require the variables:  ph x ps ch

These additional variables are allowed in its proof:  th ta et ze si rh mu la

      ka y z w v u t

The variables it contains are:  ph x ps ch

---

MM> show proof 2alimdv /detailed_step 4

Proof step 4:  wps=wal $a wff A. y ps

This step assigns source "wal" ($a) to target "wps" ($f).  The source assertion

requires the hypotheses "wph" ($f, step 2) and "vx.wal" ($f, step 3).  The

parent assertion of the target hypothesis is "alimdv" ($p, step 15).

The source assertion before substitution was:

    wal $a wff A. x ph

The following substitutions were made to the source assertion:

    Variable  Substituted with

     x         y

     ph        ps

The target hypothesis before substitution was:

    wps $f wff ps

The following substitution was made to the target hypothesis:

    Variable  Substituted with

     ps        A. y ps

[Alexandre Frechette]

Here is another example that seems to violate the other disjoint variable restriction, that two disjoint variable cannot be mapped to expressions that share a variable. In this case, `ph` and `x` are disjoint, but they get mapped in step 8 to expressions that share `x` as a variable.

MM> show statement nfdv /full

Statement 4708 is located on line 26073 of the file "set.mm".  Its statement

number for HTML pages is 1775.

"Apply the definition of not-free in a context.  (Contributed by Mario

       Carneiro, 11-Aug-2016.)"

4708 nfdv $p |- ( ph -> F/ x ps ) $= ... $.

Its mandatory hypotheses in RPN order are:

  wph $f wff ph $.

  wps $f wff ps $.

  vx $f setvar x $.

  nfdv.1 $e |- ( ph -> ( ps -> A. x ps ) ) $.

Its mandatory disjoint variable pairs are:  <ph,x>

Its optional hypotheses are:  wch wth wta wet wze wsi wrh wmu wla wka vy vz vw

      vv vu vt

The statement and its hypotheses require the variables:  ph x ps

These additional variables are allowed in its proof:  ch th ta et ze si rh mu

      la ka y z w v u t

The variables it contains are:  ph x ps

---

MM> show proof nfdv /detailed_step 8

Proof step 8:  wps=wal $a wff A. x ( ps -> A. x ps )

This step assigns source "wal" ($a) to target "wps" ($f).  The source assertion

requires the hypotheses "wph" ($f, step 6) and "vx.wal" ($f, step 7).  The

parent assertion of the target hypothesis is "sylibr" ($p, step 20).

The source assertion before substitution was:

    wal $a wff A. x ph

The following substitutions were made to the source assertion:

    Variable  Substituted with

     x         x

     ph        ( ps -> A. x ps )

The target hypothesis before substitution was:

    wps $f wff ps

The following substitution was made to the target hypothesis:

    Variable  Substituted with

     ps        A. x ( ps -> A. x ps )

[Mario Carneiro]

Disjoint variables between dummy variables (variables that are used in the proof but not the statement) are required by the spec, but it's always safe to assume they are disjoint from everything else and these DV conditions don't affect uses of the theorem (because the dummy variables are not in the substitution at point of use), so they are usually elided from presentation. Have you checked the .mm file to see if the $d y ps $. is actually there?

--
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/f14bc6d1-78d2-4cfa-b26b-5832b21ff769n%40googlegroups.com.

[Alexandre Frechette]

There is no disjoint disjoint restriction for `y` and `ps` in the immediate vicinity of statement `2alimdv` in the set.mm file.

So disjointness only really matters between mandatory variables.

This doesn't seem to explain how two disjoint mandatory variables can map to expressions both containing the same mandatory variable (see second entry in this thread). 

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSt%3D2QHagjU6nPCWbQO7HcbS7CXsOybgxgMfZcFKgfXXbw%40mail.gmail.com.

[Mario Carneiro]

Ah, I see. You have highlighted step 8 of nfdv, which is a syntax step: we are proving that "wff A. x ( ps -> A. x ps )" (that is, A. x ( ps -> A. x ps ) is a well formed formula) by applying the syntax theorem wal " 'forall' is a well formed formula constructor", which has the statement "wff A. x ph", into which we substitute x |-> x and ph |-> ( ps -> A. x ps ).

The confusion here is that DV conditions are *assumptions*. They can be assumed in the body of the proof, and the DV conditions of a theorem are enforced whenever that theorem is applied. That means that in step 8, we would only be in trouble if there was a DV condition between x and ph in the statement of wal. You should not confuse these variables x and ph, used in wal (and not necessarily disjoint), with the x and ph from nfdv (which are disjoint), because these are in different contexts; when you apply wal in nfdv the substitution determines how one context maps to the other.

Syntax steps like wal are actually required not to have DV conditions, because otherwise there would be "stuck terms" that can't be proven well formed after substitution. To keep the grammar context free we don't want any restrictions on the term language, so wal says that you can write "A. x ph" even if ph references x. (Indeed, it's a forall binder, that's kind of the point.)

Mario

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAE4YSNSX7G8u3E91uL3eirrCGzvSF2jfnevkgHoJN6ia2_%3DP_A%40mail.gmail.com.

[Norman Megill]

In addition to Mario's comments, another way to get a feeling for when $d restrictions are needed is to temporarily delete one of them in set.mm and look at the error message, which gives explicit detail of what is being violated.  For example, if we remove "$d x ph $." above 2alimdv and try to verify the proof, we get:

MM> verify proof 2alimdv

2alimdv

?Error on line 25882 of file "set.mm" at statement 4613, label "2alimdv", type

"$p":

      ( wal alimdv ) ABEGCEGDABCEFHH $.

                                   ^

There is a disjoint variable ($d) violation at proof step 15.  Assertion

"alimdv" requires that variables "ph" and "x" be disjoint.  But "ph" was

substituted with "ph" and "x" was substituted with "x".

Variables "ph" and "x" do not have a disjoint variable requirement in the

assertion being proved, "2alimdv".

Norm