📐 Demostraciones de lógica proposicional con Lean 4: guía práctica 🔗

Esta publicación ofrece un recorrido técnico por los conceptos fundamentales de la lógica proposicional y su implementación formal utilizando el lenguaje de programación y asistente de demostración de teoremas Lean 4.

Tanto si eres un matemático que busca formalizar demostraciones como un programador que se adentra en la teoría de tipos, esta guía reconstruye la lógica desde los primeros principios. Comenzaremos con las constantes lógicas básicas y exploraremos cómo Lean 4 modela con elegancia las construcciones lógicas mediante el isomorfismo de Curry-Howard: el principio de que las proposiciones son tipos y las demostraciones son programas.

📑 Tabla de Contenidos 🔗

⚙️ El preámbulo: preparando el entorno 🔗

Antes de definir nuestras conectivas lógicas, necesitamos configurar un entorno base. En Lean 4, esto suele hacerse mediante dos comandos específicos para controlar el ámbito (scope) y el comportamiento computacional.

namespace Basic

noncomputable section

• namespace Basic: Este comando agrupa nuestras definiciones, evitando conflictos de nombres con la biblioteca integrada de Lean (el Prelude). Nos permite redefinir estructuras fundamentales como True, False y And desde cero con fines educativos.
• noncomputable section: Lean 4 es tanto un demostrador de teoremas como un lenguaje de programación funcional. Por defecto, intenta generar bytecode ejecutable para cada definición. Marcar una sección como noncomputable le indica al compilador que omita este paso, lo cual es habitual en la lógica formal, donde nos importan las propiedades matemáticas más que la ejecución en tiempo de ejecución.

🧩 Conectivas lógicas fundamentales 🔗

En esta sección definiremos los elementos fundacionales de la lógica, asociando la notación matemática estándar con el código en Lean 4.

✅ 1. Verdadero (True, ⊤) 🔗

La proposición más simple es aquella que es universal y lógicamente válida. En términos de programación, $\top$ se comporta como un tipo unidad (Unit type): tiene exactamente un estado y no transporta datos adicionales.

Definición:

inductive True : Prop where
  | intro : True

Como se define con un único constructor (intro), la única forma de «demostrar» True es proporcionar exactamente este constructor.

Ejemplos:

-- Demostración incondicional de True
example : True := True.intro

-- Cualquier proposición 'a' implica trivialmente True
example {a : Prop} : a → True := fun _ => True.intro

❌ 2. Falso (False, ⊥) 🔗

Mientras que True se define por la existencia trivial de una demostración, False se define por la ausencia total de ella. Es un tipo vacío (Empty type o Void type).

Definición:

inductive False : Prop

Como False no tiene constructores, nunca puedes instanciarlo de la nada. Representa una contradicción lógica.

El principio de explosión (Ex Falso Quodlibet): Si alguna vez te encuentras con una demostración de False, la lógica se derrumba y puedes demostrar cualquier cosa. Lean gestiona esto mediante el recursor False.elim.

-- De una falsedad se sigue cualquier proposición 'a' (⊥ → a)
def False.elim {a : Prop} (false_proof : False) : a := 
  false_proof.rec

🔄 3. Negación (¬) 🔗

En Lean 4, la negación no es un concepto primitivo integrado. En su lugar, se define funcionalmente mediante la implicación y False. Para demostrar que la proposición $a$ es falsa (denotado como $\neg a$), debes construir una función en la que asumir $a$ conduzca directamente a una contradicción ($\bot$).

Definición:

def Not (a : Prop) : Prop := a → False

Teoremas clave:

-- Demostración de la negación: si asumir 'a' demuestra False, entonces Not 'a' es verdadero.
theorem Not.intro {a : Prop} (h : a → False) : Not a := 
  fun ha => h ha

-- Introducción de la doble negación (a → ¬¬a)
theorem not_not_intro {a : Prop} (ha : a) : Not (Not a) := 
  fun na => na ha  -- 'na' tiene tipo (a → False), por lo que pasarle 'ha' produce False.

-- Modus Tollens: Si (a → b) y (¬b), entonces (¬a)
theorem Not.imp {a b : Prop} (nb : Not b) (ab : a → b) : Not a := 
  fun ha => 
    have hb : b := ab ha
    nb hb

➡️ 4. Implicación (→) 🔗

Dado que Lean se basa en la teoría de tipos, la implicación lógica ($a \to b$) se trata literalmente como una función. Para demostrar que $a$ implica $b$, debes escribir una función que reciba una demostración arbitraria de $a$ y devuelva una demostración de $b$.

Ejemplo de implicación encadenada: Si puedes transformar $c$ en $a$, y transformar $b$ en $d$, puedes transformar una función de $a \to b$ en una de $c \to d$.

theorem imp_imp_imp {a b c d : Prop} 
  (ca : c → a) (bd : b → d) : (a → b) → (c → d) := 
  fun ab => fun hc => 
    have ha : a := ca hc
    have hb : b := ab ha
    bd hb

🔗 5. Conjunción (∧) 🔗

La conjunción lógica, que requiere que tanto $a$ como $b$ sean verdaderas, se modela como una estructura (structure). En términos de programación, se trata de un tipo producto (Product type) (un struct o tupla) que contiene dos pruebas independientes.

Definición:

structure And (a b : Prop) : Prop where
  intro ::
  left : a
  right : b

Patrones de demostración clave:

-- Introducción: creación de un And
example {a b : Prop} (ha : a) (hb : b) : And a b := 
  And.intro ha hb

-- Simetría: a ∧ b → b ∧ a
theorem And.symm {a b : Prop} (h : And a b) : And b a := 
  And.intro h.right h.left

🔀 6. Disyunción (∨) 🔗

La disyunción lógica requiere que al menos una de las proposiciones sea verdadera. A diferencia de And, Or es un tipo suma (Sum type) inductivo (una unión etiquetada), porque existen dos formas distintas y alternativas de construir una demostración.

Definición:

inductive Or (a b : Prop) : Prop where
  | inl (h : a) : Or a b
  | inr (h : b) : Or a b

Para demostrar $a \lor b$, envuelves una demostración de $a$ en el constructor inl (inject-left) o una demostración de $b$ en el constructor inr (inject-right).

Ejemplo:

-- Simetría: a ∨ b → b ∨ a
theorem Or.symm {a b : Prop} (h : Or a b) : Or b a :=
  match h with
  | Or.inl ha => Or.inr ha
  | Or.inr hb => Or.inl hb

↔️ 7. Equivalencia lógica (↔) 🔗

La doble implicación, o «si y solo si» (Iff), representa que dos proposiciones son lógicamente equivalentes. Se define como una estructura que contiene implicaciones en ambas direcciones.

Definición:

structure Iff (a b : Prop) : Prop where
  intro ::
  mp : a → b
  mpr : b → a

Ejemplo de reflexividad:

-- Toda proposición es equivalente a sí misma (a ↔ a)
theorem Iff.refl {a : Prop} : Iff a a :=
  Iff.intro (fun ha => ha) (fun ha => ha)

🎯 Conclusión y puntos clave 🔗

Al reconstruir la lógica proposicional desde cero en Lean 4, revelamos la belleza mecánica de los sistemas formales:

1. Constructivo por defecto: Definimos qué significa poseer evidencia de una verdad, en lugar de limitarnos a afirmar que algo es verdadero.
2. Las proposiciones como tipos: A través de la correspondencia de Curry-Howard, las conectivas lógicas se corresponden directamente con estructuras de programación estándar: la implicación es una función, And es un struct, Or es un enum, True es el tipo unidad y False es el tipo vacío (void).
3. Las demostraciones como programas: Escribir una demostración matemática en Lean es idéntico a escribir una función con seguridad de tipos que satisface una firma específica.

Dominar estos bloques de construcción fundamentales proporciona los cimientos esenciales para abordar teoremas matemáticos más complejos, lógica de predicados y la verificación de sistemas de software complejos.