Double quantification of the same type and variable?

82 Views Asked by At

If we have the following laws:

$\exists x S(x) \land T(y)$ is logically equivalent to $\exists x ( S(x) \land T(y))$

and

$ S(x) \land \exists y T(y)$ is logically equivalent to $\exists y ( S(x) \land T(y))$

Then, does the following make sense?:

$\exists a S(a) \land \exists x T(a)$ is logically equivalent to $\exists a (S(a) \land T(a))$

And what about for other connectors? Like $\implies$ and $\lor$? Does it also work, or is it different?

1

There are 1 best solutions below

0
On

No, you cannot ignore the second $\exists$. First of all, the two $a$ in the formula represent 2 different variables. So rename one to avoid a conflict:

$$(\exists a~Sa) \land (\exists b~ Tb)$$

Now you can apply the prenex rule and get:

$$\bigg((\exists a~Sa) \land (\exists b~ Tb)\bigg) \iff \exists a~(Sa \land (\exists b~ Tb))$$

There is a different (unrelated) transform, which is a consequence of how $\exists$ is just generalized $\lor$, where you can say:

$$\bigg((\exists a~Sa) \lor (\exists b~ Tb)\bigg) \iff \exists c~(Sc \lor Tc)$$

In any of these formulas (in binary logic), if you swap the $\land$s and $\lor$s, and swap $\forall$s and $\exists$s, you will also get a valid formula:

$$\bigg((\forall a~Sa) \lor (\forall b~ Tb) \bigg) \iff \forall a~(Sa \lor (\forall b~ Tb))$$