Juan Pablo Yamamoto
jpyamamoto[at]ciencias.unam.mx
Lógica Computacional II. Semestre 2025-1.
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
Codificamos las pruebas como algo con un constructor QED y los axiomas como simplemente una construcción de la prueba.
data Prueba (term :: k) = QED
axioma :: Prueba p
axioma = QED
La codificación de los términos se hace al nivel de tipos: no estamos usando el lenguaje de programación, estamos utilizando el verificador de tipos.
Valores de verdad:
data Verdadero
data Falso
Operadores "básicos":
data Conjuncion p q
data Disyuncion p q
data Implicacion p q
Operadores "derivados":
type No p = Implicacion p Falso
type Equivalencia p q = Conjuncion (Implicacion p q) (Implicacion q p)
Cuantificadores:
data Existe x p
data ParaTodo x p
Alias para simplificar la notación:
type p ∧ q = Conjuncion p q
type p ∨ q = Disyuncion p q
type p → q = Implicacion p q
type p ↔ q = Equivalencia p q
infixl 5 ∨
infixl 5 ∧
infixr 4 →
infixr 3 ↔
Notación de secuentes:
type p ⊢ q = p -> q
infixr 2 ⊢
type p ∴ q = p -> q
infixr 1 ∴
Constantes de verdad:
trivial :: Prueba Verdadero
trivial = axioma
exfalso :: Prueba Falso ∴ Prueba a
exfalso _ = axioma
Conjunción:
constructor :: (Prueba a, Prueba b) ∴ Prueba (a ∧ b)
constructor _ = axioma
first :: Prueba (a ∧ b) ∴ Prueba a
first _ = axioma
second :: Prueba (a ∧ b) ∴ Prueba b
second _ = axioma
Disyunción:
left :: Prueba a ∴ Prueba (a ∨ b)
left _ = axioma
right :: Prueba b ∴ Prueba (a ∨ b)
right _ = axioma
cases :: (Prueba (a ∨ b), Prueba a ⊢ Prueba c, Prueba b ⊢ Prueba c) ∴ Prueba c
cases (_, _, _) = axioma
Implicación:
intro :: (Prueba a ⊢ Prueba b) ∴ Prueba (a → b)
intro _ = axioma
apply :: (Prueba (a → b), Prueba a) ∴ Prueba b
apply (_, _) = axioma
Cuantificador universal:
generalize :: (forall c. Prueba (p c)) ∴ Prueba (ParaTodo x (p x))
generalize _ = axioma
specialize :: Prueba (ParaTodo x (p x)) ∴ Prueba (p c)
specialize _ = axioma
Cuantificador existencial:
use :: Prueba (p c) ∴ Prueba (Existe x (p x))
use _ = axioma
destruct :: (Prueba (Existe x (p x)), (forall c. Prueba (p c)) ⊢ Prueba q) ∴ Prueba q
destruct _ = axioma
Definimos una clase que no tiene métodos, simplemente funciona como un contexto para restringir el uso de las reglas clásicas.
class Clasicamente
Regla para caracterizar la lógica clásica:
absurd :: Clasicamente => (Prueba (No a) ⊢ Prueba Falso) ∴ Prueba a
absurd _ = axioma
ejemplo1 :: (Prueba a, Prueba ((b → a) → c)) ⊢ Prueba (d → c)
ejemplo1 (a, bac) = intro (\d -> apply (bac, intro (\b -> a)))
ejemplo2 :: Clasicamente => Prueba ((No (p → q)) → p)
ejemplo2 = intro (\nopq -> absurd (\nop -> apply (nopq, intro (\p -> exfalso (apply (nop, p))))))