Conversión de fórmulas a la forma Skolem.

Question

Estoy intentando convertir las dos fórmulas siguientes a su forma Skolem. Hice mi trabajo, pero no completamente seguro acerca de ellos, y tengo algunas preguntas acerca de algunos pasos de Skolemization:

Fórmula 1: xyzw (¬Q(f(x),y) P(a,w))

Paso 1: xyzw (¬Q(f(x),y) P(a, w)) (¿ya rectificado?)

Paso 2: x ₁ x y w (¬Q(f(x), y) P(x ₁ w)) (¿rectificado y cerrado + RPF?)

Paso 3: x (¬Q(f(x), g(x)) P(a, h(x)) (¿Forma de Skolem?)

Fórmula 2: z(y(P(x,g(y),z))¬xQ(x))

Paso 1: z(y(P(x, g(y), z)) ¬x ₁ Q(x ₁ )) (¿rectificado?)

Paso 2: xz (y (P(x, g(y), z)) ¬x ₁ Q(x ₁ )) (¿rectificado + cerrado?)

Paso 3: xzyx ₁ ((P(x, g(y), z) ¬Q(x ₁ )) (RPF?)

Paso 4: z ((P(a), g(f(z)), z) ¬Q(h(z)) (¿Skolem?)

Mi primera pregunta es, en la primera fórmula, la variable z no aparece en la fórmula, por lo tanto, ¿podemos eliminarla directamente con su cuantificador?

Otra pregunta es, cuando ligamos las variables libres, las ligamos con un cuantificador existencial. ¿Deberíamos añadir el cuantificador existencial de las variables libres al principio de la lista de cuantificadores? (por ejemplo, en la segunda fórmula, en el paso 2, usamos el cuantificador existencial para ligar x, y yo añadí x al principio de toda la fórmula, ¿es ese el caso?)

Me alegraría mucho si pudieras ayudarme con estas situaciones. También agradecería cualquier comentario sobre el proceso de Skolemización. Muchas gracias de antemano.

Answer 1

Las presentaciones habituales de la lógica de predicados de primer orden permiten sintácticamente la cuantificación vacua.Al reescribir una fórmula suprimiendo el cuantificador de ligadura vacua, la fórmula queda lógicamente equivalente. Por lo tanto, es apropiado eliminar el cuantificador $\forall z$ a partir de la fórmula

$$\forall x\exists y\forall z\exists w(\neg Q(f(x),y)\wedge P(a,w))$$

---

En cuanto a la siguiente pregunta, supongamos que tenemos una fórmula rectificada $\phi(x_{1},x_{2}\ldots, x_{n}, y_{1}, y_{1}\ldots, y_{m})$ en el que las variables $y_{k}$ es decir, gratis, $\phi$ ya es una fórmula abierta.

El siguiente paso es elaborar una fórmula cerrada $\phi'$ que sea satisfactoriamente equivalente a $\phi$ . Entonces, cuantificamos existencialmente todas las variables libres y obtenemos

$$\exists y_{1}\exists y_{2}\cdots\exists y_{m}\phi(x_{1}, x_{2}\ldots, x_{n}, y_{1}, y_{2}\ldots, y_{m})$$

Este es el procedimiento adecuado. Nótese que, con la Skolemisación, buscamos la igualabilidad con la fórmula original, no la equivalencia lógica más estricta con ella. Por lo tanto, se podría elegir entre alternativas en el procedimiento siempre que preserven la satisfabilidad. Hay que tener en cuenta que existe la práctica de tratar las variables libres como cuantificadas universalmente para eliminar después todos los cuantificadores universales y obtener la forma normal clausal.

Answer 2

Sí, puede soltar el $\forall z$ en el $\forall x \exists y \forall z \exists w (¬Q(f(x),y) \land P(a,w))$ fórmula

Además, no hay necesidad de introducir un existencial para una constante ... sólo para tener que cambiar de nuevo por una constante más tarde. Puedes simplemente dejar la constante.

Por lo tanto, para la primera, se puede ir de

$$\forall x \exists y \forall z \exists w (¬Q(f(x),y) \land P(a,w))$$

a

$$\forall x \exists y \exists w (¬Q(f(x),y) \land P(a,w))$$

a

$$\forall x \exists y \exists w (¬Q(f(x),g(x)) \land P(a,h(x)))$$

La variable libre $x$ en la segunda fórmula también se puede mantener solo .. tener una variable libre es típicamente tratado más como un universal que un existencial por lo que definitivamente don;t quiere introiduce un existencial para él. Así que aquí, usted puede ir de

$$\forall z(\exists y(P(x,g(y),z))\lor \neg \forall x Q(x))$$

a

$$\forall z \exists y(P(x,g(y),z)\lor \exists x \neg Q(x))$$

a

$$\forall z \exists y(P(x,g(y),z)\lor \exists x_1 \neg Q(x_1))$$

a

$$\forall z \exists y \exists x_1 (P(x,g(y),z)\lor \neg Q(x_1))$$

a

$$\forall z (P(x,g(f(z)),z)\lor \neg Q(h(z)))$$