[Haskell-cafe] Re: Type Eigenvariable

[oleg at pobox.com]

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.