Cuando se de-Skolemizing declaraciones apropiadas?

Question

En primer orden la lógica que a menudo convertir de forma normal prenex declaraciones a la forma normal de Skolem instrucciones para eliminar el cuantificador existencial:

$\exists$x$\forall$s$\exists$z$\phi$(x,y,z) se convierte en

$\forall$x$\phi$(a,x,f(x))

Donde a es una constante de Skolem' y f es una función de Skolem'

Porque eliminamos todos los cuantificadores existencial, podemos caer todos los cuantificadores y considerar todas las variables de forma implícita universalmente cuantificado y realizar inferencias más libremente.

Esto hace las cosas más fáciles para la refutación basada automatizado de teoremas. Dado que la forma normal de Skolem es equisatisfiable a prenex forma normal, esto es totalmente apropiado para la refutación; vamos hacia abajo en la cadena de inferencias que hasta podemos saturar la búsqueda y demostrar satisfiability, o nos topamos con una contradicción y demostrar unsatisfiability, y por lo tanto la validez de la negación de la declaración en cuestión.

Podemos utilizar Skolemization para los no-refutación teoremas? El problema que más me preocupa es la forma normal de Skolem es equisatisfiable, pero no equivalente, a la forma normal prenex. Demostrando un teorema con la refutación sólo requiere equisatisfiability, pero no estoy seguro de si eso es suficiente para regular las inferencias.

Si tengo la instrucción:

$\exists$x$\forall$s$\exists$z$\phi$(x,y,z) se convierte en $\forall$x$\phi$(a,x,f(x))

$\phi$(a,x,f(x)) $\vdash$ $\psi$(a,x,f(x))

Eso no siempre implica

$\exists$x$\forall$s$\exists$z$\psi$(x,y,z)?

Si puedo realizar inferencias sobre una Skolemized declaración, puedo siempre 'de-Skolemize' las constantes de Skolem y funciones de Skolem?

Answer 1

"Si tengo la instrucción:

∃x∀y∃zϕ(x,y,z) se convierte ∀xϕ(a,x,f(x))

ϕ(a,x,f(x)) ⊢ ψ(x,f(x))

Eso no siempre implica

∃x∀y∃zψ(x,y,z)?"

Supongamos que tenemos ϕ(a,x,f(x)), y ϕ(a,x,f(x)) ⊢ ψ(x,f(x)). A continuación, podemos separar ψ(x,f(x)). La Wikpedia en Skolemization indica que funciona, ya que de equivalencias:

"Skolemization funciona mediante la aplicación de un segundo orden de la equivalencia en relación con la definición de primer orden satisfiability. La equivalencia proporciona una forma para "mover" un cuantificador existencial antes de universal."

Así, sólo tiene que utilizar las equivalencias "en la otra dirección" y terminamos con ∃x∀y∃zψ(x,y,z).

Answer 2

Este es un comentario largo ...

Respecto a tu pregunta, tenemos que tener en cuenta que :

si $\varphi := ∀x∃y \psi(x,y)$ $\varphi^S := ∀x \psi(x,f(x))$ es su skolemization, a continuación,$\varphi \nvdash \varphi^S$,

según Andreas' como respuesta a este post, mientras que son equisatisfiable.

Andreas da un argumento semántico; aquí es una prueba teórico, basado en la Deducción Natural.

---

Pensemos en el lenguaje de primer orden de la aritmética. En ella tenemos :

• (individual) variables : $x,y,\ldots$;

• una persona constante : $0$;

• una única función de símbolo : $S$ para el "sucesor" de la función;

• dos binarios de la función de los símbolos : $+$$\times$, para las operaciones de "suma" y "producto", respectivamente.

Con ellos, podemos construir términos. El siguiente :

$x, 0, S(x), S(0), x+x, x+0, x+S(0), x+S(y), \ldots$

son los términos de primer orden de la aritmética.

Considerar como $\varphi$ la fórmula :

$\forall x \exists y (x < y)$;

su skolemization $\varphi^S$ es :

$\forall x(x < S(x))$.

Las dos fórmulas son ambas verdaderas con el "estándar" de la interpretación con el dominio $\mathbb N$, y por lo tanto son equisatisfiable (es decir, ambos tienen un modelo).

Un intento de prueba de $\varphi \vdash \varphi^S$ tiene que usar la regla para $\exists$-Eliminación; véase Ian Chiswell & Wilfrid Hodges, la Lógica Matemática (2007), página 179 :

si $\Gamma, \varphi[t/y] \vdash \chi$,$\Gamma,∃y \varphi \vdash \chi$, siempre que $t$ es un símbolo constante o una variable que no ocurre en $\chi, \varphi$ o cualquier fórmula de $\Gamma$, con la excepción de $\varphi[t/y]$.

Considere ahora nuestro ejemplo :

(1) $\forall x \exists y (x < y)$ --- premise (es la única fórmula en la $\Gamma$)

(2) $\exists y (x < y)$ - - - (1) por $\forall$E

(3) $(x < S(x))$ --- asumido [a] para $\exists$E de (2) --- ilegal !

$y$ no es libre en $\Gamma$, es decir, en (1); por lo tanto podemos aplicar el $\exists$E a derivar :

(4) $(x < S(x))$ --- de (2), la descarga de asunción [a]

(5) $\forall x (x < S(x))$ - - - (4) por $\forall$I, $x$ no es libre en $\Gamma$.

La conclusión es verdadera, pero la derivación es incorrecta, porque en el paso (3) hemos utilizado para $\exists$E un plazo : $S(x)$ que es no una variable o una constante.

La condición es necesaria, a fin de evitar las falacias; si el uso de un término cualquiera es licenciado en la aplicación de la $\exists$E regla, se puede repetir la derivación con $x+0$ en lugar de $S(x)$ y nos pondremos :

$\forall x \exists y (x < y) \vdash \forall x (x < x+0)$

lo cual es claramente falso en $\mathbb N$.

---

La conclusión es, por $\varphi$ y su skolemization $\varphi^S$, que :

$\varphi \nvdash \varphi^S$

y así :

$\varphi \nvDash \varphi^S$.

Por lo tanto, en la prueba a partir de : $∃x∀y∃zϕ(x,y,z)$, tienes que tener en cuenta que usted no está autorizado a asumir que $∃x∀y∃zϕ(x,y,z) \vdash∀xϕ(a,x,f(x))$.