Intentando comprender las reglas de inferencia del Cálculo Secuencial para cuantificadores $\forall$ y $\exists$ .

Question

Estoy tratando de entender LK cálculo secuencial (lógica) reglas de inferencia para cuantificadores (si comprendo una lo suficientemente bien, quizá pueda utilizarla para comprender las otras tres). En Wikipedia las reglas son:

$L$

$R$

$\forall$

$$\Gamma, A[t/x] \vdash \Delta \over \Gamma, \forall xA \vdash \Delta$$

$$\Gamma \vdash A[y/x], \Delta\over \Gamma \vdash \forall xA, \Delta$$

$\exists$

$$\Gamma, A[y/x] \vdash \Delta \over \Gamma, \exists xA \vdash \Delta$$

$$\Gamma \vdash A[t/x], \Delta \over \Gamma \vdash \exists xA, \Delta$$

El artículo de Wikipedia dice lo siguiente sobre estas normas:

Para intuir las reglas de cuantificación, considere la regla $({\forall }R)$ . Por supuesto, concluir que $\forall{x} A$ se sostiene sólo por el hecho de que $A[y/x]$ es cierto no es en general posible. Sin embargo, si la variable y no se menciona en ninguna otra parte (es decir, si se puede elegir libremente, sin influir en las demás fórmulas), se puede suponer que $A[y/x]$ es válida para cualquier valor de $y$ . Las demás normas deberían ser bastante sencillas.

(Primera pregunta: Las reglas de inferencia utilizan tanto $A[t/x]$ y $A[y/x]$ . ¿Existe alguna diferencia entre $A[t/x]$ y $A[y/x]$ ? Lo sé. $t$ denota convencionalmente un término. ¿Tiene $y$ también )

El mismo artículo de Wikipedia indica el significado de la notación $A[t/x]$ :

$A[t/x]$ denota la fórmula que se obtiene sustituyendo el término $t$ para cada aparición libre de la variable $x$ en fórmula $A$ con la restricción de que el término $t$ debe estar libre para la variable $x$ en $A$ (es decir, ninguna aparición de cualquier variable en $t$ se convierte en $A[t/x]$ ).

También debe tenerse en cuenta que en el cálculo secuencial

• a plazo $t$ no tiene cuantificadores (ni aglutinantes), por lo que todas sus variables son libres
• una fórmula $A$ pueden tener cuantificadores. También puede tener variables libres. Por lo tanto, puede tener variables ligadas y variables libres.

---

Por qué son las reglas de la forma:

$$\Gamma, A[t/x] \vdash \Delta \over \Gamma, \forall xA \vdash \Delta$$

en lugar de la forma

$$\Gamma, A \vdash \Delta \over \Gamma, \forall xA \vdash \Delta$$

¿Por qué son necesarias las sustituciones? Para una norma concreta, ¿garantiza la sustitución que $x$ ¿es una variable libre?

Answer 1

Porque nosotros no sólo quieren dar una bofetada de " $\forall x$ " en el anverso de la fórmula $A$ . (Para simplificar, a continuación trabajo con $\Gamma=\emptyset$ y $\Delta$ una única fórmula, a saber $\Delta=\exists xU(x)$ .)

Por ejemplo, supongamos $A$ es la fórmula $U(c)$ donde $U$ es un símbolo de predicado unario y $c$ es un símbolo constante. Del secuente $$U(c)\vdash\exists xU(x)$$ (cuya derivación dejo como ejercicio) nos gustaría inferir el secuente $$\forall xU(x)\vdash \exists xU(x).$$ Sin embargo, su versión del ${\forall}L$ regla sólo nos daría $$\forall xU(c)\vdash\exists xU(x),$$ y esto no es en absoluto lo mismo.

Answer 2

Usted tuvo una observación cuidadosa para la diferencia entre el término arbitrario $t$ y una variable arbitraria $y$ utilizado en las 4 reglas de cuantificación de $LK$ . De hecho hay algún propósito para esta diferencia intencionalmente en la mayoría de los cálculos secuenciales.

Recall $\forall$ L corresponde implícitamente a $\forall$ -elim de deducción natural, por lo que si $A$ se cumple para cada objeto, entonces podemos sustituir cualquier término $t$ por compleja que sea, en $A$ para $x$ (por supuesto asumiendo $t$ es gratuito para $x$ en $A$ ), y entonces si todavía podemos derivar $\Delta$ es cuando $\forall$ L tiene sentido. A la inversa, $\forall$ R corresponde a $\forall$ -en ND, por lo que necesitamos una regla arbitraria de solo variable $y$ (suponiendo $y$ no se menciona en ninguna otra parte) para sustituir a $x$ en $A$ como resultado de $\Gamma$ como el caso más genérico para introducir $\forall x A$ .

Y curiosamente, para el $\exists$ cuantificador las situaciones se invierten ya que en el caso de introducción ( $\exists$ Regla R) normalmente una variable genérica $y$ no tendrá derecho a derivar $A(y)$ de $\Gamma$ hay que esforzarse para encontrar un término específico $t$ satisfaciendo $\Gamma \vdash A[t/x]$ . Un razonamiento similar para $\exists$ Regla L.

Por último, si comprende $\forall$ L regla como $\forall$ -elim de la deducción natural, entonces puedes ver fácilmente del mismo razonamiento anterior que tienes que probar $\Delta$ de $\Gamma$ y $A[t/x]$ para un término arbitrario, sólo entonces $\forall$ L tiene sentido y se mantiene.