La lógica mínima , o cálculo mínimo , es un sistema lógico simbólico desarrollado originalmente por Ingebrigt Johansson . [1] Es una lógica intuicionista y paraconsistente , que rechaza tanto la ley del medio excluido como el principio de explosión ( ex falso quodlibet ) y, por lo tanto, no considera válida ninguna de las dos derivaciones siguientes:
dónde es cualquier proposición. La mayoría de las lógicas constructivas solo rechazan la primera, la ley del medio excluido. En la lógica clásica, las leyes ex falso
así como sus variantes con y conmutados, son equivalentes entre sí y válidos. La lógica mínima también rechaza esos principios.
Axiomatización
Como la lógica intuicionista, la lógica mínima se puede formular en el lenguaje usando una implicación , una conjunción , una disyunción y falsedad o absurdo como los conectivos básicos . Negación se trata como una abreviatura de . La lógica mínima se axiomatiza como el fragmento positivo de la lógica intuicionista.
Relación con la lógica clásica
Añadiendo la ley de la doble negación a la lógica mínima devuelve el cálculo a la lógica clásica :
- Medio excluido, , es entonces el equivalente al rechazo de y se logra mediante la introducción de disyunción en ambos lados.
- Explosión, , luego se sigue de prueba-por-contradicción utilizando .
Relación con la lógica intuicionista
La forma proposicional de modus ponens ,
es claramente válido también en la lógica mínima.
Constructivamente, representa una proposición para la que no puede haber ninguna razón para creerla. Para probar proposiciones de la forma, uno muestra que asumiendo conduce a una contradicción, . Con el principio de explosión, esto se establece como
el principio de explosión expresa que para derivar cualquier proposición también se puede hacer esto derivando lo absurdo . Este principio se rechaza con una lógica mínima. Esto significa que la fórmula no es axiomáticamente válida para y .
Como la lógica mínima representa solo el fragmento positivo de la lógica intuicionista, es un subsistema de la lógica intuicionista y es estrictamente más débil.
Prácticamente, el principio de explosión habilita el silogismo disyuntivo del contexto intuicionista:
Dada una prueba constructiva de y rechazo constructivo de , el principio de explosión permite incondicionalmente la elección positiva del caso de . Esto es porque si fue probado probando luego ya está probado, mientras que si fue probado probando , luego también sigue si el sistema permite una explosión.
Tenga en cuenta que con tomado por en la expresión modus ponens, la ley de la no contradicción
es decir , todavía se puede probar con una lógica mínima. Además, cualquier fórmula que utilice solo es demostrable en lógica mínima si y sólo si es demostrable en lógica intuicionista.
Relación con la teoría de tipos
Uso de la negación
Absurdo es necesario en la deducción natural , así como en las formulaciones teóricas de tipo bajo la correspondencia Curry-Howard . En sistemas de tipos,a menudo también se presenta como el tipo vacío. En muchos contextos,no es necesario que sea una constante separada en la lógica, pero su función puede reemplazarse con cualquier proposición rechazada. Por ejemplo, se puede definir como dónde debe ser distinto, como en una teoría que involucra números naturales.
Por ejemplo, con la caracterización anterior de , probando ser falso, es decir , es decir, probando , solo significa probar . Y de hecho, usando aritmética, aguanta, pero también implica . Entonces esto implicaría y de ahí obtenemos . QED.
Tipos simples
Los cálculos de programación funcional dependen principalmente del conectivo de implicación, ver, por ejemplo, el cálculo de construcciones para un marco de lógica de predicados .
En esta sección mencionamos el sistema obtenido al restringir la lógica mínima solo a la implicación. Puede ser definido por las siguientes guientes reglas:
Cada fórmula de esta lógica mínima restringida corresponde a un tipo en el cálculo lambda simplemente tipado , ver correspondencia Curry-Howard .
Semántica
Hay semánticas de lógica mínima que reflejan la semántica de marcos de la lógica intuicionista , ver la discusión de la semántica en lógica paraconsistente . Aquí, las funciones de valoración que asignan verdad y falsedad a las proposiciones pueden estar sujetas a menos restricciones.
Ver también
Referencias
- ^ Ingebrigt Johansson (1937). "Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus" . Compositio Mathematica (en alemán). 4 : 119-136.
- ^ M. Weber y M. Simons y C. Lafontaine (1993). El lenguaje de desarrollo genérico DEVA: presentación y estudios de casos . LNCS. 738 . Saltador. pag. 246. Aquí: p.36-40.
- ^ Gérard Huet (mayo de 1986). Estructuras formales para el cálculo y la deducción . Escuela Internacional de Verano sobre Lógica de Programación y Cálculos de Diseño Discreto. Marktoberdorf. Archivado desde el original el 14 de julio de 2014. Aquí: p.125, p.132
- AS Troelstra y H. Schwichtenberg, 2000, Teoría de la prueba básica , Cambridge University Press, ISBN 0521779111