# Transform the given formula $(\exists{x})a(x) \Leftrightarrow (\forall{x})\ b(x,y)$ …

Transform the formula, so that all the quantifiers are at the beginning $$(\exists{x})a(x) \Leftrightarrow (\forall{x})\ b(x,y)$$

I tried to do it this way: $$((\exists{x})a(x) \Leftrightarrow \forall{x}\ b(x,y))\Leftrightarrow \lnot (\forall{x} \lnot a(x)) \Leftrightarrow (\forall{z})\ b(z,y) \Leftrightarrow (\lnot (\forall{x}))(\forall{z})(a(x)\Leftrightarrow b(z,y)).$$

But I am pretty sure it's wrong and the negation can't be extracted this way. Can anyone help me with this?

-

Let's assume you indeed meant the unquantified $y$. Then

$$(\exists{x})a(x) \leftrightarrow (\forall{x})\ b(x,y)$$

is equivalent to

$$[(\exists{x})a(x) \rightarrow (\forall{z})\ b(z,y)] \land [(\forall{u})\ b(u,y) \rightarrow (\exists{v})a(v)]$$

is equivalent to

$$(\forall{x})(\forall{z})[a(x) \rightarrow \ b(z,y)] \land (\exists{u})(\exists{v})[b(u,y) \rightarrow a(v)]$$

is equivalent to

$$(\forall{x})(\forall{z})(\exists{u})(\exists{v})\{[a(x) \rightarrow \ b(z,y)] \land [b(u,y) \rightarrow a(v)]\}$$

though indeed, in this special sort of case, the now initial quantifiers can be reordered.

-
Thank you, Peter. I've gone without sleep far too long! I think I made amends! – amWhy Nov 18 '12 at 23:23

You have $$((\exists{x})a(x) \Leftrightarrow \forall{x}\ b(x,y))\Leftrightarrow \lnot (\forall{x} \lnot a(x)) \Leftrightarrow (\forall{z})\ b(z,y) \Leftrightarrow (\lnot (\forall{x}))(\forall{z})(a(x)\Leftrightarrow b(z,y))$$

There is no reason to "doubly negate" the existential quantifier when moving from your first to second implication. Furthermore, care must be taken when extracting quantifiers from a quantified antecedent of an implication, and moving those quantifiers to the front of the entire implication.

Precision is everything, in logic (and in math)!

It would be much more straightforward to simply proceed as follows, starting with the statement you want to transform:

Assuming $y$ is not quantified, i.e., treating $y$ is a constant, we have:

$$(\exists{x})a(x) \Leftrightarrow (\forall{x})\ b(x,y)\tag{1}$$

Then $(1)$ is equivalent to the conjunction of two implications, each of which needs distinct variables, we'll use $x$ and $z$ for the forward direction, and $s, t$ for the reverse direction:

$$[(\exists{x})a(x) \rightarrow (\forall{z})\ b(z,y)] \land [(\forall{s})\ b(s,y) \rightarrow (\exists{t})a(t)]\tag{2}$$

Given that we want to pull out the existential quantifier from the antecedent of first implication, we need to change it to a univeral quantifier of the variable $x$; likewise we need to reverse the existential quantifier in the antecedent of the second implication. With this in mind, $(2)$ is equivalent to

$$(\forall{x})(\forall{z})[a(x) \rightarrow \ b(z,y)] \land (\exists{s})(\exists{t})[b(s,y) \rightarrow a(t)]\tag{3}$$

Now we can pull the quantifiers to the front; that is, $(3)$ is equivalent to

$$(\forall{x})(\forall{z})(\exists{s})(\exists{t})\{[a(x) \rightarrow \ b(z,y)] \land [b(u,y) \rightarrow a(v)]\}\tag{4}$$

-
That's not right -- you are forgetting that pulling a quantifier out from the antecedent of a conditional flips it to its dual. – Peter Smith Nov 18 '12 at 22:48
It's all good, I believe. – amWhy Nov 19 '12 at 2:06