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
On Thursday, October 15, 2020 at 3:42:47 PM UTC-4 di....@gmail.com wrote:
> 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
>
> On Thu, Oct 15, 2020 at 2:37 PM 'Alexandre Frechette' via Metamath <
> meta...@googlegroups.com> wrote:
>
>> 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).
>>
>> On Thu, Oct 15, 2020 at 2:23 PM Mario Carneiro <di....@gmail.com> wrote:
>>
>>> 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?
>>>
>>> On Thu, Oct 15, 2020 at 2:09 PM 'Alexandre Frechette' via Metamath <
>>> meta...@googlegroups.com> wrote:
>>>
>>>> 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 )
>>>>
>>>> On Thursday, October 15, 2020 at 1:56:04 PM UTC-4 Alexandre Frechette
>>>> wrote:
>>>>
>>>>> 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
>>>>>
>>>> --
>>>> 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
>>>>
>>>> <https://groups.google.com/d/msgid/metamath/f14bc6d1-78d2-4cfa-b26b-5832b21ff769n%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 metamath+u...@googlegroups.com.
>>> To view this discussion on the web visit
>>> https://groups.google.com/d/msgid/metamath/CAFXXJSt%3D2QHagjU6nPCWbQO7HcbS7CXsOybgxgMfZcFKgfXXbw%40mail.gmail.com
>>>
>>> <https://groups.google.com/d/msgid/metamath/CAFXXJSt%3D2QHagjU6nPCWbQO7HcbS7CXsOybgxgMfZcFKgfXXbw%40mail.gmail.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 metamath+u...@googlegroups.com.
>>
> To view this discussion on the web visit
>> https://groups.google.com/d/msgid/metamath/CAE4YSNSX7G8u3E91uL3eirrCGzvSF2jfnevkgHoJN6ia2_%3DP_A%40mail.gmail.com
>>
>> <https://groups.google.com/d/msgid/metamath/CAE4YSNSX7G8u3E91uL3eirrCGzvSF2jfnevkgHoJN6ia2_%3DP_A%40mail.gmail.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 metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/90ac5dbf-6442-4125-8a8f-40b308ea764an%40googlegroups.com.
