Lista de sistemas axiomáticos en lógica

Este artículo contiene una lista de ejemplos de sistemas deductivos de estilo Hilbert para lógica proposicional .

Sistemas de cálculo proposicional clásico

El cálculo proposicional clásico es la lógica proposicional estándar. Su semántica pretendida es bivalente y su propiedad principal es que es fuertemente completa , es decir, siempre que una fórmula se sigue semánticamente de un conjunto de premisas, también se sigue sintácticamente de ese conjunto. Se han formulado muchos sistemas axiomáticos completos equivalentes diferentes. Se diferencian en la elección de los conectivos básicos utilizados, que en todos los casos tienen que ser funcionalmente completos (es decir, capaces de expresar por composición todas las tablas de verdad n -arias ), y en la elección completa exacta de axiomas sobre la base elegida de conectivos.

Implicación y negación

Las formulaciones aquí utilizan la implicación y la negación como un conjunto funcionalmente completo de conectivos básicos. Todo sistema lógico requiere al menos una regla de inferencia no nula . El cálculo proposicional clásico utiliza típicamente la regla del modus ponens : ${\displaystyle \{\to ,\neg \}}$

${\displaystyle {\frac {A,A\to B}{B}}.}$

Asumimos que esta regla está incluida en todos los sistemas a continuación, a menos que se indique lo contrario.

Sistema de axiomas de Frege : ^[1]

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

${\displaystyle (A\to (B\to C))\to (B\to (A\to C))}$

${\displaystyle (A\to B)\to (\neg B\to \neg A)}$

${\displaystyle \neg \neg A\to A}$

${\displaystyle A\to \neg \neg A}$

Sistema de axiomas de Hilbert : ^[1]

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to (B\to C))\to (B\to (A\to C))}$

${\displaystyle (B\to C)\to ((A\to B)\to (A\to C))}$

${\displaystyle A\to (\neg A\to B)}$

${\displaystyle (A\to B)\to ((\neg A\to B)\to B)}$

Sistemas de axiomas de Łukasiewicz : ^[1]

• Primero:

  ${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

  ${\displaystyle (\neg A\to A)\to A}$

  ${\displaystyle A\to (\neg A\to B)}$

• Segundo:

  ${\displaystyle ((A\to B)\to C)\to (\neg A\to C)}$

  ${\displaystyle ((A\to B)\to C)\to (B\to C)}$

  ${\displaystyle (\neg A\to C)\to ((B\to C)\to ((A\to B)\to C))}$

• Tercero:

  ${\displaystyle A\to (B\to A)}$

  ${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

  ${\displaystyle (\neg A\to \neg B)\to (B\to A)}$

Sistema de axiomas de Arai: ^[2]

${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

${\displaystyle A\to (\neg A\to B)}$

${\displaystyle (\neg A\to B)\to ((B\to A)\to A)}$

Sistema de axiomas de Łukasiewicz y Tarski : ^[3]

${\displaystyle [(A\to (B\to A))\to ([(\neg C\to (D\to \neg E))\to [(C\to (D\to F))\to ((E\to D)\to (E\to F))]]\to G)]\to (H\to G)}$

El sistema de axiomas de Meredith :

${\displaystyle ((((A\to B)\to (\neg C\to \neg D))\to C)\to E)\to ((E\to A)\to (D\to A))}$

Sistema de axiomas de Mendelson : ^[4]

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

${\displaystyle (\neg A\to \neg B)\to ((\neg A\to B)\to A)}$

El sistema de axiomas de Russell : ^[1]

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

${\displaystyle (A\to (B\to C))\to (B\to (A\to C))}$

${\displaystyle \neg \neg A\to A}$

${\displaystyle (A\to \neg A)\to \neg A}$

${\displaystyle (A\to \neg B)\to (B\to \neg A)}$

Sistemas de axiomas de Sobociński: ^[1]

• Primero:

  ${\displaystyle \neg A\to (A\to B)}$

  ${\displaystyle A\to (B\to (C\to A))}$

  ${\displaystyle (\neg A\to C)\to ((B\to C)\to ((A\to B)\to C))}$

• Segundo:

  ${\displaystyle (A\to B)\to (\neg B\to (A\to C))}$

  ${\displaystyle A\to (B\to (C\to A))}$

  ${\displaystyle (\neg A\to B)\to ((A\to B)\to B)}$

Implicación y falsedad

En lugar de la negación, la lógica clásica también puede formularse utilizando el conjunto funcionalmente completo de conectivos. ${\displaystyle \{\to ,\bot \}}$

Sistema de axiomas de Tarski- Bernays -Wajsberg:

${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

${\displaystyle A\to (B\to A)}$

${\displaystyle ((A\to B)\to A)\to A}$

${\displaystyle \bot \to A}$

El sistema de axiomas de la Iglesia :

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

${\displaystyle ((A\to \bot )\to \bot )\to A}$

Los sistemas de axiomas de Meredith:

• Primero: ^{[5] [6] [7]}

  ${\displaystyle ((((A\to B)\to (C\to \bot ))\to D)\to E)\to ((E\to A)\to (C\to A))}$

• Segundo: ^[5]

  ${\displaystyle ((A\to B)\to ((\bot \to C)\to D))\to ((D\to A)\to (E\to (F\to A)))}$

Negación y disyunción

En lugar de la implicación, la lógica clásica también puede formularse utilizando el conjunto funcionalmente completo de conectivos. Estas formulaciones utilizan la siguiente regla de inferencia: ${\displaystyle \{\neg ,\lor \}}$

${\displaystyle {\frac {A,\neg A\lor B}{B}}.}$

Sistema de axiomas de Russell-Bernays:

${\displaystyle \neg (\neg B\lor C)\lor (\neg (A\lor B)\lor (A\lor C))}$

${\displaystyle \neg (A\lor B)\lor (B\lor A)}$

${\displaystyle \neg A\lor (B\lor A)}$

${\displaystyle \neg (A\lor A)\lor A}$

Los sistemas axiomáticos de Meredith: ^[8]

• Primero:

  ${\displaystyle \neg (\neg (\neg A\lor B)\lor (C\lor (D\lor E)))\lor (\neg (\neg D\lor A)\lor (C\lor (E\lor A)))}$

• Segundo:

  ${\displaystyle \neg (\neg (\neg A\lor B)\lor (C\lor (D\lor E)))\lor (\neg (\neg E\lor D)\lor (C\lor (A\lor D)))}$

• Tercero:

  ${\displaystyle \neg (\neg (\neg A\lor B)\lor (C\lor (D\lor E)))\lor (\neg (\neg C\lor A)\lor (E\lor (D\lor A)))}$

Dualmente, la lógica proposicional clásica puede definirse utilizando únicamente la conjunción y la negación.

Conjunción y negación

Rosser J. Barkley creó un sistema basado en la conjunción y la negación , con el modus ponens como regla de inferencia. En su libro, ^[9] utilizó la implicación para presentar sus esquemas axiomáticos. " " es una abreviatura de " ": ${\displaystyle \{\wedge ,\neg \}}$ ${\displaystyle C\rightarrow D}$ ${\displaystyle \neg (C\wedge \neg D)}$

• ${\displaystyle A\rightarrow A\wedge A}$
• ${\displaystyle A\wedge B\rightarrow A}$
• ${\displaystyle \left(A\rightarrow B\right)\rightarrow \left(\neg \left(B\wedge C\right)\rightarrow \neg \left(C\wedge A\right)\right)}$

Si no utilizamos la abreviatura, obtenemos los esquemas axiomáticos en la siguiente forma:

• ${\displaystyle \neg (A\wedge \neg (A\wedge A))}$
• ${\displaystyle \neg ((A\wedge B)\wedge \neg A)}$
• ${\displaystyle \neg \left(\neg \left(A\wedge \neg B\right)\wedge \neg \neg \left(\neg \left(B\wedge C\right)\wedge \neg \neg \left(C\wedge A\right)\right)\right)}$

Además, modus ponens se convierte en:

• ${\displaystyle {\frac {A,\neg \left(A\wedge \neg B\right)}{B}}}$

Derrame cerebral de Sheffer

Debido a que el trazo de Sheffer (también conocido como operador NAND) es funcionalmente completo , se puede utilizar para crear una formulación completa de cálculo proposicional. Las formulaciones NAND utilizan una regla de inferencia llamada modus ponens de Nicod :

${\displaystyle {\frac {A,A\mid (B\mid C)}{C}}.}$

Sistema de axiomas de Nicod: ^[5]

${\displaystyle (A\mid (B\mid C))\mid [(E\mid (E\mid E))\mid ((D\mid B)\mid [(A\mid D)\mid (A\mid D)])]}$

Sistemas de axiomas de Łukasiewicz: ^[5]

• Primero:

  ${\displaystyle (A\mid (B\mid C))\mid [(D\mid (D\mid D))\mid ((D\mid B)\mid [(A\mid D)\mid (A\mid D)])]}$

• Segundo:

  ${\displaystyle (A\mid (B\mid C))\mid [(A\mid (C\mid A))\mid ((D\mid B)\mid [(A\mid D)\mid (A\mid D)])]}$

Sistema de axiomas de Wajsberg: ^[5]

${\displaystyle (A\mid (B\mid C))\mid [((D\mid C)\mid [(A\mid D)\mid (A\mid D)])\mid (A\mid (A\mid B))]}$

Sistemas de axiomas de Argonne : ^[5]

• Primero:

${\displaystyle (A\mid (B\mid C))\mid [(A\mid (B\mid C))\mid ((D\mid C)\mid [(C\mid D)\mid (A\mid D)])]}$

• Segundo:

${\displaystyle (A\mid (B\mid C))\mid [([(B\mid D)\mid (A\mid D)]\mid (D\mid B))\mid ((C\mid B)\mid A)]}$^[10]

El análisis informático realizado por Argonne ha revelado más de 60 sistemas de axiomas únicos adicionales que pueden utilizarse para formular el cálculo proposicional NAND. ^[7]

Cálculo proposicional implicacional

El cálculo proposicional implicacional es el fragmento del cálculo proposicional clásico que sólo admite la implicación conectiva. No es funcionalmente completo (porque carece de la capacidad de expresar falsedad y negación), pero sí sintácticamente completo . Los cálculos implicacionales que se presentan a continuación utilizan el modus ponens como regla de inferencia.

Sistema de axiomas de Bernays-Tarski: ^[11]

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

${\displaystyle ((A\to B)\to A)\to A}$

Sistemas de axiomas de Łukasiewicz y Tarski:

• Primero: ^[11]

  ${\displaystyle [(A\to (B\to A))\to [([((C\to D)\to E)\to F]\to [(D\to F)\to (C\to F)])\to G]]\to G}$

• Segundo: ^[11]

  ${\displaystyle [(A\to B)\to ((C\to D)\to E)]\to ([F\to ((C\to D)\to E)]\to [(A\to F)\to (D\to E)])}$

• Tercero:

  ${\displaystyle ((A\to B)\to (C\to D))\to (E\to ((D\to A)\to (C\to A)))}$

• Cuatro:

  ${\displaystyle ((A\to B)\to (C\to D))\to ((D\to A)\to (E\to (C\to A)))}$

Sistema de axiomas de Łukasiewicz: ^{[12] [11]}

${\displaystyle ((A\to B)\to C)\to ((C\to A)\to (D\to A))}$

Lógica intuicionista e intermedia

La lógica intuicionista es un subsistema de la lógica clásica. Se formula comúnmente como el conjunto de conectivos básicos (funcionalmente completos). No es sintácticamente completa ya que carece del término medio excluido A∨¬A o de la ley de Peirce ((A→B)→A)→A que pueden añadirse sin que la lógica resulte inconsistente. Tiene el modus ponens como regla de inferencia y los siguientes axiomas: ${\displaystyle \{\to ,\land ,\lor ,\bot \}}$

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

${\displaystyle (A\land B)\to A}$

${\displaystyle (A\land B)\to B}$

${\displaystyle A\to (B\to (A\land B))}$

${\displaystyle A\to (A\lor B)}$

${\displaystyle B\to (A\lor B)}$

${\displaystyle (A\to C)\to ((B\to C)\to ((A\lor B)\to C))}$

${\displaystyle \bot \to A}$

Alternativamente, la lógica intuicionista puede axiomatizarse utilizando como conjunto de conectivos básicos, reemplazando el último axioma con ${\displaystyle \{\to ,\land ,\lor ,\neg \}}$

${\displaystyle (A\to \neg A)\to \neg A}$

${\displaystyle \neg A\to (A\to B)}$

Las lógicas intermedias se encuentran entre la lógica intuicionista y la lógica clásica. A continuación se presentan algunas lógicas intermedias:

• La lógica de Jankov (KC) es una extensión de la lógica intuicionista, que puede axiomatizarse mediante el sistema de axiomas intuicionistas más el axioma ^[13]

${\displaystyle \neg A\lor \neg \neg A.}$

• La lógica de Gödel-Dummett (LC) se puede axiomatizar sobre la lógica intuicionista añadiendo el axioma ^[13]

${\displaystyle (A\to B)\lor (B\to A).}$

Cálculo implicacional positivo

El cálculo implicacional positivo es el fragmento implicacional de la lógica intuicionista. Los cálculos que se presentan a continuación utilizan el modus ponens como regla de inferencia.

El sistema de axiomas de Łukasiewicz:

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

Los sistemas de axiomas de Meredith:

• Primero:

  ${\displaystyle E\to ((A\to B)\to (((D\to A)\to (B\to C))\to (A\to C)))}$

• Segundo:

  ${\displaystyle A\to (B\to A)}$

  ${\displaystyle (A\to B)\to ((A\to (B\to C))\to (A\to C))}$

• Tercero:

  ${\displaystyle ((A\to B)\to C)\to (D\to ((B\to (C\to E))\to (B\to E)))}$^[14]

Sistemas de axiomas de Hilbert:

• Primero:

  ${\displaystyle (A\to (A\to B))\to (A\to B)}$

  ${\displaystyle (B\to C)\to ((A\to B)\to (A\to C))}$

  ${\displaystyle (A\to (B\to C))\to (B\to (A\to C))}$

  ${\displaystyle A\to (B\to A)}$

• Segundo:

  ${\displaystyle (A\to (A\to B))\to (A\to B)}$

  ${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

  ${\displaystyle A\to (B\to A)}$

• Tercero:

  ${\displaystyle A\to A}$

  ${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

  ${\displaystyle (B\to C)\to ((A\to B)\to (A\to C))}$

  ${\displaystyle (A\to (A\to B))\to (A\to B)}$

Cálculo proposicional positivo

El cálculo proposicional positivo es el fragmento de la lógica intuicionista que utiliza únicamente los conectivos (no funcionalmente completos) . Puede axiomatizarse mediante cualquiera de los cálculos mencionados anteriormente para el cálculo implicacional positivo junto con los axiomas ${\displaystyle \{\to ,\land ,\lor \}}$

${\displaystyle (A\land B)\to A}$

${\displaystyle (A\land B)\to B}$

${\displaystyle A\to (B\to (A\land B))}$

${\displaystyle A\to (A\lor B)}$

${\displaystyle B\to (A\lor B)}$

${\displaystyle (A\to C)\to ((B\to C)\to ((A\lor B)\to C))}$

Opcionalmente, también podemos incluir el conectivo y los axiomas. ${\displaystyle \leftrightarrow }$

${\displaystyle (A\leftrightarrow B)\to (A\to B)}$

${\displaystyle (A\leftrightarrow B)\to (B\to A)}$

${\displaystyle (A\to B)\to ((B\to A)\to (A\leftrightarrow B))}$

La lógica mínima de Johansson puede axiomatizarse mediante cualquiera de los sistemas axiomáticos para el cálculo proposicional positivo y ampliando su lenguaje con el conectivo nulario , sin esquemas axiomáticos adicionales. Alternativamente, también puede axiomatizarse en el lenguaje ampliando el cálculo proposicional positivo con el axioma ${\displaystyle \bot }$ ${\displaystyle \{\to ,\land ,\lor ,\neg \}}$

${\displaystyle (A\to \neg B)\to (B\to \neg A)}$

o el par de axiomas

${\displaystyle (A\to B)\to (\neg B\to \neg A)}$

${\displaystyle A\to \neg \neg A}$

La lógica intuicionista en el lenguaje con negación puede axiomatizarse sobre el cálculo positivo mediante el par de axiomas

${\displaystyle (A\to \neg B)\to (B\to \neg A)}$

${\displaystyle \neg A\to (A\to B)}$

o el par de axiomas ^[15]

${\displaystyle (A\to \neg A)\to \neg A}$

${\displaystyle \neg A\to (A\to B)}$

La lógica clásica en el lenguaje se puede obtener a partir del cálculo proposicional positivo añadiendo el axioma ${\displaystyle \{\to ,\land ,\lor ,\neg \}}$

${\displaystyle (\neg A\to \neg B)\to (B\to A)}$

o el par de axiomas

${\displaystyle (A\to \neg B)\to (B\to \neg A)}$

${\displaystyle \neg \neg A\to A}$

El cálculo de Fitch toma cualquiera de los sistemas de axiomas para el cálculo proposicional positivo y agrega los axiomas ^[15]

${\displaystyle \neg A\to (A\to B)}$

${\displaystyle A\leftrightarrow \neg \neg A}$

${\displaystyle \neg (A\lor B)\leftrightarrow (\neg A\land \neg B)}$

${\displaystyle \neg (A\land B)\leftrightarrow (\neg A\lor \neg B)}$

Nótese que el primer y tercer axioma también son válidos en la lógica intuicionista.

Cálculo equivalente

El cálculo de equivalencias es el subsistema del cálculo proposicional clásico que sólo permite el conectivo de equivalencia (funcionalmente incompleto) , denotado aquí como . La regla de inferencia utilizada en estos sistemas es la siguiente: ${\displaystyle \equiv }$

${\displaystyle {\frac {A,A\equiv B}{B}}.}$

Sistema de axiomas de Iséki: ^[16]

${\displaystyle ((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)}$

${\displaystyle (A\equiv (B\equiv C))\equiv ((A\equiv B)\equiv C)}$

Sistema de axiomas de Iséki-Arai: ^[17]

${\displaystyle A\equiv A}$

${\displaystyle (A\equiv B)\equiv (B\equiv A)}$

${\displaystyle (A\equiv B)\equiv ((B\equiv C)\equiv (A\equiv C))}$

Sistemas de axiomas de Arai;

• Primero:

  ${\displaystyle (A\equiv (B\equiv C))\equiv ((A\equiv B)\equiv C)}$

  ${\displaystyle ((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)}$

• Segundo:

  ${\displaystyle (A\equiv B)\equiv (B\equiv A)}$

  ${\displaystyle ((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)}$

Sistemas de axiomas de Łukasiewicz: ^[18]

• Primero:

  ${\displaystyle (A\equiv B)\equiv ((C\equiv B)\equiv (A\equiv C))}$

• Segundo:

  ${\displaystyle (A\equiv B)\equiv ((A\equiv C)\equiv (C\equiv B))}$

• Tercero:

  ${\displaystyle (A\equiv B)\equiv ((C\equiv A)\equiv (B\equiv C))}$

Los sistemas axiomáticos de Meredith: ^[18]

• Primero:

  ${\displaystyle ((A\equiv B)\equiv C)\equiv (B\equiv (C\equiv A))}$

• Segundo:

  ${\displaystyle A\equiv ((B\equiv (A\equiv C))\equiv (C\equiv B))}$

• Tercero:

  ${\displaystyle (A\equiv (B\equiv C))\equiv (C\equiv (A\equiv B))}$

• Cuatro:

  ${\displaystyle (A\equiv B)\equiv (C\equiv ((B\equiv C)\equiv A))}$

• Quinto:

  ${\displaystyle (A\equiv B)\equiv (C\equiv ((C\equiv B)\equiv A))}$

• Sexto:

  ${\displaystyle ((A\equiv (B\equiv C))\equiv C)\equiv (B\equiv A)}$

• Séptimo:

  ${\displaystyle ((A\equiv (B\equiv C))\equiv B)\equiv (C\equiv A)}$

Sistema de axiomas de Kalman: ^[18]

${\displaystyle A\equiv ((B\equiv (C\equiv A))\equiv (C\equiv B))}$

Sistemas de axiomas de Winker: ^[18]

• Primero:

  ${\displaystyle A\equiv ((B\equiv C)\equiv ((A\equiv C)\equiv B))}$

• Segundo:

  ${\displaystyle A\equiv ((B\equiv C)\equiv ((C\equiv A)\equiv B))}$

Sistema de axiomas XCB: ^[18]

${\displaystyle A\equiv (((A\equiv B)\equiv (C\equiv B))\equiv C)}$

Véase también

• Lógica paraconsistente § Incluido : una lista de esquemas axiomáticos para una lógica paraconsistente del estilo de Hilbert

Referencias

1. Yasuyuki Imai, Kiyoshi Iséki, Sobre sistemas axiomáticos de cálculos proposicionales, I, Actas de la Academia Japonesa. Volumen 41, Número 6 (1965), 436–439.
2. Yoshinari Arai, Sobre sistemas axiomáticos de cálculos proposicionales, II, Actas de la Academia Japonesa. Volumen 41, Número 6 (1965), 440–442.
3. Parte XIII: Shôtarô Tanaka. Sobre sistemas axiomáticos de cálculos proposicionales, XIII. Proc. Japan Acad., Volumen 41, Número 10 (1965), 904–907.
4. Elliott Mendelson, Introducción a la lógica matemática , Van Nostrand, Nueva York, 1979, pág. 31.
5. [Fitelson, 2001] "Nuevas axiomatizaciones elegantes de algunas lógicas oracionales" por Branden Fitelson
6. (El análisis computacional realizado por Argonne ha revelado que este es el axioma individual más corto con menos variables para el cálculo proposicional).
7. "Algunos resultados nuevos en cálculos lógicos obtenidos mediante razonamiento automatizado", Zac Ernst, Ken Harris y Branden Fitelson, http://www.mcs.anl.gov/research/projects/AR/award-2001/fitelson.pdf
8. C. Meredith, Axiomas simples para los sistemas (C, N), (C, 0) y (A, N) del cálculo proposicional de dos valores , Journal of Computing Systems, págs. 155-164, 1954.
9. Rosser J. Barkley, "Lógica para matemáticos", Nueva York, McGraw-Hill, 1953. [1]
10. , p. 9, Un espectro de aplicaciones del razonamiento automatizado, Larry Wos; arXiv:cs/0205078v1
11. Investigaciones sobre el cálculo oracional en lógica, semántica y metamatemática: artículos de 1923 a 1938 de Alfred Tarski , Corcoran, J., ed. Hackett. Primera edición editada y traducida por JH Woodger, Oxford Uni. Press. (1956)
12. Łukasiewicz, J.. (1948). El axioma más corto del cálculo implicacional de proposiciones. Actas de la Real Academia Irlandesa. Sección A: Ciencias matemáticas y físicas, 52, 25–33. Recuperado de https://www.jstor.org/stable/20488489
13. A. Chagrov, M. Zakharyaschev, Lógica modal , Oxford University Press, 1997.
14. C. Meredith, Un único axioma de lógica positiva , Journal of Computing Systems, pág. 169-170, 1954.
15. LH Hackstaff, Sistemas de lógica formal , Springer, 1966.
16. Kiyoshi Iséki, Sobre sistemas axiomáticos de cálculos proposicionales, XV, Actas de la Academia Japonesa. Volumen 42, Número 3 (1966), 217–220.
17. Yoshinari Arai, Sobre sistemas axiomáticos de cálculos proposicionales, XVII, Actas de la Academia Japonesa. Volumen 42, Número 4 (1966), 351–354.
18. XCB, el último de los axiomas individuales más cortos para el cálculo equivalente clásico, LARRY WOS, DOLPH ULRICH, BRANDEN FITELSON; arXiv:cs/0211015v1