2026-04-15

Debilitamiento (Weakening): Podemos añadir una premisa.

$\frac{\Gamma ⊢\Sigma }{\Gamma ,A⊢\Sigma }$

Contracción (Contraction): Podemos cancelar una premisa redundante.

$\frac{\Gamma ,A,A⊢\Sigma }{\Gamma ,A⊢\Sigma }$

Demostración por Contradicción: Asumes que A es falsa y llegas a una contradicción, por lo tanto, concluyes A.

$\frac{\Gamma ,\neg A⊢\perp }{\Gamma ⊢A}$

Lógica	Debilitamiento	Contracción	por Contradicción
Clásica	✓	✓	✓
Intuicionista	✓	✓	X
Afín	✓	X	*
Lineal	X	X	*

*: Podemos tener lógica lineal clásica y lineal intuicionista, dependiendo de si aceptamos o no, como axioma, el principio del tercio excluso; igual para la lógica afín. Recordemos que un axioma es aquello que aceptamos como verdad sin una demostración o, bajo la correspondencia Curry-Howard, sin un algoritmo.

---

Tanto en lógica lineal como en la afín, las proposiciones ahora se tratan como recursos.

1. Lógica Afín: Un recurso se usa como máximo una vez (0 o 1). No puedes duplicarlo, pero sí puedes ignorarlo o descartarlo (esto es el debilitamiento).
2. Lógica Lineal: Un recurso se usa exactamente una vez (1 y solo 1).
   • No puedes duplicarlo (porque no hay contracción).
   • No puedes ignorarlo ni descartarlo (porque no hay debilitamiento).

¿Cuál es la regla #1 de Rust? Que un valor tiene un único dueño y se usa, como máximo, una vez.

En Rust, el sistema de ownership asegura que los recursos tengan un único dueño.

fn main() {
	let s1 = String::from("hola mundo");
	// El recurso se mueve de s1 a s2.
	// s2 es el nuevo dueño.
	let s2 = s1;
	// Si intentas hacer esto, el compilador lanzará un error:
	println!("{}", s1); // ¡Error! s1 ya fue consumido.
}

Por lo tanto, Rust, en el fondo, trabaja con un sistema de tipos afín intuicionista.

En lógica lineal introducimos una nueva implicación, la implicación lineal $A⊸B$ (que se lee como ”$A$ se consume para producir $B$”), y una nueva conjunción, $A\otimes B$ (tener ambos recursos simultáneamente).

Veamos ejemplos de tautologías clásicas que fallan en lógica lineal:

1. Falla por falta de Contracción: $A⊸(A\otimes A)$

• Clásicamente: Si asumo $A$, es cierto que tengo $A\wedge A$.

ej1 :: a -> (a, a)
ej1 x = (x, x)

Linealmente: Esto es inválido. Un solo recurso $A$ no puede producir dos recursos $A$.

{-# LANGUAGE LinearTypes #-}
 
ej1 :: a %1 -> (a, a)
ej1 x = (x, x) -- ERROR: x se usa dos veces

2. Falla por falta de Debilitamiento: $(A\otimes B)⊸A$

• Clásicamente: $A\wedge B⊸A$ (Eliminación de la conjunción).

ej2 :: (a, b) -> a
ej2 (x, _) = x

Linealmente: Es inválido. Si tienes los recursos A y B, y produces solo A, ¿qué le pasó a B? La lógica lineal exige que B sea consumido de alguna manera.

ej2 :: (a, b) %1 -> a
ej2 (x, y) = x -- ERROR: y no se ha consumido

Ahora veamos teoremas que sí son válidos en lógica lineal: $⊢A⊸A$ (La identidad lineal)

ej3 :: a %1 -> a
ej3 x = x

$⊢((A⊸B)\otimes A)⊸B$ (El modus ponens lineal)

ej4 :: (a %1 -> b, a) %1 -> b
ej4 (f, x) = f x