Nivel 3 · Lógica y deducción natural

Demostrabilidad: deducción natural

La relación entre prueba y verdad en la lógica proposicional clásica se aborda desde dos planos complementarios. El plano sintáctico, regido por el símbolo de derivabilidad ( $\vdash$ ), trata la manipulación de símbolos según reglas de inferencia fijas: una fórmula es demostrable si existe una derivación formal que la produce. El plano semántico, regido por el torniquete ( $\vDash$ ), trata el significado y la verdad: una fórmula es consecuencia lógica si es verdadera en todo modelo de sus premisas. Esta página desarrolla el primero mediante la deducción natural ; la siguiente desarrolla el segundo, y las dos posteriores demuestran que ambos coinciden. La presentación sigue a Huth y Ryan (2004) .

Nota 9.1 (Convenciones)

Se escribe $\vdash$ para «demuestra» y $\vDash$ para «implica semánticamente»; $\Gamma$ denota un conjunto finito de premisas y «tautología» abrevia $\vDash\varphi$ . En la formalización en Lean (nivel 7, próximamente) esta misma relación de derivabilidad se realiza como un predicado inductivo (escrito $\Provnd$ ) y la satisfacción semántica como una función eval.

El lenguaje

La noción central del plano sintáctico es la de prueba formal: una secuencia de pasos válidos en un sistema dado, que aquí será la deducción natural. El lenguaje se construye sobre enunciados atómicos y los conectivos que los combinan.

Proposiciones atómicas: enunciados declarativos indivisibles, denotados $p, q, r, \ldots$ (por ejemplo, $p$ : «el tren llega tarde»).
Fórmulas: una proposición atómica o una expresión construida con conectivos; se usan $\phi, \psi, \chi$ para fórmulas arbitrarias.
Conectivos: negación $\neg$ , conjunción $\wedge$ , disyunción $\vee$ e implicación $\rightarrow$ . En $\phi\rightarrow\psi$ , $\phi$ es el antecedente y $\psi$ el consecuente.

Nota 9.2 (El fragmento mínimo {¬, →})

Aunque aquí se presentan los cuatro conectivos, $\wedge$ , $\vee$ y la constante $\bot$ son definibles a partir de $\neg$ y $\rightarrow$ (como se verifica con tablas de verdad):

\phi\vee\psi \;\equiv\; \neg\phi\rightarrow\psi, \qquad \phi\wedge\psi \;\equiv\; \neg(\phi\rightarrow\neg\psi), \qquad \bot \;\equiv\; \neg(\phi\rightarrow\phi).

Toda fórmula del lenguaje completo se traduce así al fragmento sin perder ni ganar tautologías, de modo que $\{\neg,\rightarrow\}$ basta para la lógica clásica. El estudio de esta «lógica mínima» con una sola implicación es clásico (Sørensen y Urzyczyn, 2006) . La formalización en Lean del nivel 7 trabaja exactamente en este fragmento $\{\neg,\rightarrow\}$ , de modo que las definiciones de esta página son su contraparte matemática directa.

Secuentes y teoremas

En deducción natural una prueba muestra cómo una conclusión se sigue de un conjunto de premisas. Esa relación se captura mediante un secuente.

Definición 9.3 (Secuente y demostrabilidad)

Un secuente es una expresión $\phi_1, \ldots, \phi_n \vdash \psi$ , donde $\{\phi_1, \ldots, \phi_n\}$ es un conjunto (posiblemente vacío) de premisas y $\psi$ es la conclusión. El secuente es válido si existe una prueba en deducción natural que deriva $\psi$ usando únicamente esas premisas y las reglas de inferencia; tal validez se denota escribiendo el secuente con $\vdash$ .

Definición 9.4 (Teorema)

Una fórmula $\phi$ es un teorema si el secuente $\vdash \phi$ es válido, es decir, si $\phi$ se demuestra sin premisas. Los teoremas son las verdades lógicas que se sostienen por la estructura misma de la lógica.

Las reglas de inferencia

Las reglas se dividen en introducción (crean un conectivo) y eliminación (usan un conectivo para derivar algo más). En los esquemas siguientes, la caja vertical indica una suposición temporal: la fórmula superior se asume, de ella se deriva la inferior, y al aplicar la regla la suposición se descarga (deja de ser una premisa pendiente).

Conjunción ( $\wedge$ )

Introducción ( $\wedge\mathrm{i}$ ): de $\phi$ y $\psi$ se concluye $\phi \wedge \psi$ . Eliminación ( $\wedge\mathrm{e}$ ): de $\phi \wedge \psi$ se concluye $\phi$ o $\psi$ .

\dfrac{\phi \quad \psi}{\phi \wedge \psi}\ \wedge\mathrm{i} \qquad\qquad \dfrac{\phi \wedge \psi}{\phi}\ \wedge\mathrm{e}_1 \qquad\qquad \dfrac{\phi \wedge \psi}{\psi}\ \wedge\mathrm{e}_2

Implicación ( $\rightarrow$ )

Eliminación ( $\rightarrow\mathrm{e}$ ), o modus ponens: de $\phi$ y $\phi \rightarrow \psi$ se concluye $\psi$ . Introducción ( $\rightarrow\mathrm{i}$ ): para probar $\phi \rightarrow \psi$ se supone $\phi$ temporalmente y se deriva $\psi$ ; al cerrar, la suposición se descarga.

\dfrac{\phi \quad \phi \rightarrow \psi}{\psi}\ \rightarrow\mathrm{e} \qquad\qquad \dfrac{\begin{array}{|l} \phi \\ \vdots \\ \psi \end{array}}{\phi \rightarrow \psi}\ \rightarrow\mathrm{i}

Disyunción ( $\vee$ )

Introducción ( $\vee\mathrm{i}$ ): de $\phi$ se concluye $\phi \vee \psi$ para cualquier $\psi$ . Eliminación ( $\vee\mathrm{e}$ ), o prueba por casos: si se tiene $\phi \vee \psi$ y una conclusión $\chi$ se sigue tanto de suponer $\phi$ como de suponer $\psi$ , entonces se concluye $\chi$ .

\dfrac{\phi}{\phi \vee \psi}\ \vee\mathrm{i}_1 \qquad \dfrac{\psi}{\phi \vee \psi}\ \vee\mathrm{i}_2 \qquad\qquad \dfrac{\phi \vee \psi \quad \begin{array}{|l} \phi \\ \vdots \\ \chi \end{array} \quad \begin{array}{|l} \psi \\ \vdots \\ \chi \end{array}}{\chi}\ \vee\mathrm{e}

Negación ( $\neg$ ) y contradicción ( $\bot$ )

El símbolo $\bot$ («falsum») representa una contradicción lógica, como $p \wedge \neg p$ . Eliminación de negación ( $\neg\mathrm{e}$ ): de $\phi$ y $\neg\phi$ se concluye $\bot$ . Eliminación de contradicción ( $\bot\mathrm{e}$ ): de $\bot$ se concluye cualquier $\phi$ (principio de explosión). Introducción de negación ( $\neg\mathrm{i}$ ): para probar $\neg\phi$ se supone $\phi$ y se deriva $\bot$ .

\dfrac{\phi \quad \neg\phi}{\bot}\ \neg\mathrm{e} \qquad\qquad \dfrac{\bot}{\phi}\ \bot\mathrm{e} \qquad\qquad \dfrac{\begin{array}{|l} \phi \\ \vdots \\ \bot \end{array}}{\neg\phi}\ \neg\mathrm{i}

Reglas derivadas y el principio clásico

Las reglas anteriores forman el núcleo intuicionista. De las que siguen, el modus tollens sí se deriva de ese núcleo; en cambio la reducción al absurdo (RAA) y el medio excluido (LEM) no son derivables de él: son principios adicionales que, al incorporarse, vuelven clásica a la lógica.

Modus tollens (MT): de $\phi \rightarrow \psi$ y $\neg\psi$ se concluye $\neg\phi$ . Reducción al absurdo (RAA), o prueba por contradicción (PBC): para probar $\phi$ se supone $\neg\phi$ y se deriva una contradicción $\bot$ . Ley del medio excluido (LEM): para toda $\phi$ , el enunciado $\phi \vee \neg\phi$ es un teorema, introducible en cualquier línea.

\dfrac{\phi \rightarrow \psi \quad \neg\psi}{\neg\phi}\ \mathrm{MT} \qquad\qquad \dfrac{\begin{array}{|l} \neg\phi \\ \vdots \\ \bot \end{array}}{\phi}\ \mathrm{RAA} \qquad\qquad \phi \vee \neg\phi \quad \mathrm{LEM}

Nota 9.5 (La regla clásica que se formaliza)

RAA, LEM y la eliminación de la doble negación ( $\neg\neg\phi\vdash\phi$ ) son inter-derivables: añadir cualquiera de ellas al núcleo intuicionista produce la lógica clásica. El cálculo formalizado en Lean en el nivel 7 (próximamente) toma como única regla clásica precisamente la reducción al absurdo sobre el fragmento $\{\neg,\rightarrow\}$ , que es lo justo y necesario para la completitud respecto de la semántica clásica.

Equivalencia demostrable

Con estas reglas se introduce la equivalencia demostrable.

Definición 9.6 (Equivalencia demostrable)

Dos fórmulas $\phi$ y $\psi$ son demostrablemente equivalentes, escrito $\phi \dashv\vdash \psi$ , si los secuentes $\phi \vdash \psi$ y $\psi \vdash \phi$ son ambos válidos.

Esto formaliza la idea de que ambas fórmulas tienen el mismo «poder deductivo»: una aparición de $\phi$ puede reemplazarse por $\psi$ y viceversa. Un ejemplo central es la equivalencia entre una implicación y su contrapositiva.

Proposición 9.7

$p \rightarrow q \dashv\vdash \neg q \rightarrow \neg p$ .

Demostración.

Se prueban ambas direcciones del secuente.

$p \rightarrow q \vdash \neg q \rightarrow \neg p$ , con las reglas de implicación y negación del núcleo intuicionista: se supone $\neg q$ (para $\rightarrow\mathrm{i}$ ) y, dentro, se supone $p$ (para $\neg\mathrm{i}$ ); con $\rightarrow\mathrm{e}$ sobre la premisa se obtiene $q$ , con $\neg\mathrm{e}$ se obtiene $\bot$ , y las dos suposiciones se descargan sucesivamente con $\neg\mathrm{i}$ y $\rightarrow\mathrm{i}$ .
$\neg q \rightarrow \neg p \vdash p \rightarrow q$ , usando RAA para deducir $q$ : se supone $p$ (para $\rightarrow\mathrm{i}$ ) y, dentro, se supone $\neg q$ (para RAA); con $\rightarrow\mathrm{e}$ sobre la premisa se obtiene $\neg p$ , con $\neg\mathrm{e}$ se obtiene $\bot$ , RAA descarga $\neg q$ y concluye $q$ , y $\rightarrow\mathrm{i}$ descarga $p$ .

Las dos derivaciones completas, línea por línea y con sus cajas de Fitch, se recorren en el explorador de abajo. Probadas ambas direcciones, $p \rightarrow q \dashv\vdash \neg q \rightarrow \neg p$ .

Recórrelas tú mismo

El explorador contiene tres derivaciones: la identidad $\vdash p \rightarrow p$ y las dos direcciones de la Proposición 9.7. Cada línea muestra la regla que la justifica, y el mismo argumento puede verse en estilo Fitch (cajas) o como árbol de inferencias. Obsérvese dónde aparece la regla clásica: solo en la dirección $\neg q \rightarrow \neg p \vdash p \rightarrow q$ , exactamente como en la demostración anterior.

Explorador de deducción natural

A demostrar: $\vdash p \rightarrow p$

p

suposición (para →i)

1 / 2

suposición (para →i): Abre una caja: la fórmula se asume temporalmente y DEBERÁ descargarse.

Hasta aquí la sintaxis: derivar sin preguntarse qué significan las fórmulas. La página siguiente construye el plano opuesto, la verdad definida por tablas, y prepara los dos puentes que los conectan.