Lista de sistemas Hilbert

Este artículo contiene una lista de ejemplos de sistemas deductivos 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 prevista es bivalente y su propiedad principal es que es fuertemente completa , de lo contrario se dice que 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 de axiomas 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 exacta y completa de los axiomas sobre la base de conectivos elegida.

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 suele utilizar 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 siguientes 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}$

El 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)}$

• Cuarto: ^{[ cita necesaria ]}

  ${\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 : ^[2]

${\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 : ^[3]

${\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 falso

En lugar de la negación, la lógica clásica también se puede formular 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 Church :

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

Sistemas de axiomas de Meredith:

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

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

• Segundo: ^[4]

  ${\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 implicaciones, la lógica clásica también se puede formular 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}$

Sistemas de axiomas de Meredith: ^[7]

• 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)))}$

De manera dual, la lógica proposicional clásica se puede definir utilizando únicamente conjunción y 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, ^[8] utilizó la implicación para presentar sus esquemas de axiomas. " " 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 usamos la abreviatura, obtenemos los esquemas de axiomas de 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, el modus ponens pasa a ser:

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

El 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: ^[4]

${\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: ^[4]

• 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: ^[4]

${\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 : ^[4]

• 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)]}$^[9]

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

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í lo es sintácticamente . Los cálculos implicacionales que aparecen a continuación utilizan el modus ponens como regla de inferencia.

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

${\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: ^[10]

  ${\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: ^[10]

  ${\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: ^{[11] [10]}

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

Lógicas intuicionistas e intermedias

La lógica intuicionista es un subsistema de la lógica clásica. Comúnmente se formula como el conjunto de conectivos básicos (funcionalmente completos). No es sintácticamente completo ya que carece del medio excluido A∨¬A o la ley de Peirce ((A→B)→A)→A que se puede agregar sin hacer que la lógica sea inconsistente. Tiene como regla de inferencia el modus ponens 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 por ${\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. Aquí hay algunas lógicas intermedias:

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

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

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

${\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 siguientes utilizan el modus ponens como regla de inferencia.

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))}$

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)))}$^[13]

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 ser axiomatizado 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 ser axiomatizada mediante cualquiera de los sistemas de axiomas del cálculo proposicional positivo y ampliando su lenguaje con el conectivo nular , sin esquemas de axiomas adicionales. Alternativamente, también se puede axiomatizar en el lenguaje expandiendo 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 ser axiomatizada 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 ^[14]

${\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 sumando 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 del cálculo proposicional positivo y suma los axiomas ^[14]

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

Tenga en cuenta que el primer y tercer axiomas también son válidos en lógica intuicionista.

Cálculo equivalente

El cálculo equivalente es el subsistema del cálculo proposicional clásico que solo 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}}.}$

El sistema de axiomas de Iséki: ^[15]

${\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: ^[16]

${\displaystyle A\equiv A}$

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

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

Los 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: ^[17]

• 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))}$

Sistemas de axiomas de Meredith: ^[17]

• 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: ^[17]

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

Sistemas de axiomas de Winker: ^[17]

• 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: ^[17]

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

Ver también

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

Referencias

1. Yasuyuki Imai, Kiyoshi Iséki, Sobre sistemas de axiomas de cálculo proposicional, I, Actas de la Academia de Japón. Volumen 41, Número 6 (1965), 436–439.
2. Parte XIII: Shôtarô Tanaka. Sobre sistemas de axiomas de cálculos proposicionales, XIII. Proc. Japan Acad., Volumen 41, Número 10 (1965), 904–907.
3. Elliott Mendelson, Introducción a la lógica matemática , Van Nostrand, Nueva York, 1979, pág. 31.
4. [Fitelson, 2001] "Nuevas axiomatizaciones elegantes de algunas lógicas oracionales" por Branden Fitelson
5. (El análisis informático realizado por Argonne ha revelado que este es el axioma individual más corto con menos variables para el cálculo proposicional).
6. "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
7. C. Meredith, Axiomas únicos 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.
8. Rosser J. Barkley, "Lógica para matemáticos", Nueva York, McGraw-Hill, 1953. [1]
9. , pág. 9, Un espectro de aplicaciones del razonamiento automatizado, Larry Wos; arXiv:cs/0205078v1
10. 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. Prensa. (1956)
11. Łukasiewicz, J. (1948). El axioma más breve del cálculo implicacional de proposiciones. Actas de la Real Academia Irlandesa. Sección A: Ciencias físicas y matemáticas, 52, 25–33. Obtenido de https://www.jstor.org/stable/20488489
12. A. Chagrov, M. Zakharyaschev, Lógica modal , Oxford University Press, 1997.
13. C. Meredith, Un axioma único de lógica positiva , Journal of Computing Systems, p. 169–170, 1954.
14. LH Hackstaff, Sistemas de lógica formal , Springer, 1966.
15. Kiyoshi Iséki, Sobre sistemas de axiomas de cálculo proposicional, XV, Actas de la Academia de Japón. Volumen 42, Número 3 (1966), 217–220.
16. Yoshinari Arai, Sobre sistemas de axiomas de cálculo proposicional, XVII, Actas de la Academia de Japón. Volumen 42, Número 4 (1966), 351–354.
17. 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