Lógica intuicionista

Diversos sistemas de lógica simbólica

La lógica intuicionista , a veces llamada de manera más general lógica constructiva , se refiere a sistemas de lógica simbólica que difieren de los sistemas utilizados para la lógica clásica al reflejar más fielmente la noción de prueba constructiva . En particular, los sistemas de lógica intuicionista no asumen la ley del tercero excluido y la eliminación de la doble negación , que son reglas de inferencia fundamentales en la lógica clásica.

La lógica intuicionista formalizada fue desarrollada originalmente por Arend Heyting para proporcionar una base formal al programa de intuicionismo de LEJ Brouwer . Desde una perspectiva de teoría de la prueba , el cálculo de Heyting es una restricción de la lógica clásica en la que se han eliminado la ley del tercio excluido y la eliminación de la doble negación. Sin embargo, la eliminación del tercio excluido y la eliminación de la doble negación aún se pueden demostrar para algunas proposiciones caso por caso, pero no se cumplen universalmente como sucede con la lógica clásica. La explicación estándar de la lógica intuicionista es la interpretación BHK . ^[1]

Se han estudiado varios sistemas de semántica para la lógica intuicionista. Una de estas semánticas refleja la semántica clásica de valor booleano pero utiliza álgebras de Heyting en lugar de álgebras booleanas . Otra semántica utiliza modelos de Kripke . Estos, sin embargo, son medios técnicos para estudiar el sistema deductivo de Heyting en lugar de formalizaciones de las intuiciones semánticas informales originales de Brouwer. Los sistemas semánticos que afirman capturar tales intuiciones, debido a que ofrecen conceptos significativos de "verdad constructiva" (en lugar de mera validez o demostrabilidad), son la interpretación dialéctica de Kurt Gödel , la realizabilidad de Stephen Cole Kleene , la lógica de problemas finitos de Yurii Medvedev, ^[2] o la lógica de computabilidad de Giorgi Japaridze . Sin embargo, tales semánticas inducen persistentemente lógicas propiamente más fuertes que la lógica de Heyting. Algunos autores han argumentado que esto podría ser una indicación de la insuficiencia del propio cálculo de Heyting, considerándolo incompleto como lógica constructiva. ^[3]

Constructivismo matemático

En la semántica de la lógica clásica, a las fórmulas proposicionales se les asignan valores de verdad del conjunto de dos elementos ("verdadero" y "falso", respectivamente), independientemente de si tenemos evidencia directa para cualquiera de los casos. Esto se conoce como la "ley del tercio excluido", porque excluye la posibilidad de cualquier valor de verdad además de "verdadero" o "falso". Por el contrario, a las fórmulas proposicionales en la lógica intuicionista no se les asigna un valor de verdad definido y solo se consideran "verdaderas" cuando tenemos evidencia directa, es decir, prueba . (También podemos decir, en lugar de que la fórmula proposicional sea "verdadera" debido a la evidencia directa, que está habitada por una prueba en el sentido de Curry-Howard ). Por lo tanto, las operaciones en la lógica intuicionista preservan la justificación , con respecto a la evidencia y la demostrabilidad, en lugar de la valoración de la verdad. ${\displaystyle \{\top ,\bot \}}$

La lógica intuicionista es una herramienta de uso común en el desarrollo de enfoques del constructivismo en matemáticas. El uso de la lógica constructivista en general ha sido un tema controvertido entre matemáticos y filósofos (véase, por ejemplo, la controversia Brouwer-Hilbert ). Una objeción común a su uso es la falta, antes citada, de dos reglas centrales de la lógica clásica, la ley del tercio excluido y la eliminación de la doble negación. David Hilbert las consideraba tan importantes para la práctica de las matemáticas que escribió:

"Quitarle el principio del tercero excluido a los matemáticos equivaldría, por ejemplo, a prohibirle el telescopio al astrónomo o el uso de los puños al boxeador. Prohibir los enunciados de existencia y el principio del tercero excluido equivale a renunciar por completo a la ciencia de las matemáticas." ^[4]

La lógica intuicionista ha encontrado un uso práctico en matemáticas a pesar de los desafíos que presenta la incapacidad de utilizar estas reglas. Una razón para esto es que sus restricciones producen pruebas que tienen la propiedad de existencia , lo que la hace también adecuada para otras formas de constructivismo matemático . Informalmente, esto significa que si hay una prueba constructiva de que un objeto existe, esa prueba constructiva puede usarse como un algoritmo para generar un ejemplo de ese objeto, un principio conocido como la correspondencia de Curry-Howard entre pruebas y algoritmos. Una razón por la que este aspecto particular de la lógica intuicionista es tan valioso es que permite a los profesionales utilizar una amplia gama de herramientas computarizadas, conocidas como asistentes de prueba . Estas herramientas ayudan a sus usuarios en la generación y verificación de pruebas a gran escala, cuyo tamaño generalmente impide la verificación humana habitual que implica la publicación y revisión de una prueba matemática. Como tal, el uso de asistentes de prueba (como Agda o Coq ) está permitiendo a los matemáticos y lógicos modernos desarrollar y probar sistemas extremadamente complejos, más allá de aquellos que son factibles de crear y verificar únicamente a mano. Un ejemplo de una prueba que era imposible de verificar satisfactoriamente sin verificación formal es la famosa prueba del teorema de los cuatro colores . Este teorema dejó perplejos a los matemáticos durante más de cien años, hasta que se desarrolló una prueba que descartaba grandes clases de posibles contraejemplos, pero aún dejaba abiertas suficientes posibilidades como para que se necesitara un programa informático para terminar la prueba. Esa prueba fue controvertida durante algún tiempo, pero, más tarde, se verificó utilizando Coq.

Sintaxis

La red de Rieger-Nishimura. Sus nodos son las fórmulas proposicionales en una variable hasta la equivalencia lógica intuicionista , ordenadas por implicación lógica intuicionista.

La sintaxis de las fórmulas de la lógica intuicionista es similar a la lógica proposicional o lógica de primer orden . Sin embargo, los conectivos intuicionistas no son definibles en términos unos de otros de la misma manera que en la lógica clásica , por lo tanto, su elección importa. En la lógica proposicional intuicionista (LPI) es habitual utilizar →, ∧, ∨, ⊥ como los conectivos básicos, tratando ¬ A como una abreviatura de ( A → ⊥) . En la lógica intuicionista de primer orden se necesitan ambos cuantificadores ∃, ∀.

Cálculo al estilo de Hilbert

La lógica intuicionista se puede definir utilizando el siguiente cálculo de estilo Hilbert . Esto es similar a una forma ^{[ ancla rota ]} de axiomatizar la lógica proposicional clásica. ^[5]

En lógica proposicional, la regla de inferencia es modus ponens

• MP: de y inferir ${\displaystyle \phi \to \psi }$ ${\displaystyle \phi }$ ${\displaystyle \psi }$

y los axiomas son

• ENTONCES-1: ${\displaystyle \psi \to (\phi \to \psi )}$
• ENTONCES-2: ${\displaystyle {\big (}\chi \to (\phi \to \psi ){\big )}\to {\big (}(\chi \to \phi )\to (\chi \to \psi ){\big )}}$
• Y-1: ${\displaystyle \phi \land \chi \to \phi }$
• Y-2: ${\displaystyle \phi \land \chi \to \chi }$
• Y-3: ${\displaystyle \phi \to {\big (}\chi \to (\phi \land \chi ){\big )}}$
• O-1: ${\displaystyle \phi \to \phi \lor \chi }$
• O-2: ${\displaystyle \chi \to \phi \lor \chi }$
• O-3: ${\displaystyle (\phi \to \psi )\to {\Big (}(\chi \to \psi )\to {\big (}(\phi \lor \chi )\to \psi ){\Big )}}$
• FALSO: ${\displaystyle \bot \to \phi }$

Para hacer de este un sistema de lógica de predicados de primer orden, las reglas de generalización

• ${\displaystyle \forall }$-GEN: de inferir , si no es libre en ${\displaystyle \psi \to \phi }$ ${\displaystyle \psi \to (\forall x\ \phi )}$ ${\displaystyle x}$ ${\displaystyle \psi }$
• ${\displaystyle \exists }$-GEN: de inferir , si no es libre en ${\displaystyle \phi \to \psi }$ ${\displaystyle (\exists x\ \phi )\to \psi }$ ${\displaystyle x}$ ${\displaystyle \psi }$

se añaden, junto con los axiomas

• PRED-1: , si el término es libre para la sustitución de la variable en (es decir, si ninguna ocurrencia de ninguna variable en queda ligada en ) ${\displaystyle (\forall x\ \phi (x))\to \phi (t)}$ ${\displaystyle t}$ ${\displaystyle x}$ ${\displaystyle \phi }$ ${\displaystyle t}$ ${\displaystyle \phi (t)}$
• PRED-2: , con la misma restricción que para PRED-1 ${\displaystyle \phi (t)\to (\exists x\ \phi (x))}$

Negación

Si se desea incluir un conectivo para la negación en lugar de considerarlo una abreviatura de , basta con añadir: ${\displaystyle \neg }$ ${\displaystyle \phi \to \bot }$

• NO-1': ${\displaystyle (\phi \to \bot )\to \neg \phi }$
• NO-2': ${\displaystyle \neg \phi \to (\phi \to \bot )}$

Hay varias alternativas disponibles si se desea omitir el conectivo (falso). Por ejemplo, se pueden reemplazar los tres axiomas FALSO, NO-1' y NO-2' con los dos axiomas ${\displaystyle \bot }$

• NO-1: ${\displaystyle (\phi \to \chi )\to {\big (}(\phi \to \neg \chi )\to \neg \phi {\big )}}$
• NO-2: ${\displaystyle \chi \to (\neg \chi \to \psi )}$

como en Cálculo proposicional § Axiomas . Las alternativas a NOT-1 son o . ${\displaystyle (\phi \to \neg \chi )\to (\chi \to \neg \phi )}$ ${\displaystyle (\phi \to \neg \phi )\to \neg \phi }$

Equivalencia

El conector de equivalencia puede tratarse como una abreviatura, con el símbolo . Alternativamente, se pueden agregar los axiomas ${\displaystyle \leftrightarrow }$ ${\displaystyle \phi \leftrightarrow \chi }$ ${\displaystyle (\phi \to \chi )\land (\chi \to \phi )}$

• FIB-1: ${\displaystyle (\phi \leftrightarrow \chi )\to (\phi \to \chi )}$
• FIB-2: ${\displaystyle (\phi \leftrightarrow \chi )\to (\chi \to \phi )}$
• FIB-3: ${\displaystyle (\phi \to \chi )\to ((\chi \to \phi )\to (\phi \leftrightarrow \chi ))}$

IFF-1 e IFF-2 pueden, si se desea, combinarse en un solo axioma utilizando la conjunción. ${\displaystyle (\phi \leftrightarrow \chi )\to ((\phi \to \chi )\land (\chi \to \phi ))}$

Cálculo secuencial

Gerhard Gentzen descubrió que una simple restricción de su sistema LK (su cálculo secuencial para lógica clásica) da como resultado un sistema sólido y completo con respecto a la lógica intuicionista. A este sistema lo llamó LJ. En LK se permite que aparezca cualquier número de fórmulas en el lado de la conclusión de un secuencial; en cambio, LJ permite como máximo una fórmula en esta posición.

Otras derivadas de LK se limitan a derivaciones intuicionistas pero aún permiten conclusiones múltiples en una secuencia. LJ' ^[6] es un ejemplo.

Teoremas

Los teoremas de la lógica pura son los enunciados demostrables a partir de los axiomas y las reglas de inferencia. Por ejemplo, el uso de THEN-1 en THEN-2 lo reduce a . En esa página se ofrece una prueba formal de esto último utilizando el sistema de Hilbert . Con para , esto a su vez implica . En palabras: "Si ser el caso implica que es absurdo, entonces si se cumple, se tiene que no es el caso". Debido a la simetría del enunciado, de hecho se obtuvo ${\displaystyle {\big (}\chi \to (\phi \to \psi ){\big )}\to {\big (}\phi \to (\chi \to \psi ){\big )}}$ ${\displaystyle \bot }$ ${\displaystyle \psi }$ ${\displaystyle (\chi \to \neg \phi )\to (\phi \to \neg \chi )}$ ${\displaystyle \chi }$ ${\displaystyle \phi }$ ${\displaystyle \phi }$ ${\displaystyle \chi }$

${\displaystyle (\chi \to \neg \phi )\leftrightarrow (\phi \to \neg \chi )}$

Al explicar los teoremas de la lógica intuicionista en términos de la lógica clásica, se puede entender como un debilitamiento de esta última: es más conservadora en lo que permite inferir a un razonador, mientras que no permite ninguna inferencia nueva que no se pueda hacer bajo la lógica clásica. Cada teorema de la lógica intuicionista es un teorema de la lógica clásica, pero no a la inversa. Muchas tautologías de la lógica clásica no son teoremas de la lógica intuicionista; en particular, como se dijo anteriormente, uno de los principales objetivos de la lógica intuicionista es no afirmar la ley del tercero excluido de modo de viciar el uso de la prueba no constructiva por contradicción , que puede usarse para proporcionar afirmaciones de existencia sin proporcionar ejemplos explícitos de los objetos que prueba que existen.

Dobles negaciones

Una doble negación no afirma la ley del tercio excluido (PEM); si bien no es necesariamente el caso de que PEM se sostenga en cualquier contexto, tampoco se puede dar ningún contraejemplo. Tal contraejemplo sería una inferencia (inferir la negación de la ley para una cierta proposición) no permitida bajo la lógica clásica y, por lo tanto, PEM no está permitido en un debilitamiento estricto como la lógica intuicionista. Formalmente, es un teorema simple que para cualesquiera dos proposiciones. Al considerar que cualquier establecido es falso, esto de hecho muestra que la doble negación de la ley se mantiene como una tautología ya en la lógica minimal . Y ahora, como se establece que es inconsistente, el tercio excluido ni siquiera será demostrable para todas las disyunciones del tercio excluido. Y esto también significa que el cálculo proposicional siempre es compatible con la lógica clásica. ${\displaystyle {\big (}(\psi \lor (\psi \to \varphi ))\to \varphi {\big )}\leftrightarrow \varphi }$ ${\displaystyle \varphi }$ ${\displaystyle \neg \neg (\psi \lor \neg \psi )}$ ${\displaystyle \neg (\psi \lor \neg \psi )}$

Si se supone que la ley del tercero excluido implica una proposición, entonces, al aplicar la contraposición dos veces y usar el tercero excluido doblemente negado, se pueden demostrar variantes doblemente negadas de varias tautologías estrictamente clásicas. La situación es más complicada para las fórmulas de lógica de predicados, cuando se niegan algunas expresiones cuantificadas.

Doble negación e implicación

De manera similar a lo anterior, de modus ponens en la forma se sigue . La relación entre ellos siempre puede usarse para obtener nuevas fórmulas: Una premisa debilitada produce una implicación fuerte, y viceversa. Por ejemplo, note que si se cumple, entonces también se cumple , pero el esquema en la otra dirección implicaría el principio de eliminación de la doble negación. Las proposiciones para las que es posible la eliminación de la doble negación también se denominan estables . La lógica intuicionista prueba la estabilidad solo para tipos restringidos de proposiciones. Una fórmula para la que se cumple el término medio excluido se puede probar estable usando el silogismo disyuntivo , que se analiza más detalladamente a continuación. Sin embargo, lo inverso no se cumple en general, a menos que el enunciado del término medio excluido en cuestión sea estable en sí mismo. ${\displaystyle \psi \to ((\psi \to \varphi )\to \varphi )}$ ${\displaystyle \psi \to \neg \neg \psi }$ ${\displaystyle (\neg \neg \psi )\to \phi }$ ${\displaystyle \psi \to \phi }$

Se puede demostrar que una implicación es equivalente a , cualesquiera sean las proposiciones. Como caso especial, se deduce que las proposiciones de forma negada ( aquí) son estables, es decir, siempre son válidas. ${\displaystyle \psi \to \neg \phi }$ ${\displaystyle \neg \neg \psi \to \neg \phi }$ ${\displaystyle \psi =\neg \phi }$ ${\displaystyle \neg \neg \neg \phi \to \neg \phi }$

En general, es más fuerte que , que es más fuerte que , lo que implica las tres afirmaciones equivalentes , y . Utilizando el silogismo disyuntivo, las cuatro anteriores son de hecho equivalentes. Esto también da una derivación intuicionistamente válida de , ya que es equivalente a una identidad . ${\displaystyle \neg \neg \psi \to \phi }$ ${\displaystyle \psi \to \phi }$ ${\displaystyle \neg \neg (\psi \to \phi )}$ ${\displaystyle \psi \to (\neg \neg \phi )}$ ${\displaystyle (\neg \neg \psi )\to (\neg \neg \phi )}$ ${\displaystyle \neg \phi \to \neg \psi }$ ${\displaystyle \neg \neg (\neg \neg \phi \to \phi )}$

Cuando se expresa una afirmación, entonces su doble negación simplemente expresa la afirmación de que una refutación de sería inconsistente. Habiendo demostrado tal mera doble negación también ayuda a negar otras afirmaciones a través de la introducción de la negación , como entonces . Una afirmación existencial doblemente negada no denota la existencia de una entidad con una propiedad, sino más bien el absurdo de la supuesta no existencia de cualquier entidad de ese tipo. Además, todos los principios en la siguiente sección que involucran cuantificadores explican el uso de implicaciones con la existencia hipotética como premisa. ${\displaystyle \psi }$ ${\displaystyle \neg \neg \psi }$ ${\displaystyle \psi }$ ${\displaystyle (\phi \to \neg \psi )\to \neg \phi }$

Traducción de fórmulas

El debilitamiento de los enunciados mediante la adición de dos negaciones antes de los cuantificadores existenciales (y átomos) es también el paso central en la traducción de doble negación . Constituye una incorporación de la lógica clásica de primer orden a la lógica intuicionista: una fórmula de primer orden es demostrable en la lógica clásica si y solo si su traducción de Gödel-Gentzen es demostrable intuicionistamente. Por ejemplo, cualquier teorema de lógica proposicional clásica de la forma tiene una prueba que consiste en una prueba intuicionista de seguida de una aplicación de eliminación de doble negación. La lógica intuicionista puede verse así como un medio de extender la lógica clásica con semántica constructiva. ${\displaystyle \psi \to \phi }$ ${\displaystyle \psi \to \neg \neg \phi }$

No interdefinibilidad de los operadores

La lógica mínima demuestra fácilmente los siguientes teoremas, relacionando la conjunción o disyunción con la implicación usando la negación :

${\displaystyle (\phi \lor \psi )\to \neg (\neg \phi \land \neg \psi )}$

${\displaystyle (\phi \lor \psi )\to (\neg \phi \to \neg \neg \psi )}$, una variante debilitada del silogismo disyuntivo

resp.

${\displaystyle (\phi \land \psi )\to \neg (\neg \phi \lor \neg \psi )}$

${\displaystyle (\phi \land \psi )\to \neg (\phi \to \neg \psi )}$y de manera similar ${\displaystyle (\phi \to \psi )\to \neg (\phi \land \neg \psi )}$

De hecho, todavía se mantienen variantes más fuertes de estas: por ejemplo, los antecedentes pueden ser doblemente negados, como se señaló, o todos pueden ser reemplazados por en los lados de los antecedentes, como se discutirá. Sin embargo, ninguna de estas cinco implicaciones puede revertirse sin implicar inmediatamente la exclusión del medio (considere para ) o la eliminación de la doble negación (considere verdadero ). Por lo tanto, los lados izquierdos no constituyen una posible definición de los lados derechos. ${\displaystyle \psi }$ ${\displaystyle \neg \neg \psi }$ ${\displaystyle \neg \psi }$ ${\displaystyle \phi }$ ${\displaystyle \phi }$

En cambio, en la lógica proposicional clásica es posible tomar uno de esos tres conectivos más la negación como primitivo y definir los otros dos en términos de él, de esta manera. Así se hace, por ejemplo, en los tres axiomas de la lógica proposicional de Łukasiewicz . Incluso es posible definirlos todos en términos de un único operador suficiente como la flecha de Peirce (NOR) o el trazo de Sheffer (NAND). De manera similar, en la lógica clásica de primer orden, uno de los cuantificadores puede definirse en términos del otro y la negación. Estas son fundamentalmente consecuencias de la ley de bivalencia , que hace que todos esos conectivos sean meras funciones booleanas . No se requiere que la ley de bivalencia se cumpla en la lógica intuicionista. Como resultado, no se puede prescindir de ninguno de los conectivos básicos, y todos los axiomas anteriores son necesarios. Por lo tanto, la mayoría de las identidades clásicas entre conectivos y cuantificadores son solo teoremas de la lógica intuicionista en una dirección. Algunos de los teoremas van en ambas direcciones, es decir, son equivalencias, como se analiza más adelante.

Cuantificación existencial vs. cuantificación universal

En primer lugar, cuando no es libre en la proposición , entonces ${\displaystyle x}$ ${\displaystyle \varphi }$

${\displaystyle {\big (}\exists x\,(\phi (x)\to \varphi ){\big )}\,\,\to \,\,{\Big (}{\big (}\forall x\ \phi (x){\big )}\to \varphi {\Big )}}$

Cuando el dominio del discurso está vacío, entonces, por el principio de explosión , una afirmación existencial implica cualquier cosa. Cuando el dominio contiene al menos un término, entonces, suponiendo que hay un tercero excluido para , la inversa de la implicación anterior se vuelve demostrable también, lo que significa que los dos lados se vuelven equivalentes. Esta dirección inversa es equivalente a la paradoja del bebedor (PD). Además, una variante existencial y dual de ella está dada por el principio de independencia de las premisas (PI). Clásicamente, la afirmación anterior es además equivalente a una forma más disyuntiva que se analiza más adelante. Sin embargo, de manera constructiva, las afirmaciones de existencia son generalmente más difíciles de conseguir. ${\displaystyle \forall x\,\phi (x)}$

Si el dominio del discurso no está vacío y además es independiente de , tales principios son equivalentes a fórmulas en el cálculo proposicional. Aquí, la fórmula simplemente expresa la identidad . Esta es la forma currificada del modus ponens , que en el caso especial de como proposición falsa da como resultado la ley del principio de no contradicción . ${\displaystyle \phi }$ ${\displaystyle x}$ ${\displaystyle (\phi \to \varphi )\to (\phi \to \varphi )}$ ${\displaystyle ((\phi \to \varphi )\land \phi )\to \varphi }$ ${\displaystyle \varphi }$ ${\displaystyle \neg (\phi \land \neg \phi )}$

Considerar una proposición falsa para la implicación original da como resultado lo importante ${\displaystyle \varphi }$

• ${\displaystyle (\exists x\ \neg \phi (x))\to \neg (\forall x\ \phi (x))}$

En palabras: "Si existe una entidad que no tiene la propiedad , entonces se refuta lo siguiente : Cada entidad tiene la propiedad ". ${\displaystyle x}$ ${\displaystyle \phi }$ ${\displaystyle \phi }$

La fórmula cuantificadora con negaciones también se sigue inmediatamente del principio de no contradicción derivado anteriormente, cada instancia del cual ya se sigue a partir del más particular . Para derivar una contradicción dada , basta con establecer su negación (en oposición a la más fuerte ) y esto hace que probar las dobles negaciones también sea valioso. Por la misma razón, la fórmula cuantificadora original de hecho todavía se cumple con negaciones debilitadas a . Y entonces, de hecho, se cumple un teorema más fuerte: ${\displaystyle \neg (\neg \neg \phi \land \neg \phi )}$ ${\displaystyle \neg \phi }$ ${\displaystyle \neg \neg \phi }$ ${\displaystyle \phi }$ ${\displaystyle \forall x\ \phi (x)}$ ${\displaystyle \forall x{\big (}(\phi (x)\to \varphi )\to \varphi {\big )}}$

${\displaystyle (\exists x\ \neg \phi (x))\to \neg (\forall x\,\neg \neg \phi (x))}$

En palabras: "Si existe una entidad que no tiene la propiedad , entonces se refuta lo siguiente : para cada entidad, no es posible probar que no tiene la propiedad ". ${\displaystyle x}$ ${\displaystyle \phi }$ ${\displaystyle \phi }$

En segundo lugar,

${\displaystyle {\big (}\forall x\,(\phi (x)\to \varphi ){\big )}\,\,\leftrightarrow \,\,{\big (}(\exists x\ \phi (x))\to \varphi {\big )}}$

donde se aplican consideraciones similares. Aquí la parte existencial es siempre una hipótesis y esto es una equivalencia. Considerando nuevamente el caso especial,

• ${\displaystyle (\forall x\ \neg \phi (x))\leftrightarrow \neg (\exists x\ \phi (x))}$

La conversión probada se puede utilizar para obtener dos implicaciones adicionales: ${\displaystyle (\chi \to \neg \phi )\leftrightarrow (\phi \to \neg \chi )}$

${\displaystyle (\forall x\ \phi (x))\to \neg (\exists x\ \neg \phi (x))}$

${\displaystyle (\exists x\ \phi (x))\to \neg (\forall x\ \neg \phi (x))}$

Por supuesto, también se pueden derivar variantes de dichas fórmulas que tengan las negaciones dobles en el antecedente. Un caso especial de la primera fórmula aquí es y esto es de hecho más fuerte que la dirección - del punto de equivalencia mencionado anteriormente. Para simplificar la discusión aquí y más adelante, las fórmulas generalmente se presentan en formas debilitadas sin todas las posibles inserciones de negaciones dobles en los antecedentes. ${\displaystyle (\forall x\,\neg \phi (x))\to \neg (\exists x\,\neg \neg \phi (x))}$ ${\displaystyle \to }$

Existen variantes más generales. Incorporando el predicado y la currificación, la siguiente generalización también implica la relación entre implicación y conjunción en el cálculo de predicados, que se analiza a continuación. ${\displaystyle \psi }$

${\displaystyle {\big (}\forall x\ \phi (x)\to (\psi (x)\to \varphi ){\big )}\,\,\leftrightarrow \,\,{\Big (}{\big (}\exists x\ \phi (x)\land \psi (x){\big )}\to \varphi {\Big )}}$

Si el predicado es decididamente falso para todos , entonces esta equivalencia es trivial. Si es decididamente verdadero para todos , el esquema simplemente se reduce a la equivalencia establecida previamente. En el lenguaje de las clases , y , el caso especial de esta equivalencia con falso equivale a dos caracterizaciones de disyunción : ${\displaystyle \psi }$ ${\displaystyle x}$ ${\displaystyle \psi }$ ${\displaystyle x}$ ${\displaystyle A=\{x\mid \phi (x)\}}$ ${\displaystyle B=\{x\mid \psi (x)\}}$ ${\displaystyle \varphi }$ ${\displaystyle A\cap B=\emptyset }$

${\displaystyle \forall (x\in A).x\notin B\,\,\leftrightarrow \,\,\neg \exists (x\in A).x\in B}$

Disyunción vs. conjunción

Existen variaciones finitas de las fórmulas cuantificadoras, con sólo dos proposiciones:

• ${\displaystyle (\neg \phi \lor \neg \psi )\to \neg (\phi \land \psi )}$
• ${\displaystyle (\neg \phi \land \neg \psi )\leftrightarrow \neg (\phi \lor \psi )}$

El primer principio no se puede revertir: considerar para implicaría el débil tercero excluido, es decir, la afirmación . Pero la lógica intuicionista por sí sola ni siquiera prueba . Así que, en particular, no hay un principio de distributividad para las negaciones que derivan la afirmación de . Para un ejemplo informal de la lectura constructiva, considere lo siguiente: A partir de evidencia concluyente de que no es el caso de que tanto Alice como Bob se presentaron a su cita, uno no puede derivar evidencia concluyente, vinculada a cualquiera de las dos personas, de que esta persona no se presentó. Las proposiciones negadas son comparativamente débiles, en el sentido de que la ley de De Morgan , clásicamente válida , que concede una disyunción a partir de una única hipótesis negativa, no se cumple automáticamente de manera constructiva. El cálculo proposicional intuicionista y algunas de sus extensiones exhiben la propiedad de disyunción en cambio, lo que implica que uno de los disyuntos de cualquier disyunción individualmente también tendría que ser derivable. ${\displaystyle \neg \psi }$ ${\displaystyle \phi }$ ${\displaystyle \neg \psi \lor \neg \neg \psi }$ ${\displaystyle \neg \psi \lor \neg \neg \psi \lor (\neg \neg \psi \to \psi )}$ ${\displaystyle \neg \phi \lor \neg \psi }$ ${\displaystyle \neg (\phi \land \psi )}$

Las variantes inversas de estas dos, y las variantes equivalentes con antecedentes doblemente negados, ya se han mencionado anteriormente. Las implicaciones hacia la negación de una conjunción a menudo se pueden demostrar directamente a partir del principio de no contradicción. De esta manera también se puede obtener la forma mixta de las implicaciones, por ejemplo . Concatenando los teoremas, también encontramos ${\displaystyle (\neg \phi \lor \psi )\to \neg (\phi \land \neg \psi )}$

• ${\displaystyle (\neg \neg \phi \lor \neg \neg \psi )\to \neg \neg (\phi \lor \psi )}$

Lo inverso no se puede demostrar, ya que demostraría un tercio excluido débil.

En lógica de predicados, el principio de dominio constante no es válido: no implica que la proposición sea más fuerte . Sin embargo, las propiedades distributivas se cumplen para cualquier número finito de proposiciones. Para una variante de la ley de De Morgan relativa a dos predicados decidibles existencialmente cerrados , véase LLPO . ${\displaystyle \forall x{\big (}\varphi \lor \psi (x){\big )}}$ ${\displaystyle \varphi \lor \forall x\,\psi (x)}$

Conjunción vs. implicación

De la equivalencia general se sigue también import-export , expresando incompatibilidad de dos predicados utilizando dos conectivos diferentes:

• ${\displaystyle (\phi \to \neg \psi )\leftrightarrow \neg (\phi \land \psi )}$

Debido a la simetría de la conjunción conectiva, esto implica nuevamente la ya establecida . La fórmula de equivalencia para la conjunción negada puede entenderse como un caso especial de currificación y descurrificación. Nuevamente se aplican muchas más consideraciones con respecto a las dobles negaciones. Y ambos teoremas no reversibles que relacionan la conjunción y la implicación mencionados en la introducción se derivan de esta equivalencia. Uno es un recíproco y se cumple simplemente porque es más fuerte que . ${\displaystyle (\phi \to \neg \psi )\leftrightarrow (\psi \to \neg \phi )}$ ${\displaystyle (\phi \to \psi )\to \neg (\phi \land \neg \psi )}$ ${\displaystyle \phi \to \psi }$ ${\displaystyle \phi \to \neg \neg \psi }$

Ahora bien, al utilizar el principio en la siguiente sección, también se cumple la siguiente variante de este último, con más negaciones a la izquierda:

• ${\displaystyle \neg (\phi \to \psi )\leftrightarrow (\neg \neg \phi \land \neg \psi )}$

Una consecuencia es que

• ${\displaystyle \neg \neg (\phi \land \psi )\leftrightarrow (\neg \neg \phi \land \neg \neg \psi )}$

Disyunción vs. implicación

La lógica mínima ya demuestra que el término medio excluido es equivalente a la consequentia mirabilis , un ejemplo de la ley de Peirce . Ahora bien, es similar al modus ponens, claramente ya en la lógica mínima, que es un teorema que ni siquiera implica negaciones. En la lógica clásica, esta implicación es de hecho una equivalencia. Al tomar como de la forma , se ve que el término medio excluido junto con la explosión implican la ley de Peirce. ${\displaystyle (\phi \lor \psi )\to ((\phi \to \psi )\to \psi )}$ ${\displaystyle \phi }$ ${\displaystyle \psi \to \varphi }$

En la lógica intuicionista, se obtienen variantes del teorema enunciado que implica , como sigue. En primer lugar, observe que se pueden usar dos fórmulas diferentes para mencionadas anteriormente para implicar . Las últimas son formas del silogismo disyuntivo para proposiciones negadas, . Una forma reforzada aún se mantiene en la lógica intuicionista: ${\displaystyle \bot }$ ${\displaystyle \neg (\phi \land \psi )}$ ${\displaystyle (\neg \phi \vee \neg \psi )\to (\phi \to \neg \psi )}$ ${\displaystyle \neg \psi }$

• ${\displaystyle (\neg \phi \lor \psi )\to (\phi \to \psi )}$

Como en secciones anteriores, las posiciones de y pueden intercambiarse, lo que da como resultado un principio más fuerte que el mencionado en la introducción. Así, por ejemplo, intuicionistamente "O bien o bien " es una fórmula proposicional más fuerte que "Si no , entonces ", mientras que estas son clásicamente intercambiables. La implicación no puede generalmente invertirse, ya que eso implica inmediatamente un tercero excluido. ${\displaystyle \neg \phi }$ ${\displaystyle \phi }$ ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle P}$ ${\displaystyle Q}$

La no contradicción y la explosión juntas también prueban la variante más fuerte . Y esto muestra cómo el término medio excluido para implica la eliminación de la doble negación para él. Para un fijo , esta implicación no puede generalmente revertirse. (Sin embargo, como siempre es constructivamente válido, se deduce que suponer la eliminación de la doble negación para todas esas disyunciones implica también lógica clásica.) ${\displaystyle (\neg \phi \lor \psi )\to (\neg \neg \phi \to \psi )}$ ${\displaystyle \psi }$ ${\displaystyle \psi }$ ${\displaystyle \neg \neg (\psi \lor \neg \psi )}$

Por supuesto, las fórmulas aquí establecidas pueden combinarse para obtener aún más variantes. Por ejemplo, el silogismo disyuntivo tal como se presenta se generaliza a

${\displaystyle {\Big (}{\big (}\exists x\ \neg \phi (x){\big )}\lor \varphi {\Big )}\,\,\to \,\,{\Big (}{\big (}\forall x\ \phi (x){\big )}\to \varphi {\Big )}}$

Si es que existe algún término, el antecedente aquí incluso implica , lo que a su vez también implica la conclusión aquí (esta es nuevamente la primerísima fórmula mencionada en esta sección). ${\displaystyle \exists x{\big (}\phi (x)\to \varphi {\big )}}$

La mayor parte de la discusión en estas secciones se aplica también a la lógica mínima. Pero en cuanto al silogismo disyuntivo con general , la lógica mínima puede, como máximo, demostrar que donde denota . La conclusión aquí solo se puede simplificar utilizando la explosión. ${\displaystyle \psi }$ ${\displaystyle (\neg \phi \lor \psi )\to (\neg \neg \phi \to \psi ')}$ ${\displaystyle \psi '}$ ${\displaystyle \neg \neg \psi \land (\psi \lor \neg \psi )}$ ${\displaystyle \psi }$

Equivalencias

Las listas anteriores también contienen equivalencias. La equivalencia que implica una conjunción y una disyunción se deriva de que en realidad es más fuerte que . Ambos lados de la equivalencia pueden entenderse como conjunciones de implicaciones independientes. Arriba, el absurdo se usa para . En las interpretaciones funcionales, corresponde a las construcciones de cláusulas if . Así, por ejemplo, "No ( o )" es equivalente a "No , y también no ". ${\displaystyle (P\lor Q)\to R}$ ${\displaystyle P\to R}$ ${\displaystyle \bot }$ ${\displaystyle R}$ ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle P}$ ${\displaystyle Q}$

Una equivalencia en sí misma se define generalmente como, y luego es equivalente a, una conjunción ( ) de implicaciones ( ), de la siguiente manera: ${\displaystyle \land }$ ${\displaystyle \to }$

• ${\displaystyle (\phi \leftrightarrow \psi )\leftrightarrow {\big (}(\phi \to \psi )\land (\psi \to \phi ){\big )}}$

Con él, dichos conectivos se vuelven a su vez definibles a partir de él:

• ${\displaystyle (\phi \to \psi )\leftrightarrow ((\phi \lor \psi )\leftrightarrow \psi )}$
• ${\displaystyle (\phi \to \psi )\leftrightarrow ((\phi \land \psi )\leftrightarrow \phi )}$
• ${\displaystyle (\phi \land \psi )\leftrightarrow ((\phi \to \psi )\leftrightarrow \phi )}$
• ${\displaystyle (\phi \land \psi )\leftrightarrow (((\phi \lor \psi )\leftrightarrow \psi )\leftrightarrow \phi )}$

A su vez, y son bases completas de conectivos intuicionistas, por ejemplo. ${\displaystyle \{\lor ,\leftrightarrow ,\bot \}}$ ${\displaystyle \{\land ,\leftrightarrow ,\neg \}}$

Conectivas funcionalmente completas

Como lo demostró Alexander V. Kuznetsov , cualquiera de los siguientes conectivos –el primero ternario, el segundo quinario– es por sí mismo funcionalmente completo : cualquiera de ellos puede cumplir el papel de único operador suficiente para la lógica proposicional intuicionista, formando así un análogo del trazo de Sheffer de la lógica proposicional clásica: ^[7]

• ${\displaystyle {\big (}(P\lor Q)\land \neg R{\big )}\lor {\big (}\neg P\land (Q\leftrightarrow R){\big )}}$
• ${\displaystyle P\to {\big (}Q\land \neg R\land (S\lor T){\big )}}$

Semántica

La semántica es bastante más complicada que en el caso clásico. Una teoría de modelos puede darse mediante álgebras de Heyting o, equivalentemente, mediante la semántica de Kripke . En 2014, Bob Constable demostró que una teoría de modelos similar a la de Tarski estaba completa , pero con una noción de completitud diferente a la clásica. ^[8]

A las afirmaciones no demostradas en la lógica intuicionista no se les asigna un valor de verdad intermedio (como a veces se afirma erróneamente). Se puede demostrar que dichas afirmaciones no tienen un tercer valor de verdad, un resultado que se remonta a Glivenko en 1928. ^[1] En cambio, siguen teniendo un valor de verdad desconocido hasta que se las prueba o se las refuta. Las afirmaciones se refutan deduciendo una contradicción de ellas.

Una consecuencia de este punto de vista es que la lógica intuicionista no tiene interpretación como lógica bivalente, ni siquiera como lógica finita, en el sentido habitual. Aunque la lógica intuicionista conserva las proposiciones triviales de la lógica clásica, cada prueba de una fórmula proposicional se considera un valor proposicional válido, por lo que, según la noción de proposiciones como conjuntos de Heyting , las fórmulas proposicionales son conjuntos (potencialmente no finitos) de sus pruebas. ${\displaystyle \{\top ,\bot \}}$

Semántica del álgebra de Heyting

En lógica clásica, a menudo discutimos los valores de verdad que puede tomar una fórmula. Los valores se eligen generalmente como los miembros de un álgebra de Boole . Las operaciones de encuentro y unión en el álgebra de Boole se identifican con los conectores lógicos ∧ y ∨, de modo que el valor de una fórmula de la forma A ∧ B es el encuentro del valor de A y el valor de B en el álgebra de Boole. Entonces tenemos el teorema útil de que una fórmula es una proposición válida de lógica clásica si y solo si su valor es 1 para cada valoración , es decir, para cualquier asignación de valores a sus variables.

Un teorema correspondiente es válido para la lógica intuicionista, pero en lugar de asignar a cada fórmula un valor de un álgebra de Boole, se utilizan valores de un álgebra de Heyting , de la que las álgebras de Boole son un caso especial. Una fórmula es válida en la lógica intuicionista si y solo si recibe el valor del elemento superior para cualquier valoración en cualquier álgebra de Heyting.

Se puede demostrar que para reconocer fórmulas válidas, es suficiente considerar una única álgebra de Heyting cuyos elementos son los subconjuntos abiertos de la recta real R . ^[9] En esta álgebra tenemos:

${\displaystyle {\begin{aligned}{\text{Value}}[\bot ]&=\emptyset \\{\text{Value}}[\top ]&=\mathbf {R} \\{\text{Value}}[A\land B]&={\text{Value}}[A]\cap {\text{Value}}[B]\\{\text{Value}}[A\lor B]&={\text{Value}}[A]\cup {\text{Value}}[B]\\{\text{Value}}[A\to B]&={\text{int}}\left({\text{Value}}[A]^{\complement }\cup {\text{Value}}[B]\right)\end{aligned}}}$

donde int( X ) es el interior de X y X ^∁ su complemento .

La última identidad respecto a A → B nos permite calcular el valor de ¬ A :

${\displaystyle {\begin{aligned}{\text{Value}}[\neg A]&={\text{Value}}[A\to \bot ]\\&={\text{int}}\left({\text{Value}}[A]^{\complement }\cup {\text{Value}}[\bot ]\right)\\&={\text{int}}\left({\text{Value}}[A]^{\complement }\cup \emptyset \right)\\&={\text{int}}\left({\text{Value}}[A]^{\complement }\right)\end{aligned}}}$

Con estas asignaciones, las fórmulas intuicionistamente válidas son precisamente aquellas a las que se les asigna el valor de la línea entera. ^[9] Por ejemplo, la fórmula ¬( A ∧ ¬ A ) es válida, porque no importa qué conjunto X se elija como valor de la fórmula A , se puede demostrar que el valor de ¬( A ∧ ¬ A ) es la línea entera:

${\displaystyle {\begin{aligned}{\text{Value}}[\neg (A\land \neg A)]&={\text{int}}\left({\text{Value}}[A\land \neg A]^{\complement }\right)&&{\text{Value}}[\neg B]={\text{int}}\left({\text{Value}}[B]^{\complement }\right)\\&={\text{int}}\left(\left({\text{Value}}[A]\cap {\text{Value}}[\neg A]\right)^{\complement }\right)\\&={\text{int}}\left(\left({\text{Value}}[A]\cap {\text{int}}\left({\text{Value}}[A]^{\complement }\right)\right)^{\complement }\right)\\&={\text{int}}\left(\left(X\cap {\text{int}}\left(X^{\complement }\right)\right)^{\complement }\right)\\&={\text{int}}\left(\emptyset ^{\complement }\right)&&{\text{int}}\left(X^{\complement }\right)\subseteq X^{\complement }\\&={\text{int}}(\mathbf {R} )\\&=\mathbf {R} \end{aligned}}}$

Por lo tanto, la valoración de esta fórmula es verdadera y, de hecho, la fórmula es válida. Pero se puede demostrar que la ley del tercio excluido, A ∨ ¬ A , no es válida utilizando un valor específico del conjunto de números reales positivos para A :

${\displaystyle {\begin{aligned}{\text{Value}}[A\lor \neg A]&={\text{Value}}[A]\cup {\text{Value}}[\neg A]\\&={\text{Value}}[A]\cup {\text{int}}\left({\text{Value}}[A]^{\complement }\right)&&{\text{Value}}[\neg B]={\text{int}}\left({\text{Value}}[B]^{\complement }\right)\\&=\{x>0\}\cup {\text{int}}\left(\{x>0\}^{\complement }\right)\\&=\{x>0\}\cup {\text{int}}\left(\{x\leqslant 0\}\right)\\&=\{x>0\}\cup \{x<0\}\\&=\{x\neq 0\}\\&\neq \mathbf {R} \end{aligned}}}$

La interpretación de cualquier fórmula válida desde el punto de vista intuicionista en el álgebra de Heyting infinita descrita anteriormente da como resultado que el elemento superior, que representa la verdad, sea la valoración de la fórmula, independientemente de qué valores del álgebra se asignen a las variables de la fórmula. ^[9] Por el contrario, para cada fórmula inválida, hay una asignación de valores a las variables que produce una valoración que difiere del elemento superior. ^{[10] [11]} Ningún álgebra de Heyting finita tiene la segunda de estas dos propiedades. ^[9]

Semántica de Kripke

Basándose en su trabajo sobre la semántica de la lógica modal , Saul Kripke creó otra semántica para la lógica intuicionista, conocida como semántica de Kripke o semántica relacional. ^{[12] [13] [5]}

Semántica similar a la de Tarski

Se descubrió que no era posible demostrar que la semántica de tipo Tarski para la lógica intuicionista fuera completa. Sin embargo, Robert Constable ha demostrado que una noción más débil de completitud sigue siendo válida para la lógica intuicionista bajo un modelo de tipo Tarski. En esta noción de completitud no nos interesan todas las afirmaciones que son verdaderas para cada modelo, sino las afirmaciones que son verdaderas de la misma manera en cada modelo. Es decir, una única prueba de que el modelo juzga que una fórmula es verdadera debe ser válida para cada modelo. En este caso, no sólo hay una prueba de completitud, sino una que es válida según la lógica intuicionista. ^[8]

Metalógica

Reglas admisibles

En la lógica intuicionista o en una teoría fija que utilice la lógica, puede darse la situación de que una implicación siempre se cumpla metateóricamente, pero no en el lenguaje. Por ejemplo, en el cálculo proposicional puro, si es demostrable, entonces también lo es . Otro ejemplo es que ser demostrable siempre significa también que también lo es . Se dice que el sistema está cerrado bajo estas implicaciones como reglas y que pueden adoptarse. ${\displaystyle (\neg A)\to (B\lor C)}$ ${\displaystyle (\neg A\to B)\lor (\neg A\to C)}$ ${\displaystyle (A\to B)\to (A\lor C)}$ ${\displaystyle {\big (}(A\to B)\to A{\big )}\lor {\big (}(A\to B)\to C{\big )}}$

Relación con otras lógicas

Lógica paraconsistente

La lógica intuicionista está relacionada por dualidad con una lógica paraconsistente conocida como lógica brasileña , antiintuicionista o dual-intuicionista . ^[14]

El subsistema de la lógica intuicionista con el axioma FALSO (resp. NO-2) eliminado se conoce como lógica mínima y algunas diferencias se han explicado anteriormente.

Lógica intermedia

En 1932, Kurt Gödel definió un sistema de lógicas intermedio entre la lógica clásica y la lógica intuicionista. De hecho, cualquier álgebra de Heyting finita que no sea equivalente a un álgebra de Boole define (semánticamente) una lógica intermedia . Por otra parte, la validez de las fórmulas en la lógica intuicionista pura no está ligada a ninguna álgebra de Heyting individual, sino que se relaciona con todas y cada una de las álgebras de Heyting al mismo tiempo.

Por ejemplo, para un esquema que no implica negaciones, considere la lógica clásicamente válida . Al adoptar esta lógica en lugar de la lógica intuicionista, se obtiene la lógica intermedia llamada lógica de Gödel-Dummett. ${\displaystyle (A\to B)\lor (B\to A)}$

Relación con la lógica clásica

El sistema de la lógica clásica se obtiene añadiendo cualquiera de los siguientes axiomas:

• ${\displaystyle \phi \lor \neg \phi }$(Ley del tercero excluido)
• ${\displaystyle \neg \neg \phi \to \phi }$(Eliminación de doble negación)
• ${\displaystyle (\neg \phi \to \phi )\to \phi }$( Consequentia mirabilis , ver también ley de Peirce )

También existen varias reformulaciones o formulaciones como esquemas en dos variables (por ejemplo, la ley de Peirce). Una de ellas es la ley de contraposición (inversa).

• ${\displaystyle (\neg \phi \to \neg \chi )\to (\chi \to \phi )}$

Estos se detallan en el artículo sobre lógica intermedia .

En general, se puede tomar como axioma adicional cualquier tautología clásica que no sea válida en el marco de dos elementos de Kripke (en otras palabras, que no esté incluida en la lógica de Smetanich ). ${\displaystyle \circ {\longrightarrow }\circ }$

Lógica de múltiples valores

El trabajo de Kurt Gödel sobre la lógica de múltiples valores mostró en 1932 que la lógica intuicionista no es una lógica de valores finitos . ^[15] (Véase la sección titulada Semántica del álgebra de Heyting más arriba para una interpretación de la lógica intuicionista desde el punto de vista de la lógica de valores infinitos ).

Lógica modal

Cualquier fórmula de la lógica proposicional intuicionista (CPI) puede traducirse al lenguaje de la lógica modal normal S4 de la siguiente manera:

${\displaystyle {\begin{aligned}\bot ^{*}&=\bot \\A^{*}&=\Box A&&{\text{if }}A{\text{ is prime (a positive literal)}}\\(A\wedge B)^{*}&=A^{*}\wedge B^{*}\\(A\vee B)^{*}&=A^{*}\vee B^{*}\\(A\to B)^{*}&=\Box \left(A^{*}\to B^{*}\right)\\(\neg A)^{*}&=\Box (\neg (A^{*}))&&\neg A:=A\to \bot \end{aligned}}}$

y se ha demostrado que la fórmula traducida es válida en la lógica modal proposicional S4 si y solo si la fórmula original es válida en IPC. ^[16] El conjunto de fórmulas anterior se denomina traducción de Gödel–McKinsey–Tarski . También existe una versión intuicionista de la lógica modal S4 llamada Lógica modal constructiva CS4. ^[17]

Cálculo lambda

Existe un isomorfismo de Curry-Howard extendido entre el IPC y el cálculo lambda de tipos simples . ^[17]

Véase también

• Interpretación de BHK
• Lógica de computabilidad
• Análisis constructivo
• Prueba constructiva
• Teoría de conjuntos constructivos
• Correspondencia entre Curry y Howard
• Semántica del juego
• Fórmula de Harrop
• Aritmética de Heyting
• Conjunto habitado
• Lógica intermedia
• Teoría de tipos intuicionista
• Semántica de Kripke
• Lógica lineal
• Lógica paraconsistente
• Realizabilidad
• Teoría de la relevancia
• Análisis infinitesimal suave

• Portal de filosofía

Notas

1. Van Atten 2022.
2. Shehtman 1990.
3. Japaridze 2009.
4. Van Heijenoort : Hilbert (1927), p.476
5. Bezhanishvili y De Jongh, p. 8.
6. Takeuti 2013.
7. Chagrov y Zakharyaschev 1997, págs. 58–59.
8. Constable y Bickford 2014.
9. Sørensen y Urzyczyn 2006, pág. 42.
10. Tarski 1938.
11. Rasiowa y Sikorski 1963, págs. 385–386.
12. Kripke 1965.
13. Moschovakis 2022.
14. Aoyama 2004.
15. Burgess 2014.
16. Lévy 2011, págs. 4-5.
17. Alechina y col. 2003.

Referencias

• Alechina, Natasha; Mendler, Michael; De Paiva, Valeria ; Ritter, Eike (enero de 2003). Semántica categórica y de Kripke para lógica modal constructiva S4 (PDF) . Actas del 15.º Taller internacional sobre lógica informática. Apuntes de clase en informática . doi :10.1007/3-540-44802-0_21.
• Aoyama, Hiroshi (2004). "LK, LJ, lógica intuicionista dual y lógica cuántica". Notre Dame Journal of Formal Logic . 45 (4): 193–213. doi : 10.1305/ndjfl/1099238445 .
• Bezhanishvili, Nick; De Jongh, Dick. "Lógica intuicionista" (PDF) . Universidad de Ámsterdam (Instituto de Lógica, Lenguaje y Computación).
• Brunner, ABM; Carnielli, Walter (marzo de 2005). "Anti-intuicionismo y paraconsistencia". Journal of Applied Logic . 3 (1): 161–184. doi : 10.1016/j.jal.2004.07.016 .
• Burgess, John (enero de 2014). "Intuiciones de tres tipos en las opiniones de Gödel sobre el continuo" (PDF) . doi :10.1017/CBO9780511756306.002 (inactivo 2024-06-04).{{cite web}}: CS1 maint: DOI inactive as of June 2024 (link)
• Chagrov, Alexander; Zakharyaschev, Michael (1997). Lógica modal . Guías de lógica de Oxford. Vol. 35. Oxford University Press . Págs. XV, 605. ISBN. 0-19-853779-4.
• Constable, R.; Bickford, M. (2014). "Completitud intuicionista de la lógica de primer orden". Anales de lógica pura y aplicada . 165 : 164–198. arXiv : 1110.1614 . doi :10.1016/j.apal.2013.07.009. S2CID  849930.
• Van Dalen, Dirk (2001). "Lógica intuicionista". En Goble, Lou (ed.). The Blackwell Guide to Philosophical Logic . Nueva York: Blackwell Publishing . págs. 224–257. doi :10.1002/9781405164801.ch11. ISBN 9780631206934.
• Heyting, Arend (1930). Die formalen Regeln der intuitionistischen Logik I, II, III . Sitzungsberichte der preussischen Akademie der Wissenschaften (en alemán). págs. 42–56, 57–71, 158–169. en tres partes
• Japaridze, Giorgi (enero de 2009). "¿En el principio existía la semántica de los juegos?". En Majer, O.; Pietarinen, A.-V.; Tulenheimo, T. (eds.). Juegos: unificación de la lógica, el lenguaje y la filosofía. Vol. 15. Springer . pp. 249–350. arXiv : cs/0507045 . doi :10.1007/978-1-4020-9374-6_11. ISBN . 978-1-4020-9373-9.
• Kripke, Saul A. (1965). "Análisis semántico de la lógica intuicionista I" (PDF) . En Crossley, JN; Dummett, MAE (eds.). Sistemas formales y funciones recursivas. Actas del octavo coloquio de lógica, Oxford, julio de 1963. Estudios de lógica y fundamentos de las matemáticas. Vol. 40. Ámsterdam: North-Holland Publishing Company . págs. 92-130. doi :10.1016/S0049-237X(08)71685-9. ISBN . 9780444534057.
• Lévy, Michel (29 de abril de 2011), Logique modale propositionnelle S4 et logique intuitioniste propositionnelle (PDF) (en francés)
• Rasiowa, Helena; Sikorski, romano (1963). Las Matemáticas de las Metamatemáticas . Monografía matematyczne. Varsovia: Państwowe Wydawn. Naukowe. pag. 519.
• Shehtman, Valentin (1990). "Las contrapartes modales de la lógica de Medvedev de problemas finitos no son finitamente axiomatizables". Studia Logica . 49 (3): 365–385. doi :10.1007/BF00370370.
• Sørensen, Morten H.; Urzyczyn, Paweł (2006). "Capítulo 2: Lógica intuicionista". Lecciones sobre el isomorfismo de Curry-Howard . Estudios de lógica y fundamentos de las matemáticas. Vol. 149 (1.ª ed.). Ámsterdam: Elsevier . ISBN. 978-0-444-52077-7.
• Takeuti, Gaisi (2013) [1975]. Teoría de la prueba (segunda edición). Mineola, Nueva York: Dover Publications. ISBN 978-0-486-49073-1.
• Tarski, Alfred (1938). "Der Aussagenkalkül und die Topologie". Fundamentos Mathematicae . 31 : 103-134. doi :10.1007/BF00370370.
• Troelstra, AS; Van Ulsen, P. "El descubrimiento de la semántica de EW Beth para la lógica intuicionista" (PDF) . Instituto de Lógica, Lenguaje y Computación (ILLC). Universidad de Ámsterdam.

Enlaces externos

• Van Atten, Mark (4 de mayo de 2022). "El desarrollo de la lógica intuicionista". En Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy .

• McCarty, David Charles (2009). "Intuicionismo en matemáticas". En Shapiro, Stewart (ed.). The Oxford Handbook of Philosophy of Mathematics and Logic . págs. 356–386. doi :10.1093/oxfordhb/9780195325928.003.0010. ISBN 978-0-19-532592-8.

• Moschovakis, Joan (16 de diciembre de 2022). "Lógica intuicionista". En Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy .

• "Método de Tableaux para la lógica intuicionista mediante la traducción S4". Laboratoire d'Informatique de Grenoble . Prueba la validez intuicionista de fórmulas proposicionales.