Preámbulo · Lean desde cero

Prop: cuando el tipo es una afirmación

La página 1 dejó una deuda: además del == que calcula, existe un = de un solo signo, «el de los enunciados». Es hora de pagarla. Pregúntese a Lean por el tipo de la igualdad de toda la vida:

#check 2 + 2 = 4   -- 2 + 2 = 4 : Prop

La respuesta merece una pausa. No dice Bool. Dice Prop: la expresión 2 + 2 = 4 es una proposición, un enunciado matemático. Y aquí viene el giro que organiza todo lo que sigue: en Lean, una proposición es un tipo. Igual que Nat es el tipo cuyos habitantes son los números, 2 + 2 = 4 es el tipo cuyos habitantes son… sus demostraciones. Afirmar la proposición es exhibir un habitante de ese tipo.

Dos igualdades, dos oficios

Compárense las dos preguntas, lado a lado:

#check 2 + 2 == 4   -- 2 + 2 == 4 : Bool
#check 2 + 2 = 4    -- 2 + 2 = 4  : Prop

El doble signo == calcula: es una función que compara y devuelve true o false, un dato como cualquier otro. El signo simple = enuncia: no calcula nada, construye una proposición que podrá demostrarse o no. Es la diferencia entre apretar el botón de la calculadora y escribir un teorema en la pizarra. El matemático usa las dos operaciones todos los días sin distinguirlas; Lean exige distinguirlas, y la disciplina resulta iluminadora: hay igualdades que ninguna calculadora decide (entre funciones, entre conjuntos, entre infinitos) y que sin embargo se enuncian y se demuestran. == vive en el mundo del #eval; = vive en el mundo de la demostración.

Las proposiciones falsas también tienen tipo

Otra pausa necesaria:

#check 2 + 2 = 5   -- 2 + 2 = 5 : Prop

Lean acepta la expresión sin protestar, y hace bien. 2 + 2 = 5 es una proposición perfectamente bien formada; solo que es falsa. En el lenguaje de los tipos: es un tipo sin habitantes. Nadie encontrará jamás una demostración que lo habite, pero el enunciado existe, se puede negar, se puede usar como hipótesis. #check juzga la gramática de la afirmación, no su verdad; exactamente como un lógico distingue «fórmula bien formada» de «fórmula válida». La verdad no se comprueba: se demuestra, exhibiendo el habitante.

Los conectivos

Las proposiciones se combinan con los conectivos de siempre, y cada uno produce otra proposición:

-- con p y q proposiciones (p q : Prop):
#check p ∧ q    -- Prop   («p y q»)
#check p ∨ q    -- Prop   («p o q»)
#check ¬p       -- Prop   («no p»)
#check p → q    -- Prop   («p implica q»)

Los tres primeros son vocabulario nuevo. El cuarto no. Mírese dos veces: la implicación p → q se escribe con la misma flecha que Nat → Nat, y no es una coincidencia tipográfica: es literalmente el mismo símbolo del sistema, la flecha de los tipos de funciones de la página 2. La teoría de tipos de Lean no tiene una flecha para funciones y otra para implicaciones: tiene una.

Y entonces la pregunta se hace sola. Si p y q son tipos (proposiciones) y p → q es el tipo de las funciones de p en q… ¿qué sería una función de tipo p → q? Recibiría un habitante de p (una demostración de $p$) y devolvería un habitante de q (una demostración de $q$). Una máquina que transforma pruebas de $p$ en pruebas de $q$. El lector puede sospechar ya cómo se llama eso en matemática.

Lo que ya sabes

• #check 2 + 2 = 4 responde Prop: el signo = no calcula, enuncia una proposición.
• Una proposición es un tipo cuyos habitantes son sus demostraciones; == produce un dato (Bool), = produce un tipo (Prop). La deuda de la página 1 está saldada.
• 2 + 2 = 5 también es una Prop legítima: un tipo sin habitantes. Bien formada no significa verdadera.
• Los conectivos ∧, ∨, ¬, → construyen proposiciones a partir de proposiciones.
• La flecha de p → q es la misma flecha de Nat → Nat.

Queda planteada la pregunta con la que abre la página siguiente: ¿qué es un habitante de p → p? La respuesta ya está escrita en este preámbulo, en la página 2, esperando ser releída.