Nivel 3 · Lógica y deducción natural

Completitud: el argumento de Kalmár

La recíproca de la solidez es el resultado más profundo de este nivel y el que se formaliza en Lean: el sistema es lo bastante expresivo para demostrar todas las verdades semánticas. Esta propiedad es la completitud , y el argumento que la demuestra, debido a Kalmár (Kalmár, 1935) , tiene la virtud de ser completamente explícito.

Teorema 9.12 (Completitud de la lógica proposicional)

Si $\Gamma \vDash \psi$ (con $\Gamma = \{\phi_1, \ldots, \phi_n\}$ ), entonces $\Gamma \vdash \psi$ . En resumen: si $\Gamma \vDash \psi$ , entonces $\Gamma \vdash \psi$ .

Esbozo de demostración.

La prueba completa está en la sección 1.4.4 de (Huth y Ryan, 2004) y sigue el argumento clásico de Kalmár (Kalmár, 1935) . Consta de tres pasos.

Paso 1: reducir la consecuencia a una tautología. De $\Gamma \vDash \psi$ se sigue que $\eta \equiv \phi_1 \rightarrow (\cdots \rightarrow (\phi_n \rightarrow \psi)\cdots)$ es una tautología ( $\vDash \eta$ ), pues el único modo de falsarla sería con todas las $\phi_i$ verdaderas y $\psi$ falsa, lo que $\Gamma \vDash \psi$ prohíbe.
Paso 2 (lema de Kalmár): toda tautología es un teorema. Es el núcleo: si $\vDash \eta$ $⊨ η$ entonces $\vdash \eta$ $⊢ η$ . La derivación se construye a partir de la tabla de verdad de $\eta$ $η$ :
1. por inducción sobre la estructura de $\eta$ se demuestra un enunciado bilateral: para cada fila (valuación $v$ ), los literales de la fila derivan $\eta$ si $v(\eta)=T$ y derivan $\neg\eta$ si $v(\eta)=F$ (si la fila es $v(p)=T$ , $v(q)=F$ y $v(\eta)=T$ , se prueba $p, \neg q \vdash \eta$ ). La forma bilateral es imprescindible: en los casos de la negación y de la implicación, la hipótesis de inducción debe cubrir también a las subfórmulas que resultan falsas en la fila;
2. como $\eta$ es tautología, en toda fila ocurre el primer caso, y esto da una derivación de $\eta$ por cada una de las $2^k$ filas, donde $k$ es el número de átomos distintos de $\eta$ ;
3. las $2^k$ derivaciones se ensamblan en una sola prueba de $\vdash \eta$ descargando los átomos uno a uno mediante la ley del medio excluido y la eliminación de la disyunción.
Paso 3: reconstruir la derivación. A partir de $\vdash \phi_1 \rightarrow (\cdots \rightarrow \psi)$ y las premisas originales, $n$ aplicaciones de modus ponens producen $\Gamma \vdash \psi$ .

Nota 9.13 (La completitud como programa)

El lema de Kalmár es constructivo: no solo afirma que la derivación existe, sino que la produce a partir de la tabla de verdad de $\eta$ . Leída así, la completitud es un programa que toma una tautología y devuelve su prueba, una perspectiva que la formalización en Lean (nivel 7, próximamente) lleva al extremo realizando este argumento sobre el fragmento $\{\neg,\rightarrow\}$ , con la reducción al absurdo en lugar de la disyunción para descargar los átomos. El caso $\Gamma=\emptyset$ del teorema (toda tautología es derivable a partir del contexto vacío) es exactamente el enunciado que allí se demuestra y verifica por máquina.

Corolario 9.14 (Equivalencia de sintaxis y semántica)

La solidez y la completitud establecen conjuntamente $\Gamma \vdash \psi \quad \text{si y solo si} \quad \Gamma \vDash \psi,$ es decir, la demostrabilidad sintáctica captura exactamente la consecuencia semántica.

Ejecuta el algoritmo

El argumento anterior no es solo un esquema: es un programa. El siguiente componente lo ejecuta de verdad sobre la tautología que elijas (fragmento $\{\neg,\rightarrow\}$ , hasta dos átomos): construye la tabla, la derivación bilateral de cada fila y el árbol de descarga, y un verificador independiente comprueba que cada paso es una instancia correcta de su regla.

El algoritmo de Kalmár, ejecutable

De la tabla de verdad a la derivación: el contenido constructivo del teorema de completitud.

Etapa 1 · La tabla de verdad

$p$	$p \rightarrow p$	derivación de la fila
T	T
F	T

Etapa 2 · El lema de Kalmár en la fila 1

El contexto de literales de la fila deriva la fórmula (bilateral: derivaría su negación si la fila la falsara). Cada paso lleva su regla.

p,\, p\, \vdash p

→i

p\, \vdash p \rightarrow p

Etapa 3 · Descarga de los átomos

El análisis por casos clásico (byCases, vía RAA) funde las 2 ramas en una derivación sin hipótesis. (Se muestran los últimos niveles; las hojas son las derivaciones de la Etapa 2.)

→i

p\, \vdash p \rightarrow p

→i

\neg p\, \vdash p \rightarrow p

byCases

\vdash p \rightarrow p

✓ Verificador independiente: las 3 derivaciones construidas son instancias correctas de las reglas.

El lema de Kalmár en acción

Ejemplo 9.15 (La completitud como construcción: p → p)

Para ver el lema de Kalmár en acción, y no solo enunciado, se aplica a la tautología más simple, $\varphi \equiv p\rightarrow p$ , en el fragmento $\{\neg,\rightarrow\}$ . Tiene un solo átomo, así que su tabla de verdad consta de dos filas, y en ambas $\varphi$ es verdadera:

\begin{array}{c|c} v(p) & v(p\rightarrow p) \\ \hline T & T \\ F & T \end{array}

Paso 1: una derivación por fila. Para cada fila se deriva $\varphi$ a partir de los literales de esa fila (el literal de $p$ es $p$ si $v(p)=T$ y $\neg p$ si $v(p)=F$ ). Como $\varphi$ es verdadera en ambas filas, en los dos casos la meta es $p\rightarrow p$ :

\dfrac{\dfrac{p\in\{p\}}{p \;\vdash\; p}\;\text{hipótesis}}{p \;\vdash\; p\rightarrow p}\;\rightarrow\text{i} \qquad\qquad \dfrac{\dfrac{p\in\{\neg p,\; p\}}{\neg p,\; p \;\vdash\; p}\;\text{hipótesis}}{\neg p \;\vdash\; p\rightarrow p}\;\rightarrow\text{i}

(En la fila $v(p)=F$ el literal $\neg p$ queda disponible como hipótesis, pero no hace falta usarlo.)

Paso 2: descargar el átomo. Quedan dos derivaciones, $p\vdash p\rightarrow p$ y $\neg p\vdash p\rightarrow p$ , que difieren solo en el literal de $p$ . El análisis por casos clásico las ensambla en una sola prueba sin hipótesis, $\vdash p\rightarrow p,$ con el razonamiento «si vale $p$ , uso la primera; si vale $\neg p$ , uso la segunda; y como $p\vee\neg p$ es un teorema, $\varphi$ se sigue en cualquier caso». En el fragmento $\{\neg,\rightarrow\}$ , sin disyunción, este ensamblaje se realiza mediante la reducción al absurdo; se formaliza como la regla derivada byCases en el nivel 7 (próximamente).

Lo esencial: partiendo únicamente de la tabla de verdad, el procedimiento fabrica el árbol de derivación de $\vdash p\rightarrow p$ . Esto es la «completitud como programa» de forma literal; en el nivel 7 este mismo cómputo lo ejecuta Lean sobre $p\rightarrow p$ y devuelve el término de prueba resultante.

El medio excluido aparece dos veces en este nivel: como regla que hace clásico al cálculo (Nota 9.5) y ahora como la pieza que ensambla las $2^k$ derivaciones del lema de Kalmár. La página siguiente examina qué ocurre cuando se renuncia a él: la perspectiva constructiva.