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
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
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
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
