Lógica intuicionista

La lógica intuicionista , a veces denominada lógica constructiva , se refiere a sistemas de lógica simbólica que difieren de los sistemas utilizados en la lógica clásica al reflejar con mayor precisión la noción de prueba constructiva . En particular, los sistemas de lógica intuicionista no presuponen el principio del tercero excluido ni 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 la teoría de la demostración , el cálculo de Heyting es una restricción de la lógica clásica en la que se han eliminado la ley del tercero excluido y la eliminación de la doble negación. Sin embargo, la eliminación del tercero excluido y la eliminación de la doble negación aún pueden demostrarse para algunas proposiciones caso por caso, pero no se cumplen universalmente como en la lógica clásica. La explicación estándar de la lógica intuicionista es la interpretación BHK . ^[¹^]

Se han estudiado varios sistemas semánticos para la lógica intuicionista. Uno de ellos refleja la semántica clásica de valores booleanos , pero utiliza álgebras de Heyting en lugar de álgebras booleanas . Otro sistema semántico utiliza modelos de Kripke . Sin embargo, estos son medios técnicos para estudiar el sistema deductivo de Heyting, más que formalizaciones de las intuiciones semánticas informales originales de Brouwer. Los sistemas semánticos que pretenden capturar dichas intuiciones, al ofrecer 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 ^[²^] o la lógica de computabilidad de Giorgi Japaridze . Sin embargo, estas 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 un indicio de la insuficiencia del cálculo de Heyting en sí mismo, considerándolo incompleto como lógica constructiva. ^[³^]

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. $\{\top ,\bot \}$ («verdadero» y «falso» respectivamente), independientemente de si tenemos evidencia directa para cada caso. Esto se conoce como la «ley del tercero excluido», porque excluye la posibilidad de cualquier valor de verdad que no sea «verdadero» o «falso». En contraste, 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 que, en lugar de que la fórmula proposicional sea «verdadera» debido a la evidencia directa, está integrada en 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.

La lógica intuicionista es una herramienta comúnmente utilizada en el desarrollo de enfoques constructivistas en matemáticas. El uso de lógicas constructivistas 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 mencionada ausencia de dos reglas centrales de la lógica clásica: el principio del tercero 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 al matemático sería como prohibirle el telescopio al astrónomo o el uso de los puños al boxeador. Prohibir las afirmaciones de existencia y el principio del tercero excluido equivale a renunciar por completo a la ciencia de las matemáticas.

— Hilbert (1927), véase Van Heijenoort 2002 , p. 476

La lógica intuicionista ha encontrado aplicaciones prácticas en matemáticas a pesar de las dificultades que plantea la imposibilidad de utilizar estas reglas. Una razón es que sus restricciones generan demostraciones con propiedades de disyunción y existencia , lo que la hace adecuada también para otras formas de constructivismo matemático . En términos sencillos, esto significa que si existe una demostración constructiva de la existencia de un objeto, dicha demostración puede utilizarse como algoritmo para generar un ejemplo de ese objeto, un principio conocido como la correspondencia de Curry-Howard entre demostraciones y algoritmos. Una de las razones por las que este aspecto particular de la lógica intuicionista es tan valioso es que permite a los profesionales utilizar una amplia gama de herramientas informáticas, conocidas como asistentes de demostración . Estas herramientas ayudan a sus usuarios en la generación y verificación de demostraciones a gran escala, cuyo tamaño suele impedir la verificación manual habitual que se realiza al publicar y revisar una demostración matemática. De este modo, el uso de asistentes de demostración (como Agda o Rocq ) permite a los matemáticos y lógicos modernos desarrollar y demostrar sistemas extremadamente complejos, más allá de aquellos que son factibles de crear y verificar únicamente a mano. Un ejemplo de una demostración imposible de verificar satisfactoriamente sin una verificación formal es la famosa demostración del teorema de los cuatro colores . Este teorema desconcertó a los matemáticos durante más de cien años, hasta que se desarrolló una demostración que descartaba amplias clases de posibles contraejemplos, pero que aún dejaba abiertas suficientes posibilidades como para que fuera necesario un programa informático para completarla. Dicha demostración fue controvertida durante un tiempo, pero, posteriormente, fue verificada utilizando Rocq .

Sintaxis

El retículo de Rieger-Nishimura . Sus nodos son las fórmulas proposicionales en una variable salvo 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 de la lógica proposicional o la lógica de primer orden . Sin embargo, los conectores intuicionistas no se definen entre sí de la misma manera que en la lógica clásica , por lo que su elección es importante. En la lógica proposicional intuicionista (LPI) es habitual usar →, ∧, ∨, ⊥ como conectores básicos, tratando ¬ A como una abreviatura de ( A → ⊥) . En la lógica de primer orden intuicionista se necesitan ambos cuantificadores ∃, ∀.

Cálculo al estilo de Hilbert

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

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

MP: de $\phi \to \psi$ y $\phi$ inferir $\psi$

y los esquemas axiomáticos son

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

Para convertir esto en un sistema de lógica de predicados de primer orden , se utilizan las reglas de generalización.

$\forall$ -GEN: de $\psi \to \phi$ inferir $\psi \to (\forall x\ \phi )$ , si $x$ no es gratis en $\psi$
$\exists$ -GEN: de $\phi \to \psi$ inferir $(\exists x\ \phi )\to \psi$ , si $x$ no es gratis en $\psi$

se añaden, junto con los axiomas

PRED-1: $(\forall x\ \phi (x))\to \phi (t)$ , si el término $t$ es libre para sustituir por la variable $x$ en $\phi$ (es decir, si no ocurre ninguna variable en $t$ se vuelve vinculado en $\phi (t)$ )
PRED-2: $\phi (t)\to (\exists x\ \phi (x))$ , con la misma restricción que para PRED-1

Negación

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

NO-1': $(\phi \to \bot )\to \neg \phi$
NO-2': $\neg \phi \to (\phi \to \bot )$

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

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

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

Equivalencia

El conector $\leftrightarrow$ para la equivalencia puede tratarse como una abreviatura, con $\phi \leftrightarrow \chi$ de pie por $(\phi \to \chi )\land (\chi \to \phi )$ Alternativamente, se pueden añadir los axiomas

IFF-1: $(\phi \leftrightarrow \chi )\to (\phi \to \chi )$
IFF-2: $(\phi \leftrightarrow \chi )\to (\chi \to \phi )$
IFF-3: $(\phi \to \chi )\to ((\chi \to \phi )\to (\phi \leftrightarrow \chi ))$

IFF-1 e IFF-2 pueden, si se desea, combinarse en un único axioma. $(\phi \leftrightarrow \chi )\to ((\phi \to \chi )\land (\chi \to \phi ))$ usando conjunción.

Cálculo de secuencias

Gerhard Gentzen descubrió que una simple restricción de su sistema LK (su cálculo de secuentes para la lógica clásica) da como resultado un sistema sólido y completo con respecto a la lógica intuicionista. Lnominó a este sistema LJ. En LK, cualquier número de fórmulas puede aparecer en el sucesor (el lado de la conclusión de un secuente). LJ solo permite 0 o 1 fórmula en esta posición.

Otros derivados de LK se limitan a derivaciones intuicionistas pero aún permiten múltiples conclusiones en una secuencia. LJ' ^{[ 5 ]} es un ejemplo.

Teoremas

Los teoremas de la lógica pura son las afirmaciones demostrables a partir de los axiomas y las reglas de inferencia. Por ejemplo, usar ENTONCES-1 en ENTONCES-2 lo reduce a ${\big (}\chi \to (\phi \to \psi ){\big )}\to {\big (}\phi \to (\chi \to \psi ){\big )}$ En esa página se ofrece una demostración formal de esto último utilizando el sistema de Hilbert . $\bot$ para $\psi$ , esto a su vez implica $(\chi \to \neg \phi )\to (\phi \to \neg \chi )$ . En palabras: "Si $\chi$ Que sea así implica que $\phi$ es absurdo, entonces si $\phi$ sí se sostiene, uno tiene eso $\chi$ No es el caso." Debido a la simetría de la afirmación, de hecho se obtuvo

(\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, sin permitir nuevas inferencias que no pudieran realizarse 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 mencionó anteriormente, uno de los objetivos principales de la lógica intuicionista es no afirmar el principio del tercero excluido para así invalidar el uso de la prueba no constructiva por contradicción , que puede utilizarse para presentar afirmaciones de existencia sin proporcionar ejemplos explícitos de los objetos cuya existencia se demuestra.

Doble negación

Una doble negación no afirma la ley del tercero excluido ( PEM ); si bien no es necesariamente cierto que la PEM se sostenga en cualquier contexto, tampoco se puede dar un contraejemplo. Tal contraejemplo sería una inferencia (inferir la negación de la ley para una proposición determinada) prohibida por la lógica clásica y, por lo tanto, la PEM no está permitida en un debilitamiento estricto como la lógica intuicionista. Formalmente, es un teorema simple que ${\big (}(\psi \lor (\psi \to \varphi ))\to \varphi {\big )}\leftrightarrow \varphi$ para cualesquiera dos proposiciones. Al considerar cualquier $\varphi$ establecido como falso esto en efecto muestra que la doble negación de la ley $\neg \neg (\psi \lor \neg \psi )$ se mantiene como una tautología ya en la lógica mínima . Esto significa que cualquier $\neg (\psi \lor \neg \psi )$ Se ha demostrado que es inconsistente y el cálculo proposicional, a su vez, es siempre compatible con la lógica clásica.

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

Doble negación e implicación

Similar a lo anterior, del modus ponens en la forma $\psi \to ((\psi \to \varphi )\to \varphi )$ sigue $\psi \to \neg \neg \psi$ . La relación entre ellas siempre puede usarse para obtener nuevas fórmulas: una premisa debilitada da lugar a una implicación fuerte, y viceversa. Por ejemplo, observe que si $(\neg \neg \psi )\to \phi$ se mantiene, entonces también $\psi \to \phi$ 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 demuestra la estabilidad solo para tipos restringidos de proposiciones. Una fórmula para la que se cumple el principio del tercero excluido puede demostrarse estable mediante el silogismo disyuntivo , que se analiza con más detalle a continuación. Sin embargo, lo contrario no se cumple en general, a menos que la proposición del tercero excluido en cuestión sea estable en sí misma.

Una implicación $\psi \to \neg \phi$ se puede demostrar que es equivalente a $\neg \neg \psi \to \neg \phi$ , cualesquiera que sean las proposiciones. Como caso especial, se deduce que las proposiciones de forma negada ( $\psi =\neg \phi$ aquí) son estables, es decir $\neg \neg \neg \phi \to \neg \phi$ Siempre es válido.

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

Cuando $\psi$ expresa una afirmación, luego su doble negación $\neg \neg \psi$ simplemente expresa la afirmación de que una refutación de $\psi$ sería inconsistente. Habiendo demostrado tal mera doble negación también ayuda a negar otras afirmaciones mediante la introducción de la negación , ya que entonces $(\phi \to \neg \psi )\to \neg \phi$ Una proposición existencial doblemente negada no denota la existencia de una entidad con una propiedad, sino más bien la absurdidad de suponer la inexistencia de dicha entidad. Asimismo, todos los principios de la siguiente sección que involucran cuantificadores explican el uso de implicaciones con la existencia hipotética como premisa.

Traducción de fórmulas

Debilitar las proposiciones añadiendo 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 incrustación de la lógica clásica de primer orden en la lógica intuicionista: una fórmula de primer orden es demostrable en lógica clásica si y solo si su traducción de Gödel-Gentzen es demostrable intuicionistamente. Por ejemplo, cualquier teorema de la lógica proposicional clásica de la forma $\psi \to \phi$ tiene una prueba que consiste en una prueba intuicionista de $\psi \to \neg \neg \phi$ seguido de una aplicación de eliminación de doble negación. La lógica intuicionista puede considerarse, por lo tanto, un medio para extender la lógica clásica con semántica constructiva.

No interdefinibilidad de los operadores

La lógica mínima ya demuestra fácilmente los siguientes teoremas, que relacionan la conjunción y la disyunción con la implicación mediante la negación . En primer lugar,

$(\phi \lor \psi )\to \neg (\neg \phi \land \neg \psi )$

En palabras: " $\phi$ y $\psi$ cada uno implica que no es el caso que ambos $\phi$ y $\psi$ no logran mantenerse unidos."

Y aquí la conclusión lógicamente negativa $\neg (\neg \phi \land \neg \psi )$ es de hecho equivalente a $\neg \phi \to \neg \neg \psi$ . El teorema implícito alternativo, $(\phi \lor \psi )\to (\neg \phi \to \neg \neg \psi )$ , representa una variante debilitada del silogismo disyuntivo. En segundo lugar,

$(\phi \land \psi )\to \neg (\neg \phi \lor \neg \psi )$

En palabras: " $\phi$ y $\psi$ ambos juntos implican que ninguno $\phi$ ni $\psi$ no lograron sostenerse."

Y aquí la conclusión lógicamente negativa $\neg (\neg \phi \lor \neg \psi )$ es de hecho equivalente a $\neg (\phi \to \neg \psi )$ . Una variante del recíproco del teorema aquí implícito también se cumple, a saber:

$(\phi \to \psi )\to \neg (\phi \land \neg \psi )$

En palabras: " $\phi$ reticente $\psi$ implica que no es el caso que $\phi$ sostiene mientras $\psi$ no se sostiene."

Y de hecho, variantes más fuertes de todas estas siguen siendo válidas; por ejemplo, los antecedentes pueden ser doblemente negados, como se señaló, o todos $\psi$ puede ser reemplazado por $\neg \neg \psi$ en los lados antecedentes, como se discutirá.

Sin embargo, ninguna de estas cinco implicaciones anteriores puede revertirse sin implicar inmediatamente el principio del tercero excluido (considere $\neg \psi$ para $\phi$ ) respectivamente, eliminación de doble negación (considerar verdadero) $\phi$ Por lo tanto, los lados izquierdos no constituyen una posible definición de los lados derechos.

En contraste, en la lógica proposicional clásica es posible tomar uno de esos tres conectores 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 consecuencias fundamentales de la ley de bivalencia , que convierte a todos estos conectores en meras funciones booleanas . La ley de bivalencia no es necesaria en la lógica intuicionista. Como resultado, no se puede prescindir de ninguno de los conectores básicos, y los axiomas anteriores son todos necesarios. Por lo tanto, la mayoría de las identidades clásicas entre conectores y cuantificadores son solo teoremas de la lógica intuicionista en una dirección. Algunos de los teoremas funcionan en ambas direcciones, es decir, son equivalencias, como se analizará más adelante.

cuantificación existencial frente a cuantificación universal

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

{\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 asumiendo el tercero excluido para $\forall x\,\phi (x)$ La inversa de la implicación anterior también se vuelve demostrable, lo que significa que ambas partes se vuelven equivalentes. Esta dirección inversa es equivalente a la paradoja del bebedor (PD). Además, una variante existencial y dual de la misma viene dada por el principio de independencia de 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, desde un punto de vista constructivo, las afirmaciones de existencia suelen ser más difíciles de obtener.

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

Considerar una proposición falsa $\varphi$ para la implicación original resulta en lo importante

$(\exists x\ \neg \phi (x))\to \neg (\forall x\ \phi (x))$

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

La fórmula del cuantificador con negaciones también se deduce inmediatamente del principio de no contradicción derivado anteriormente, cada instancia del cual ya se deduce del más particular. $\neg (\neg \neg \phi \land \neg \phi )$ Para derivar una contradicción dada $\neg \phi$ , basta con establecer su negación $\neg \neg \phi$ (en contraposición al más fuerte) $\phi$ ) y esto hace que probar las dobles negaciones también sea valioso. Del mismo modo, la fórmula original del cuantificador de hecho sigue siendo válida con $\forall x\ \phi (x)$ debilitado a $\forall x{\big (}(\phi (x)\to \varphi )\to \varphi {\big )}$ . Y, de hecho, se cumple un teorema más fuerte:

(\exists x\ \neg \phi (x))\to \neg (\forall x\,\neg \neg \phi (x))

En palabras: "Si existe una entidad $x$ que no tiene la propiedad $\phi$ , entonces se refuta lo siguiente : Para cada entidad, no se puede probar que no tiene la propiedad $\phi$ ".

En segundo lugar,

{\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,

$(\forall x\ \neg \phi (x))\leftrightarrow \neg (\exists x\ \phi (x))$

La conversión comprobada $(\chi \to \neg \phi )\leftrightarrow (\phi \to \neg \chi )$ puede utilizarse para obtener dos implicaciones adicionales:

(\forall x\ \phi (x))\to \neg (\exists x\ \neg \phi (x))

(\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 dobles negaciones en el antecedente. Un caso especial de la primera fórmula aquí es $(\forall x\,\neg \phi (x))\to \neg (\exists x\,\neg \neg \phi (x))$ y esto es de hecho más fuerte que el $\to$ -dirección del punto de equivalencia mencionado anteriormente. Para simplificar la discusión aquí y a continuación, las fórmulas se presentan generalmente en formas debilitadas, sin todas las posibles inserciones de doble negación en los antecedentes.

Se mantienen variantes más generales. Incorporando el predicado $\psi$ y 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 más adelante.

{\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 $\psi$ es rotundamente falso para todos $x$ , entonces esta equivalencia es trivial. Si $\psi$ Esto es definitivamente cierto para todos. $x$ , el esquema simplemente se reduce a la equivalencia previamente establecida. En el lenguaje de clases , $A=\{x\mid \phi (x)\}$ y $B=\{x\mid \psi (x)\}$ , el caso especial de esta equivalencia con falso $\varphi$ equipara dos caracterizaciones de disyunción $A\cap B=\emptyset$ :

\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 de cuantificación, con solo dos proposiciones:

$(\neg \phi \lor \neg \psi )\to \neg (\phi \land \psi )$
$(\neg \phi \land \neg \psi )\leftrightarrow \neg (\phi \lor \psi )$

El primer principio no se puede revertir: Considerando $\neg \psi$ para $\phi$ implicaría el término medio excluido débil, es decir, la afirmación $\neg \psi \lor \neg \neg \psi$ Pero la lógica intuicionista por sí sola ni siquiera demuestra $\neg \psi \lor \neg \neg \psi \lor (\neg \neg \psi \to \psi )$ . Por lo tanto, en particular, no existe un principio de distributividad para las negaciones que derivan la afirmación. $\neg \phi \lor \neg \psi$ de $\neg (\phi \land \psi )$ Para un ejemplo informal de lectura constructiva, considérese lo siguiente: A partir de evidencia concluyente de que no es cierto que tanto Alice como Bob se presentaran a su cita, no se puede derivar evidencia concluyente, vinculada a ninguna de las dos personas, de que esta persona no se presentó. Las proposiciones negadas son comparativamente débiles, ya 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 forma constructiva. El cálculo proposicional intuicionista y algunas de sus extensiones exhiben la propiedad de disyunción , lo que implica que uno de los disyuntos de cualquier disyunción individualmente también tendría que ser derivable.

Las variantes inversas de esas dos, y las variantes equivalentes con antecedentes doblemente negados, ya se habían 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 $(\neg \phi \lor \psi )\to \neg (\phi \land \neg \psi )$ . Concatenando los teoremas, también encontramos

$(\neg \neg \phi \lor \neg \neg \psi )\to \neg \neg (\phi \lor \psi )$

Lo contrario no se puede demostrar, ya que demostraría un teorema del tercero excluido débil.

En lógica de predicados, el principio del dominio constante no es válido: $\forall x{\big (}\varphi \lor \psi (x){\big )}$ no implica que sea más fuerte $\varphi \lor \forall x\,\psi (x)$ 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 .

Conjunción vs. implicación

De la equivalencia general también se deduce la importación-exportación , que expresa la incompatibilidad de dos predicados utilizando dos conectores diferentes:

$(\phi \to \neg \psi )\leftrightarrow \neg (\phi \land \psi )$

Debido a la simetría del conector de conjunción, esto nuevamente implica lo ya establecido. $(\phi \to \neg \psi )\leftrightarrow (\psi \to \neg \phi )$ La fórmula de equivalencia para la conjunción negada puede entenderse como un caso especial de currificación y descurrificación. Se aplican muchas más consideraciones sobre las dobles negaciones. Y ambos teoremas no reversibles que relacionan la conjunción y la implicación mencionados en la introducción a la no interdefinibilidad anterior se derivan de esta equivalencia. Uno es una variante simplemente demostrada de un recíproco, mientras que $(\phi \to \psi )\to \neg (\phi \land \neg \psi )$ se sostiene simplemente porque $\phi \to \psi$ es más fuerte que $\phi \to \neg \neg \psi$ .

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

$\neg (\phi \to \psi )\leftrightarrow (\neg \neg \phi \land \neg \psi )$

Una consecuencia es que

$\neg \neg (\phi \land \psi )\leftrightarrow (\neg \neg \phi \land \neg \neg \psi )$

lo cual implica que una conjunción de proposiciones irrechazables tampoco puede ser rechazada.

Disyunción vs. implicación

La lógica mínima ya demuestra que el principio del tercero excluido es equivalente a la consequentia mirabilis , un ejemplo de la ley de Peirce . Ahora, similar al modus ponens, claramente $(\phi \lor \psi )\to ((\phi \to \psi )\to \psi )$ ya es derivable en lógica mínima, que es un teorema que ni siquiera involucra negaciones. En lógica clásica, esta implicación es de hecho una equivalencia. Tomando $\phi$ ser de la forma $\psi \to \varphi$ , se excluye el medio junto con la explosión, lo que implica la ley de Peirce.

En la lógica intuicionista, se obtienen variantes del teorema enunciado que involucran $\bot$ , como sigue. En primer lugar, observe que existen dos fórmulas diferentes para $\neg (\phi \land \psi )$ lo mencionado anteriormente puede usarse para implicar $(\neg \phi \vee \neg \psi )\to (\phi \to \neg \psi )$ También se dedujo del análisis directo de casos, al igual que las variantes en las que se mueven las negaciones, como los teoremas. $(\neg \phi \lor \psi )\to (\phi \to \neg \neg \psi )$ o $(\phi \lor \psi )\to (\neg \phi \to \neg \neg \psi )$ , este último mencionado en la introducción a la no interdefinibilidad. Estas son formas del silogismo disyuntivo que involucra proposiciones negadas. $\neg \psi$ . Las formas reforzadas aún se mantienen en la lógica intuicionista, por ejemplo

$(\neg \phi \lor \psi )\to (\phi \to \psi )$

La implicación generalmente no se puede revertir, ya que eso implicaría inmediatamente el tercero excluido. Por lo tanto, intuicionistamente, "O bien $P$ o $Q$ " es generalmente también una fórmula proposicional más fuerte que "Si no $P$ , entonces $Q$ ", mientras que en la lógica clásica son intercambiables.

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

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

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

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

La mayor parte de la discusión en estas secciones se aplica igualmente bien a la lógica mínima. Pero en cuanto al silogismo disyuntivo con general $\psi$ y en su forma de proposición única, la lógica mínima puede, como máximo, demostrar $(\neg \phi \lor \psi )\to {\big (}\neg \neg \phi \to (\bot \lor \psi ){\big )}$ La conclusión final aquí todavía implica $\neg \neg \psi$ , pero para - en todos los casos - simplificarlo aún más a $\psi$ requiere explosión.

Equivalencias

Las listas anteriores también contienen equivalencias. La equivalencia que involucra una conjunción y una disyunción proviene de $(P\lor Q)\to R$ en realidad ser más fuerte que $P\to R$ Ambos lados de la equivalencia pueden entenderse como conjunciones de implicaciones independientes. Arriba, absurdo $\bot$ se utiliza para $R$ . En las interpretaciones funcionales, corresponde a construcciones de cláusulas condicionales . Por ejemplo, "No ( $P$ o $Q$ )" es equivalente a "No $P$ y tampoco $Q$ ".

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

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

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

$(\phi \to \psi )\leftrightarrow ((\phi \lor \psi )\leftrightarrow \psi )$
$(\phi \to \psi )\leftrightarrow ((\phi \land \psi )\leftrightarrow \phi )$
$(\phi \land \psi )\leftrightarrow ((\phi \to \psi )\leftrightarrow \phi )$
$(\phi \land \psi )\leftrightarrow (((\phi \lor \psi )\leftrightarrow \psi )\leftrightarrow \phi )$

Sucesivamente, $\{\lor ,\leftrightarrow ,\bot \}$ y $\{\lor ,\leftrightarrow ,\neg \}$ son bases completas de conectores intuicionistas, por ejemplo.

Conectores funcionalmente completos

Como lo demostró Alexander V. Kuznetsov , cualquiera de los siguientes conectores —el primero ternario, el segundo quinario— es por sí mismo funcionalmente completo : cualquiera de ellos puede servir como un único operador suficiente para la lógica proposicional intuicionista, formando así un análogo del golpe de Sheffer de la lógica proposicional clásica: ^{[ 6 ]}

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

Semántica

La semántica es bastante más compleja que en el caso clásico. Una teoría de modelos puede estar dada por álgebras de Heyting o, equivalentemente, por la semántica de Kripke . En 2014, Bob Constable demostró la completitud de una teoría de modelos similar a la de Tarski , pero con una noción de completitud distinta a la clásica. ^[⁷^]

En lógica intuicionista, las afirmaciones no probadas no tienen un tercer valor de verdad (como a veces se afirma erróneamente). Se puede demostrar que tales afirmaciones carecen de un tercer valor de verdad, un resultado que se remonta a Glivenko en 1928. ^{[ 1 ]} En cambio, su valor de verdad permanece desconocido hasta que se prueban o se refutan. 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 una lógica bivaluada, ni siquiera como una lógica de valores finitos, en el sentido familiar. Aunque la lógica intuicionista conserva las proposiciones triviales $\{\top ,\bot \}$ Desde la lógica clásica, cada prueba de una fórmula proposicional se considera un valor proposicional válido; por lo tanto, según la noción de Heyting de proposiciones como conjuntos, las fórmulas proposicionales son conjuntos (potencialmente no finitos) de sus pruebas.

Semántica del álgebra de Heyting

En lógica clásica, a menudo se discuten los valores de verdad que puede tomar una fórmula. Estos valores suelen elegirse como los elementos de un álgebra booleana . Las operaciones de intersección y unión en el álgebra booleana se identifican con los conectores lógicos ∧ y ∨, de modo que el valor de una fórmula de la forma A ∧ B es la intersección del valor de A y el valor de B en el álgebra booleana. Entonces, tenemos el útil teorema 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 cualquier valuación , es decir, para cualquier asignación de valores a sus variables.

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

Se puede demostrar que para reconocer fórmulas válidas, basta con considerar un único álgebra de Heyting cuyos elementos son los subconjuntos abiertos de la recta real R. [ ^{8 ] En} esta álgebra tenemos:

{\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 relativa a A → B nos permite calcular el valor de ¬ A :

{\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 toda la línea. ^{[ 8 ]} 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 toda la línea:

{\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 tercero excluido, A ∨ ¬ A , es inválida utilizando un valor específico del conjunto de números reales positivos para A :

{\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 intuicionistamente válida en el álgebra de Heyting infinita descrita anteriormente da como resultado que el elemento superior, que representa lo verdadero, sea la valoración de la fórmula, independientemente de los valores del álgebra que se asignen a las variables de la fórmula. ^{[ 8 ]} Por el contrario, para cada fórmula inválida, existe una asignación de valores a las variables que produce una valoración que difiere del elemento superior. ^{[ 9 ]}^{[ 10 ]} Ningún álgebra de Heyting finita posee la segunda de estas dos propiedades. ^{[ 8 ]}

Semántica de Kripke

Partiendo de 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. ^{[ 11 ]}^{[ 12 ]}^{[ 4 ]}

Semántica al estilo Tarski

Se descubrió que no era posible demostrar la completitud de la semántica tipo Tarski para la lógica intuicionista. 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 tipo Tarski. En esta noción de completitud, no nos interesan todas las proposiciones que son verdaderas para cada modelo, sino las proposiciones que son verdaderas de la misma manera en cada modelo. Es decir, una única prueba de que el modelo considera verdadera una fórmula debe ser válida para cada modelo. En este caso, no solo existe una prueba de completitud, sino una que es válida según la lógica intuicionista. ^{[ 7 ]}

Metalogic

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 $(\neg A)\to (B\lor C)$ Si es demostrable, entonces también lo es. $(\neg A\to B)\lor (\neg A\to C)$ Otro ejemplo es que $(A\to B)\to (A\lor C)$ Que sea demostrable siempre también significa que también lo es. ${\big (}(A\to B)\to A{\big )}\lor {\big (}(A\to B)\to C{\big )}$ Se dice que el sistema está cerrado bajo estas implicaciones como reglas y que pueden ser adoptadas.

Características de las teorías

Las teorías sobre lógicas constructivas pueden exhibir la propiedad de disyunción . El cálculo proposicional intuicionista puro también lo hace.

En particular, esto significa que la disyunción del tercero excluido para una afirmación irrechazable $A$ es demostrable exactamente cuando $A$ es demostrable.

Si una teoría con la propiedad de disyunción tiene proposiciones indecidibles, las disyunciones del medio excluido de algunasLas disyunciones del medio excluido tampoco son demostrables.

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 . ^{[ 13 ]}

El subsistema de la lógica intuicionista al que se le ha eliminado el axioma FALSO (o NO-2) se conoce como lógica mínima , y algunas de sus diferencias se han explicado con más detalle anteriormente.

Lógicas intermedias

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

Por ejemplo, para un esquema que no involucre negaciones, consideremos el esquema clásicamente válido. $(A\to B)\lor (B\to A)$ . Al adoptar esto en lugar de la lógica intuicionista, se obtiene la lógica intermedia llamada lógica de Gödel-Dummett .

Relación con la lógica clásica

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

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

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

$(\neg \phi \to \neg \chi )\to (\chi \to \phi )$

Estos detalles se explican 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 Kripke de dos elementos. $\circ {\longrightarrow }\circ$ (en otras palabras, eso no está incluido en la lógica de Smetanich ).

Lógica multivaluada

El trabajo de Kurt Gödel sobre lógica multivaluada demostró en 1932 que la lógica intuicionista no es una lógica de valores finitos . ^{[ 14 ]} (Véase la sección titulada « Semántica del álgebra de Heyting» más arriba para una interpretación de la lógica intuicionista en términos de lógica de valores infinitos ).

Lógica modal

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

{\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}}

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. ^{[ 15 ]} 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. ^{[ 16 ]}

Cálculo lambda

Existe una correspondencia extendida de Curry-Howard entre IPC y el cálculo lambda simplemente tipado . ^{[ 16 ]}

Véase también

Notas

1 2 Van Atten 2022 .
↑ Shehtman 1990 .
↑ Japaridze 2009 .
^ Bezhanishvili y De Jongh , pág. 8.
↑ Takeuti 2013 .
^ Chagrov y Zakharyaschev 1997 , págs .
1 2 Constable & Bickford 2014 .
^ Sørensen y Urzyczyn 2006 , pág .42.
↑ Tarski 1938 .
^ Rasiowa y Sikorski 1963 , págs. 385–386.
↑ Kripke 1965 .
↑ Moschovakis 2022 .
↑ Aoyama 2004 .
↑ Burgess 2014 .
↑ Lévy 2011 , págs. 4–5.
1 2 Alechina et al. 2003 .

Referencias

Alechina, Natasha; Mendler, Michael; De Paiva, Valeria ; Ritter, Eike (enero de 2003). Semántica categórica y de Kripke para la lógica modal constructiva S4 (PDF) . Actas del 15.º Taller Internacional sobre Lógica en Ciencias de la Computación. Lecture Notes in Computer Science . doi : 10.1007/3-540-44802-0_21 . Archivado del original (PDF) el 26 de marzo de 2015. Consultado el 23 de enero de 2014 .
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). "Antiintuicionismo 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 el 12 de julio de 2025).{{cite web}}: CS1 maint: DOI inactivo desde julio de 2025 ( enlace )
Chagrov, Alexander; Zakharyaschev, Michael (1997). Lógica modal . Oxford Logic Guides. Vol. 35. Oxford University Press . pp. XV, 605. ISBN 0-19-853779-4.
Constable, R.; Bickford, M. (2014). "Completitud intuicionista de la lógica de primer orden". Annals of Pure and Applied Logic . 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 . pp. 224–257 . doi : 10.1002/9781405164801.ch11 . ISBN 9780631206934.
Van Heijenoort, Jean (2002) [1967]. De Frege a Gödel: Un libro de referencia en lógica matemática, 1879-1931 (edición reimpresa con correcciones ). Harvard University Press . ISBN 9780674324497OCLC 749638436
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 fue la semántica de los juegos?" . En Majer, O.; Pietarinen, A.-V.; Tulenheimo, T. (eds.). Juegos: Unificando 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 en lógica y fundamentos de las matemáticas. Vol. 40. Ámsterdam: North-Holland Publishing Company . pp. 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 en 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 demostración (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.). Enciclopedia de filosofía de Stanford . ISSN 1095-5054 . OCLC 429049174 .

McCarty, David Charles (2009). «Intuicionismo en matemáticas». En Shapiro, Stewart (ed.). The Oxford Handbook of Philosophy of Mathematics and Logic . pp. 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.). Enciclopedia de filosofía de Stanford ( edición de invierno de 2022). ISSN 1095-5054 . OCLC 429049174 .

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

[FOOTNOTEVan_Atten2022-1] 1 2 Van Atten 2022 .

[FOOTNOTEShehtman1990-2] Shehtman 1990 .

[FOOTNOTEJaparidze2009-3] Japaridze 2009 .

[FOOTNOTEBezhanishviliDe_Jongh8-4] Bezhanishvili y De Jongh , pág. 8.

[FOOTNOTETakeuti2013-5] Takeuti 2013 .

[FOOTNOTEChagrovZakharyaschev199758–59-6] Chagrov y Zakharyaschev 1997 , págs .

[FOOTNOTEConstableBickford2014-7] 1 2 Constable & Bickford 2014 .

[FOOTNOTESørensenUrzyczyn200642-8] Sørensen y Urzyczyn 2006 , pág .42.

[FOOTNOTETarski1938-9] Tarski 1938 .

[FOOTNOTERasiowaSikorski1963385–386-10] Rasiowa y Sikorski 1963 , págs. 385–386.

[FOOTNOTEKripke1965-11] Kripke 1965 .

[FOOTNOTEMoschovakis2022-12] Moschovakis 2022 .

[FOOTNOTEAoyama2004-13] Aoyama 2004 .

[FOOTNOTEBurgess2014-14] Burgess 2014 .

[FOOTNOTELévy20114–5-15] Lévy 2011 , págs. 4–5.

[FOOTNOTEAlechinaMendlerDe_PaivaRitter2003-16] 1 2 Alechina et al. 2003 .

[

[

[

[ 4 ]

[ 5 ]

[ 6 ]

[

8 ] En

[ 9 ]

[ 10 ]

[ 11 ]

[ 12 ]

[ 13 ]

[ 14 ]

[ 15 ]

[ 16 ]