The first three quantifiers are substitutional, the last may be either referential or substitutional. If you think the two possibilities for the last quantifier should not be combined into a single rule, fine. I am inclined to agree, but nothing turns on that here. I have combined them only for brevity of exposition.

The variable '$\phi $' has a substitution class of formulas. The variable '$x$' is of the sort bound by the leftmost '$(\forall x)$.' It has a substitution class consisting of the variables suitable to be bound by the quantifier of the second '$(\forall x)$' Thus, for example, if the variables bound by the quantifier of the second '$(\forall x)$' include '$u$' and '$v$,' then both will be in the domain of the leftmost '$(\forall x)$' and the rightmost one will instantiate to '$(\forall u)$,' '$(\forall v)$,' and the like. The variable '$\tau $' has a substitution class of whatever objects are of the syntactically correct sort to be substituted for '$x$.' If '$x$' is an individual variable, those will be terms; if '$x$,' like '$\phi$,' is a formula with formulas as its substitution class, then '$\tau $' has formulas as its substitution class.

If you don't think all that is coherent, then so much the worse for expressing the generality of (US) using quantification. I have put these problems into the category of niceties to be passed over because I wish to emphasize a different problem.

-- ShaughanLavine - 16 Mar 2005