Lista de sistemas Hilbert

Este artículo necesita citas adicionales para su verificación . Por favor, ayuda a mejorar este artículo mediante la adición de citas de fuentes confiables . El material no obtenido puede ser cuestionado y eliminado. Buscar fuentes:  "Lista de sistemas Hilbert"  -  noticias  · periódicos  · libros  · académico  · JSTOR ( septiembre de 2010 ) ( Aprenda cómo y cuándo eliminar este mensaje de plantilla )

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

Sistemas clásicos de cálculo proposicional

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 , de lo contrario se dice que siempre que una fórmula se sigue semánticamente de un conjunto de premisas semánticamente, también se sigue de ese conjunto sintácticamente. Se han formulado muchos sistemas de axiomas completos equivalentes diferentes. Se diferencian en la elección de 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í usan 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 generalmente usa la regla del modus ponens :${\displaystyle \{\to ,\neg \}}$

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

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

• Tercera:

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

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

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 se puede formular utilizando el conjunto funcionalmente completo de conectivos.${\displaystyle \{\to ,\bot \}}$

Tarski– Bernays - Sistema de axiomas de 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}$

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 A,\neg A\lor B\vdash 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)))}$

• Tercera:

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

Doblemente, la lógica proposicional clásica se puede definir usando solo conjunción y negación.

Accidente cerebrovascular de Sheffer

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

${\displaystyle A,A\mid (B\mid C)\vdash 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))]}$

Argonne sistemas axiomáticos: ^[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)]}$^[8]

El análisis informático de Argonne ha revelado> 60 sistemas de axioma único adicionales que se pueden utilizar para formular el cálculo proposicional NAND. ^[6]

Cálculo proposicional implícito

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

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

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

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

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

• Tercera:

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

${\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 con el conjunto de conectivos básicos (funcionalmente completos). No es sintácticamente completo ya que carece de A∨¬A central excluida o de la ley de Peirce ((A → B) → A) → A que se puede agregar sin hacer que la lógica sea inconsistente. Tiene 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. 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 por el sistema de axioma intuicionista más el axioma ^[11]

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

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

Cálculo de implicaciones positivas

El cálculo implicacional positivo es el fragmento implicacional de la lógica intuicionista. Los cálculos siguientes utilizan 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))}$

• Tercera:

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

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

• Tercera:

  ${\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 lógica intuicionista que utiliza únicamente los conectivos (no funcionalmente completos) . Puede ser axiomatizado por cualquiera de los cálculos antes mencionados 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 por cualquiera de los sistemas de axiomas para el cálculo proposicional positivo y expandiendo 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 se puede axiomatizar sobre el cálculo positivo por 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 ^[13]

${\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 del cálculo proposicional positivo agregando 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 ^[13]

${\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 la lógica intuicionista.

Cálculo equivalente

El cálculo equivalente es el subsistema del cálculo proposicional clásico que solo permite la conectiva de equivalencia (funcionalmente incompleta) , denotada aquí como . La regla de inferencia utilizada en estos sistemas es la siguiente:${\displaystyle \equiv }$

${\displaystyle A,A\equiv B\vdash B}$

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

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

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

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

• Tercera:

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

Sistemas de axiomas de Meredith: ^[16]

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

• Tercera:

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

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

Sistemas de axiomas de Winker : ^[16]

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

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

Ver también

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

Referencias

1. Yasuyuki Imai, Kiyoshi Iséki, Sobre sistemas de axiomas de cálculo proposicional, I, Actas de la Academia Japonesa. Volumen 41, Número 6 (1965), 436–439.
2. Parte XIII: Shôtarô Tanaka. Sobre los sistemas de axiomas de los 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. 31.
4. [Fitelson, 2001] "Nuevas axiomatizaciones elegantes de algunas lógicas oracionales " por Branden Fitelson
5. (El análisis informático de 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 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.
8. , pág. 9, Un espectro de aplicaciones del razonamiento automatizado , Larry Wos; arXiv: cs / 0205078v1
9. Investigaciones sobre el cálculo oracional en lógica, semántica, metamatemática: artículos de 1923 a 1938 por Alfred Tarski , Corcoran, J., ed. Hackett. 1ª edición editada y traducida por JH Woodger, Oxford Uni. Presionar. (1956)
10. Łukasiewicz, J .. (1948). El axioma más corto del cálculo implícito 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
11. A. Chagrov, M. Zakharyaschev, lógica modal , Oxford University Press, 1997.
12. C. Meredith, Un solo axioma de lógica positiva , Journal of Computing Systems, p. 169-170, 1954.
13. L. H. Hackstaff, Sistemas de lógica formal , Springer, 1966.
14. Kiyoshi Iséki, Sobre sistemas de axiomas de cálculos proposicionales, XV, Actas de la Academia de Japón. Volumen 42, Número 3 (1966), 217-220.
15. 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.
16. 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