Bill Wood wrote:
is |nabla x, nabla y. phi(x,y)| logically equivalent to |forall x, forall y. x <> y only-if phi(x,y)|? I use |P only-if Q| for |P materially implies Q|
First of all, I should remark that Miller and Tiu introduce two calculi (with names that are hardly speakable, even in TeX). One of them is the sequent calculus with globally and locally scoped eigen-variables and the _open_ world of predicates. The other, calculus of definitions, uses the _closed_ world of predicates (the authors neglect to emphasize the closedness, btw). Universal and existentials quantifiers deal with eigenvariables of the global scope; only nabla can affect the locally scoped eigen variables. Also, the only rules that can irrevocable destroy/create locally scoped variables are "False --> X" and "X --> True". Because of these properties, nabla quantification in the open world neither implies nor implied by the universal quantification (ditto for the existential). So, the answer to your question for the open world calculus is no. In the closed world, the matters are muddier and depend on the predicates in the closed world. If we manage to reduce our sequent to the form, "X --> Y" where X has no definition, then, by closed world property, we proved the sequent (regardless of how many locally-scoped variables we have there). So, we can in some cases replace quantifiers. I must acknowledge Chung-chieh Shan for helpful discussions on these matters.