La lógica afín es una lógica subestructural cuya teoría de la demostración rechaza la regla estructural de contracción . También puede caracterizarse como lógica lineal con debilitamiento .
El nombre de "lógica afín" se asocia a la lógica lineal , de la que se diferencia al permitir la regla de debilitamiento. Jean-Yves Girard introdujo el nombre como parte de la geometría de la semántica de interacción de la lógica lineal, que caracteriza a la lógica lineal en términos de álgebra lineal ; aquí alude a las transformaciones afines en espacios vectoriales . [1]
La lógica afín precedió a la lógica lineal. VN Grishin utilizó esta lógica en 1974, [2] después de observar que la paradoja de Russell no puede derivarse en una teoría de conjuntos sin contracción, incluso con un axioma de comprensión ilimitado . [3] Asimismo, la lógica formó la base de una subteoría decidible de la lógica de predicados , llamada 'lógica directa' (Ketonen y Wehrauch, 1984; Ketonen y Bellin, 1989).
La lógica afín se puede integrar en la lógica lineal reescribiendo la flecha afín como la flecha lineal .
Mientras que la lógica lineal completa (es decir, la lógica lineal proposicional con multiplicativos, aditivos y exponenciales) es indecidible, la lógica afín completa es decidible.
La lógica afín constituye la base de la lúdica .
