Ejercicios

Tratemos de demostrar los siguientes teoremas construyendo programas que compilen.

Ejercicio 1: Identidad $A⟹A$ “Dado que asumimos A, concluimos A”.

identidad :: a -> a
identidad a = a

Ejercicio 2: Constante** $A⟹B⟹A$

constante :: a -> b -> a
constante a b = a

Ejercicio 3: Modus Ponens $(A⟹B)⟹A⟹B$

modusPonens :: (a -> b) -> a -> b
modusPonens f x = f x

Ejercicio 4: Silogismo Hipotético $(A⟹B)⟹(B⟹C)⟹(A⟹C)$

transitividad :: (a -> b) -> (b -> c) -> (a -> c)
transitividad f g x = g (f x)
-- También válido usando composición:
-- transitividad f g = g . f

Ejercicio 5: Conmutatividad de la Conjunción $A\wedge B⟹B\wedge A$****

conjConmuta :: (a, b) -> (b, a)
conjConmuta (x, y) = (y, x)

Ejercicio 6: El problema de la Negación y Lógica Intuicionista En Haskell, el tipo Void (que no tiene constructores) representa lo falso ($\perp$).

data Falso -- Tipo sin constructores
type Not a = a -> Falso
 
{-# LANGUAGE EmptyCase #-}
exFalso :: Falso -> a
exFalso x = case x of {}

¿Qué pasa con el Tercio Excluso ($A\vee \neg A$) o la Doble Negación?

-- dobleNeg :: Not (Not a) -> a
-- dobleNeg = ???
 
-- tercioExcluso :: Either a (Not a)
-- tercioExcluso = ???

Nos quedaremos atrapados. ¿Por qué? Porque lenguajes como Haskell (y asesores de pruebas como Rocq o LEAN) operan bajo lógica constructivista. Si afirmas que algo existe o es verdadero, tienes que construir el algoritmo para obtenerlo.

Resumen

Proposición	Tipo
Implicación $A\to B$	a -> b
Conjunción $A\wedge B$	(a, b)
Disyunción $A\vee B$	Either a b
Verdadero ($\top$)	()
Falso ($\perp$)	Void
Negación $\neg A$	a -> Void

Reglas en Deducción Natural	Operaciones en Haskell
Intro $\to$	\x -> ...
Elim $\to$	f x
Intro $\wedge$	(x, y)
Elim $\wedge$	fst p, snd p
Intro $\vee$	Left x, Right y
Elim $\vee$	case x of {Left a -> ...; Right b -> ...}