20 Jan
2006
20 Jan
'06
12:48 a.m.
On Thu, 2006-01-19 at 19:18 -0800, oleg@pobox.com wrote: . . .
_variables_. The paper argues, btw, for the separation of those senses and for a new quantifier to mean uniqueness only. In short, when we write forall x. forall y. body then x may well be equal to y (in body). And so, forall x. forall y. B[x,y] ====> forall z. B[z,z] OTH, when we write |nabla x. nabla y. body| then x and y are guaranteed to be different, and so the implication above no longer holds.
OK, I gotta ask: 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|. -- Bill Wood