Demostración del teorema de la deducción en el cálculo secuencial

Question

¿Puede alguien recomendarme un texto, donde el teorema de deducción para la lógica de predicados se demuestra en LK ? Me refiero a la siguiente proposición:

si $A$ es una fórmula cerrada, y $B$ es arbitraria, entonces la existencia de un árbol de Gentzen $$ \frac{\frac{\vdash A}{\dots}}{\vdash B} $$ implica la deducibilidad del secuente $A\vdash B$ (o, equivalentemente, la deducibilidad del secuente $\vdash A\to B$ ).

De forma más general, me pregunto si existen libros de texto de lógica en los que la exposición se presente desde el punto de vista del cálculo secuencial.

Answer 1

En el cálculo secuencial, el Teorema de la Deducción es simplemente el $(\supset \text{Right})$ regla :

\begin{align} \frac{C, \Gamma \to \Delta, D}{\Gamma \to \Delta, C \supset D} (\supset \text R) \end{align}

Ver : Gaisi Takeuti, Teoría de la prueba (2ª ed., 1987), página 10. En general, es un excelente libro dedicado al cálculo secuencial.

También puede ver : Sara Negri y Jan von Plato, Teoría de la prueba estructural , Cambridge UP (2001).

Nota sobre el simbolismo : He seguido a Takeuti en el uso de $\supset$ para el condicional conentivo ("si..., entonces...") y $\to$ para el "símbolo auxiliar" utilizado en el secuencias : $\Gamma \to \Delta$ .

---

---

Añadido (tras el comentario de Henning).

Asumimos tener una prueba de $B$ es decir, una derivación en el cálculo del secuente : $\to B$ .

Aplicamos $(\text {Weakening Left})$ para obtener : $A \to B$ seguido de $(\supset \text{Right})$ para concluir con el secuente : $\to (A \supset B)$ .

En cuanto a los cuantificadores, el $(\forall \text { Right})$ La regla es [ver página 10] :

\begin{align} \frac{\Gamma \to \Delta, F(a)}{\Gamma \to \Delta, \forall x F(x)} (\forall \text { R}) \end{align}

con la restricción : $a$ no ocurre en el secuencial inferior.

Esto significa que no podemos utilizar la derivación :

\begin{align} \frac{F(a) \to F(a)}{\to F(a) \supset \forall x F(x)} (\forall \text { R}) \end{align}

para derivar los inválidos $F(a) \supset \forall x F(x)$ .