¿Cómo desplazar cuantificadores al principio de una fórmula?

Question

Ahora mismo estoy aprendiendo sobre la forma normal prenex y tengo problemas para obtener la siguiente fórmula en forma prenex:

$\forall q (\exists x G(x,q) \longleftrightarrow \exists x L(x,q))$

Entiendo que primero tengo que reescribir la doble flecha, luego resolver las negaciones, luego renombrar las variables y finalmente mover los cuantificadores al frente. Si lo hiciera bien, los tres primeros pasos me daría esto:

$\forall q ((\exists x G(x,q) \wedge \exists y L(y,q)) \vee (\forall z \neg G(z,q) \wedge \forall w \neg L(w,q)) $

Pero lo que no consigo averiguar es cómo mover los cuantificadores al principio. Creo que los dos cuantificadores existenciales se pueden adelantar sin más, pero ¿y los dos universales? ¿Tengo que mantener su orden? Si es así, ¿puedo escribir simplemente Ex Ey Az Aw, o se omitirán los cuantificadores universales y sus variables se convertirán en constantes?

Agradecería que alguien me echara una mano.

Answer 1

Sí, puedes elegir. Tomando un ejemplo más pequeño, la fórmula $\forall x(Px) \lor \exists y(Qy)$ tiene dos diferentes formas normales prenex: $$ \forall x\exists y(Px \lor Qy) \qquad\qquad \exists y\forall x(Px \lor Qy) $$

Normalmente $\forall x\exists y$ y $\exists y\forall x$ no son intercambiables, pero en este ejemplo concreto, las dos formas normales prenex son en realidad lógicamente equivalentes, debido a la estructura especial de la fórmula bajo los cuantificadores.

En la práctica, normalmente se intentará elegir la de $\forall x\exists y$ o $\exists y\forall x$ que produzca menos cambios entre $\exists$ y $\forall$ dans le final forma prenex -- pero eso es sólo porque tal fórmula será normalmente más conveniente para seguir trabajando después, no porque la otra opción sería incorrecta.

Answer 2

Reglas.

Los "obvios":

$\forall xA(x) \land \forall x B(x) \equiv \forall x (A(x) \land B(x))$

$\exists xA(x) \lor \exists x B(x) \equiv \exists x (A(x) \lor B(x))$ .

Y:

$A \land \forall x B(x) \equiv \forall x (A \land B(x))$

$A \lor \forall x B(x) \equiv \forall x (A \lor B(x))$

$A \lor \exists x B(x) \equiv \exists x (A \lor B(x))$

$A \land \exists x B(x) \equiv \exists x (A \land B(x))$ ,

si $x$ no es gratis en $A$ .

Los "difíciles":

$A \to \forall x B(x) \equiv \forall x (A \to B(x))$

$A \to \exists x B(x) \equiv \exists x (A \to B(x))$ ,

si $x$ no es gratis en $A$ .

Y:

$\exists x A(x) \to B \equiv \forall x (A(x) \to B)$

$\forall x A(x) \to B \equiv \exists x (A(x) \to B)$ ,

si $x$ no es gratis en $B$ .

Por fin:

$\forall x A(x) \to \exists x B \equiv \exists x (A(x) \to B(x))$ .