¿Cuál es la diferencia en los procedimientos de prueba por resolución en los siguientes escenarios?

Question

No estoy seguro de cuál es la diferencia en la prueba por resolución en los dos escenarios siguientes, uno de los cuales es un implica, el otro es un conlleva:

$(\exists y\forall x P(x, y)) \to (\forall x\exists y P(x, y))$

$(\exists y\forall x P(x, y)) \vdash (\forall x\exists y P(x, y))$

¿Sigues el mismo procedimiento en ambos casos para demostrar la validez, es decir, negando la RHS y tratando los procedimientos de skolemisation por separado?

Gracias.

Answer 1

En primer lugar, habrá una diferencia en el punto de partida. En el primer caso, se niega todo el condicional, mientras que en el segundo se afirma la premisa y se niega la conclusión.

En segundo lugar, pueden producirse otras diferencias después de eso, pero exactamente qué tipo de diferencias dependerá del orden de los pasos que utilice para generar las cláusulas. Por ejemplo, una vez que hayas negado el condicional en el primer caso:

$$\neg (\exists y \forall x \ P(x,y) \rightarrow \forall x \exists y \ P(x,y))$$

puedes reescribirlo como una conjunción:

$$\exists y \forall x \ P(x,y) \land \neg (\forall x \exists y \ P(x,y))$$

y ahora el movimiento "inteligente" (y perfectamente legal) sería simplemente dejar el $\land$ y continuar con el proceso con lo que resultan ser las mismas dos declaraciones que se obtienen al inicio del segundo caso: $\exists y \forall x \ P(x,y)$ y $\neg \forall x \exists y \ P(x,y)$

Sin embargo, en lugar de abandonar el $\land$ También puede (de hecho, algunos algoritmos en este punto dictar esto) sacar los cuantificadores ... lo que implica renombrar las variables ... lo que podría (dependiendo del orden en que se saquen los cuantificadores) terminar con:

$$\exists y \forall x \exists x' \forall y' (P(x,y) \land \neg P(x',y'))$$

... y ahora necesitas usar una función $f(x)$ al skolemizar el $\exists x'$ algo que podría haberse evitado.

Respuesta larga y corta: la diferencia entre los dos casos podría ser trivial, pero también podría ser más sustancial .... Depende del orden de los pasos dados para generar las eventuales cláusulas.