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 < [email protected]> 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 [email protected]. > 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSt%3D2QHagjU6nPCWbQO7HcbS7CXsOybgxgMfZcFKgfXXbw%40mail.gmail.com.
