# Quantifiers for mutually distinct variables

Okay, this is freaking me out, I'm going nuts. In a first-order condition with formula $\phi$ containing $x, y$ such as

$\forall x\forall y . \phi$

I need to ensure that the second variable bound by the universal quantifier can only take values that are distinct from those of the first variable bound by the first universal quantifier respectively, but I do not know how to write this down cleanly as a formula. I need something like

$\forall x\in D\,\forall y\in D-\{x\}.\phi$

but this does not seem to be the proper way of writing it down either (although I've seen this in CS papers). It mixes up variables with their interpretation and only hints at the intended dependence. You might think that the textbook restriction

$\forall x\,\forall y. x\neq y\to\phi$

would do the trick but it doesn't seem to work. If $x=y$, then the condition ought to be false or undefined, but not vacuously true. However, $\phi$ contains an anti-reflexive relation, so with unrestricted quantification the whole condition could never be true, which is not right either. I rather need this: "The condition is true if for all distinct $x$ and $y$, $\phi$ is true, otherwise it is false." - but as a formula, not as paraphrase!

I've looked up branching quantifiers and IF logic, but they seem to do the opposite, allowing one to express independence between quantifiers rather than additional dependencies. I suspect I have overlooked something very basic and simple, but what?

• $(\forall x \in D)(\forall y \in D - \{x\}) \phi$ is actually just an abbreviation for $(\forall x \in D)(\forall y \in D)(y \not = x \to \phi)$. So the first won't work if the second doesn't. Both of those do have the property that they hold if and only if, for all distinct $x$ and $y$, $\phi(x,y)$ holds. But I still do not know, from the question, what exactly you are trying to accomplish, so I cannot yet write an answer. Apr 2 '15 at 12:34
• I need the condition as a whole to be false if $D=\{a\}$. Apr 2 '15 at 13:51
• You cannot have a sentence that is some case is true, "otherwise it is false." A sentence has a definite truth-value : TRUE or FALSE. A formula like $x \ne y \land \phi$ is FALSE when $x=y$ and has the same truth-value of $\phi$ when $x \ne y$. But if we universally quantify it, the result : $\forall x \forall y (x \ne y \land \phi)$ is FALSE. Apr 2 '15 at 13:53

If the goal is to avoid a model with only one element, why not just prepend $(\exists x)(\exists y)[x \not = y]$ to the front, and then use the definition that you like for models that have more than one element?