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.
