Cómo definir nuevas constantes en el método Tableaux de la lógica de predicados

Question

Como todos sabéis, en la lógica de predicados cuando se utiliza el método Tableaux hay que eliminar los cuantificadores y sustituir sus variables por constantes dentro de las relaciones y funciones. El problema es que no sé cómo debe hacerse este proceso. He leído mucha documentación (como este o este y muchos otros archivos y páginas web) pero sigo sin poder resolver estos problemas y no sé cómo asignar las constantes. Aquí hay algunas preguntas en mi mente:

• ¿Cuál es la diferencia entre $\forall$ y $\exists$ ¿al introducir una nueva constante?

• ¿Es cierto que se puede definir la misma constante para diferentes variables? $\forall x,y R(x,y)$ con $R(a,a)$ es correcto o debe ser $R(a,b)$ ?

• ¿Bajo qué condiciones se nos permite utilizar una constante ya utilizada (definida) para una variable de un cuantificador (me refiero a que la constante se utiliza en el nodo antecesor)?

• ¿Qué restricciones hay que tener en cuenta a la hora de introducir constantes en las distintas ramas?

Por ejemplo $\exists y \exists x \forall z (C(x,y,z) \rightarrow \neg C(x,x,x))$ es inconsistente pero no pude probarlo, es la forma en que lo intenté:

$\exists y \exists x \forall z (C(x,y,z) \rightarrow \neg C(x,x,x))$

$\exists y \exists x \forall z (\neg C(x,y,z) \lor \neg C(x,x,x))$

$\exists y \exists x (\neg C(x,y,\overbrace {a} ^ {Constant}) \lor \neg C(x,x,x))$

$\exists y (\neg C(b,y,a) \lor \neg C(b,b,b))$

$(\neg C(b,d,a) \lor \neg C(b,b,b))$

y no es una contradicción mientras que estoy seguro de que esta fórmula es inconsistente.

Como otro ejemplo, este conjunto de fórmulas es consistente pero no sé cómo asignar constantes a las variables de los cuantificadores, te agradecería que me ayudaras con este conjunto.

$\{ \forall x \exists y B(x,y) \rightarrow \neg \exists y \forall x B(x,y) , \exists B(x,x) \}$

Sólo he probado esto:

$\exists B(x,x)$

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

$\neg \forall x \exists y B(x,y) \vee \neg \exists y \forall x B(x,y)$

$B(a,a)$

pero en este momento no sé si es cierto que hay que usar $a$ en su lugar si $x$ en $\neg \forall x \exists y B(x,y) \vee \neg \exists y \forall x B(x,y)$ o no (porque $a$ se utiliza en lugar de $\exists$ cuantificador en otra fórmula)?

Gracias

Answer 1

El cuantificador existencial nos permite introducir testigos - constantes ficticias, si se quiere. Por ejemplo, desde $\exists xPx$ puede escribir $Pa$ pero sólo si $a$ no existe ya.

Los nuevos cuantificadores existenciales introducirán nuevos (diferentes) testigos cada vez. Los cuantificadores universales utilizan estas constantes y testigos. Así, si una de sus premisas es $Qb$ Entonces, usted sabe que $b$ es parte de su dominio. Así que cuando veas $\forall y Ry$ sabes que esto debe ser cierto para $b$ y puedes escribir $Rb$ . Por supuesto, también puedes escribir tus enunciados universales con los testigos introducidos por los cuantificadores existenciales.

Resumiendo: los cuantificadores existenciales se utilizan para crear nuevas constantes, los cuantificadores universales sólo pueden aplicarse a constantes YA DECLARADAS (ya sea mediante premisas o cuantificadores existenciales).

Answer 2

La fórmula :

$∃y∃x∀z(C(x,y,z) → ¬C(x,x,x))$

es satisfaciendo ; considere :

1) $∃y∃x∀z(C(x,y,z) → ¬C(x,x,x))$

2) $∃x∀z(C(x,a,z) → ¬C(x,x,x))$ --- por norma para $\exists$ : $a$ nuevo

3) $∀z(C(b,a,z) \to \lnot C(b,b,b))$ --- por norma para $\exists$ : $b$ nuevo

4) $C(b,a,a) \to \lnot C(b,b,b)$ --- de 3) por regla general para $\forall$ : con $a$

5) $C(b,a,b) \to \lnot C(b,b,b)$ --- de 3) por regla general para $\forall$ : con $b$

Podemos detenernos aquí, porque podemos ver que el árbol terminará con Abrir caminos.

Para demostrar que la fórmula de 1) es satisfaciendo basta con definir un modelo $\mathfrak A$ con dominio $A = \{ a,b \}$ tal que la relación ternaria que interpreta el símbolo de predicado $C$ no es válida ni para $(b,a,a)$ ni para $(b,a,b)$ es decir $(b,a,a), (b,a,b) \notin C^\mathfrak A$ .

De este modo, vemos que : $\forall z (C(b,a,z) \to \lnot C(b,b,b))$ se cumple, porque el antecedente del condicional es falso para cualquier valor posible de $z$ .

Así, también la fórmula $∃y∃x∀z(C(x,y,z) → ¬C(x,x,x))$ es satisfaciendo .

---

---

Para el segundo ejemplo, hay que aplicar el método a :

1) $∀x∃yB(x,y) → ¬∃y∀xB(x,y)$

2) $∃B(x,x)$

Partimos de 2) con la regla para $\exists$ :

3) $B(a,a)$ --- $a$ nuevo

y entonces producimos dos ramas; la de la izquierda con :

$4_L$ ) $\lnot ∀x∃yB(x,y)$

y el derecho con :

$4_R$ ) $¬∃y∀xB(x,y)$

Ahora considera la izquierda y aplica la regla para $\lnot ∀$ :

$5_L$ ) $\lnot ∃yB(b,y)$ --- $b$ nuevo

$6_L$ ) $\lnot B(b,a)$ --- regla para $\lnot ∃$

$7_L$ ) $\lnot B(b,b)$ --- regla para $\lnot ∃$ .

Hemos encontrado el modelo $\mathfrak A$ que satisfacen 1) y 2), con dominio $A = \{ a,b \}$ tal que $(a,a) \in B^\mathfrak A$ y $(b,a), (b,b) \notin B^\mathfrak A$ .

Tenemos que : $(a,a) \in B^\mathfrak A$ satisfará $\exists xB(x,x)$ mientras que $\exists yB(b,y)$ no se satisface, y por lo tanto también $\forall x \exists yB(x,y)$ no lo es.

Por lo tanto, el antecedente del condicional 1) es falso y el condicional es verdadero.

---

---

Las reglas de gestión de los cuantificadores son bastante sencillas; véase :

• Raymond Smullyan, Lógica de primer orden (1968), página 54.

Las llamadas "Reglas C" para $\forall$ y $\lnot \exists$ debe ser instanciado con un término cualquiera, mientras que las llamadas "Reglas D" para $\exists$ y $\lnot \forall$ necesitan un nuevo plazo.

La motivación es : "Las reglas C" operan sobre $\forall$ -fórmulas prefijadas (porque $\lnot \exists$ es $\forall \lnot$ ) : por lo tanto, equivalen a la inferencia válida : si $\forall x \varphi$ entonces $\varphi^x_t$ .

Las "reglas D", en cambio, operan sobre $\exists$ -fórmulas prefijadas; así, cuando derivamos $\varphi$ de $\exists x \varphi$ no podemos reutilizar un término ya existente (en la prueba), porque la nueva hipótesis (expresada por $\exists \varphi$ ) no implica que el objeto que satisface $\varphi$ era uno de los ya "mencionados" en la prueba.