Articulo de referencia

Lista de sistemas axiomáticos en lógica

Este artículo contiene una lista de ejemplos de sistemas deductivos al estilo de Hilbert para lógicas proposicionales . Sistemas de cálculo proposicional clásico El cálculo prop...

Este artículo contiene una lista de ejemplos de sistemas deductivos al estilo de Hilbert para lógicas proposicionales .

Sistemas de cálculo proposicional clásico

El cálculo proposicional clásico es la lógica proposicional estándar. Su semántica es bivalente y su propiedad principal es la fuerte completitud ; es decir, siempre que una fórmula se deduce semánticamente de un conjunto de premisas, también se deduce sintácticamente de dicho conjunto. Se han formulado numerosos sistemas de axiomas completos equivalentes. Estos difieren en la elección de los conectores básicos utilizados, que en todos los casos deben 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 conectores elegida.

Implicación y negación

Las formulaciones aquí empleadas utilizan implicación y negación.{,¬}{\displaystyle \{\to ,\neg \}}como un conjunto funcionalmente completo de conectores 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 :

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

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

Sistema axiomático de Frege : [ 1 ]

A(BA){\displaystyle A\to (B\to A)}
(A(Bdo))((AB)(Ado)){\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}
(A(Bdo))(B(Ado)){\displaystyle (A\to (B\to C))\to (B\to (A\to C))}
(AB)(¬B¬A){\displaystyle (A\to B)\to (\neg B\to \neg A)}
¬¬AA{\displaystyle \neg \neg A\to A}
A¬¬A{\displaystyle A\to \neg \neg A}

Sistema de axiomas de Hilbert : [ 1 ]

A(BA){\displaystyle A\to (B\to A)}
(A(Bdo))(B(Ado)){\displaystyle (A\to (B\to C))\to (B\to (A\to C))}
(Bdo)((AB)(Ado)){\displaystyle (B\to C)\to ((A\to B)\to (A\to C))}
A(¬AB){\displaystyle A\to (\neg A\to B)}
(AB)((¬AB)B){\displaystyle (A\to B)\to ((\neg A\to B)\to B)}

Sistemas de axiomas de Łukasiewicz : [ 1 ]

  • Primero:
    (AB)((Bdo)(Ado)){\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}
    (¬AA)A{\displaystyle (\neg A\to A)\to A}
    A(¬AB){\displaystyle A\to (\neg A\to B)}
  • Segundo:
    ((AB)do)(¬Ado){\displaystyle ((A\to B)\to C)\to (\neg A\to C)}
    ((AB)do)(Bdo){\displaystyle ((A\to B)\to C)\to (B\to C)}
    (¬Ado)((Bdo)((AB)do)){\displaystyle (\neg A\to C)\to ((B\to C)\to ((A\to B)\to C))}
  • Tercero:
    A(BA){\displaystyle A\to (B\to A)}
    (A(Bdo))((AB)(Ado)){\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}
    (¬A¬B)(BA){\displaystyle (\neg A\to \neg B)\to (B\to A)}

Sistema axiomático de Arai : [ 2 ]

(AB)((Bdo)(Ado)){\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}
A(¬AB){\displaystyle A\to (\neg A\to B)}
(¬AB)((BA)A){\displaystyle (\neg A\to B)\to ((B\to A)\to A)}

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

[(A(BA))([(¬do(D¬mi))[(do(DF))((miD)(miF))]]GRAMO)](HGRAMO){\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 :

((((AB)(¬do¬D))do)mi)((miA)(DA)){\displaystyle ((((A\to B)\to (\neg C\to \neg D))\to C)\to E)\to ((E\to A)\to (D\to A))}

Sistema axiomático de Mendelson : [ 4 ]

A(BA){\displaystyle A\to (B\to A)}
(A(Bdo))((AB)(Ado)){\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}
(¬A¬B)((¬AB)A){\displaystyle (\neg A\to \neg B)\to ((\neg A\to B)\to A)}

Sistema axiomático de Russell : [ 1 ]

A(BA){\displaystyle A\to (B\to A)}
(AB)((Bdo)(Ado)){\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}
(A(Bdo))(B(Ado)){\displaystyle (A\to (B\to C))\to (B\to (A\to C))}
¬¬AA{\displaystyle \neg \neg A\to A}
(A¬A)¬A{\displaystyle (A\to \neg A)\to \neg A}
(A¬B)(B¬A){\displaystyle (A\to \neg B)\to (B\to \neg A)}

Sistemas axiomáticos de Sobociński : [ 1 ]

  • Primero:
    ¬A(AB){\displaystyle \neg A\to (A\to B)}
    A(B(doA)){\displaystyle A\to (B\to (C\to A))}
    (¬Ado)((Bdo)((AB)do)){\displaystyle (\neg A\to C)\to ((B\to C)\to ((A\to B)\to C))}
  • Segundo:
    (AB)(¬B(Ado)){\displaystyle (A\to B)\to (\neg B\to (A\to C))}
    A(B(doA)){\displaystyle A\to (B\to (C\to A))}
    (¬AB)((AB)B){\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.{,}{\displaystyle \{\to,\bot \}}de conectores.

Sistema de axiomas de Tarski- Bernays - Wajsberg :

(AB)((Bdo)(Ado)){\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}
A(BA){\displaystyle A\to (B\to A)}
((AB)A)A{\displaystyle ((A\to B)\to A)\to A}. [ 5 ]
A{\displaystyle \bot \to A}

El sistema de axiomas de Church :

A(BA){\displaystyle A\to (B\to A)}
(A(Bdo))((AB)(Ado)){\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}
((A))A{\displaystyle ((A\to \bot )\to \bot )\to A}

Sistemas axiomáticos de Meredith:

  • Primero: [ 6 ] [ 7 ] [ 8 ]
    ((((AB)(do))D)mi)((miA)(doA)){\displaystyle ((((A\to B)\to (C\to \bot ))\to D)\to E)\to ((E\to A)\to (C\to A))}
  • Segundo: [ 6 ]
    ((AB)((do)D))((DA)(mi(FA))){\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 implicación, la lógica clásica también puede formularse utilizando el conjunto funcionalmente completo.{¬,}{\displaystyle \{\neg ,\lor \}}de conectores. Estas formulaciones utilizan la siguiente regla de inferencia;

A,¬ABB.{\displaystyle {\frac {A,\neg A\lor B}{B}}.}

Sistema axiomático de Russell-Bernay:

¬(¬Bdo)(¬(AB)(Ado)){\displaystyle \neg (\neg B\lor C)\lor (\neg (A\lor B)\lor (A\lor C))}
¬(AB)(BA){\displaystyle \neg (A\lor B)\lor (B\lor A)}
¬A(BA){\displaystyle \neg A\lor (B\lor A)}
¬(AA)A{\displaystyle \neg (A\lor A)\lor A}

Sistemas axiomáticos de Meredith: [ 9 ]

  • Primero:
    ¬(¬(¬AB)(do(Dmi)))(¬(¬DA)(do(miA))){\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:
    ¬(¬(¬AB)(do(Dmi)))(¬(¬miD)(do(AD))){\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:
    ¬(¬(¬AB)(do(Dmi)))(¬(¬doA)(mi(DA))){\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 igual modo, 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.{,¬}{\displaystyle \{\wedge ,\neg \}}, con el modus ponens como regla de inferencia. En su libro, [ 10 ] utilizó la implicación para presentar sus esquemas axiomáticos.doD{\displaystyle C\rightarrow D}" es una abreviatura de "¬(do¬D){\displaystyle \neg (C\wedge \neg D)}":

  • AAA{\displaystyle A\rightarrow A\wedge A}
  • ABA{\displaystyle A\wedge B\rightarrow A}
  • (AB)(¬(Bdo)¬(doA)){\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 de la siguiente forma:

  • ¬(A¬(AA)){\displaystyle \neg (A\wedge \neg (A\wedge A))}
  • ¬((AB)¬A){\displaystyle \neg ((A\wedge B)\wedge \neg A)}
  • ¬(¬(A¬B)¬¬(¬(Bdo)¬¬(doA))){\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:

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

El derrame cerebral de Sheffer

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

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

Sistema axiomático de Nicod: [ 6 ]

(A(Bdo))[(mi(mimi))((DB)[(AD)(AD)])]{\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: [ 6 ]

  • Primero:
    (A(Bdo))[(D(DD))((DB)[(AD)(AD)])]{\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:
    (A(Bdo))[(A(doA))((DB)[(AD)(AD)])]{\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 axiomático de Wajsberg: [ 6 ]

(A(Bdo))[((Ddo)[(AD)(AD)])(A(AB))]{\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 axiomáticos de Argonne : [ 6 ]

  • Primero:
(A(Bdo))[(A(Bdo))((Ddo)[(doD)(AD)])]{\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:
(A(Bdo))[([(BD)(AD)](DB))((doB)A)]{\displaystyle (A\mid (B\mid C))\mid [([(B\mid D)\mid (A\mid D)]\mid (D\mid B))\mid ((C\mid B)\mid A)]}[ 11 ]

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. [ 8 ]

cálculo proposicional implicacional

El cálculo proposicional implicacional es el fragmento del cálculo proposicional clásico que solo admite el conector de implicación. No es funcionalmente completo (porque carece de la capacidad de expresar falsedad y negación), pero sí es 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: [ 12 ]

A(BA){\displaystyle A\to (B\to A)}
(AB)((Bdo)(Ado)){\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}
((AB)A)A{\displaystyle ((A\to B)\to A)\to A}

Sistemas de axiomas de Łukasiewicz y Tarski:

  • Primero: [ 12 ]
    [(A(BA))[([((doD)mi)F][(DF)(doF)])GRAMO]]GRAMO{\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: [ 12 ]
    [(AB)((doD)mi)]([F((doD)mi)][(AF)(Dmi)]){\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:
    ((AB)(doD))(mi((DA)(doA))){\displaystyle ((A\to B)\to (C\to D))\to (E\to ((D\to A)\to (C\to A)))}
  • Cuatro:
    ((AB)(doD))((DA)(mi(doA))){\displaystyle ((A\to B)\to (C\to D))\to ((D\to A)\to (E\to (C\to A)))}

Sistema de axiomas de Łukasiewicz: [ 13 ] [ 12 ]

((AB)do)((doA)(DA)){\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. Se formula comúnmente con{,,,}{\displaystyle \{\to ,\land ,\lor ,\bot \}}como el conjunto de conectores básicos (funcionalmente completos). No es sintácticamente completo ya que carece del tercero excluido A∨¬A o de la ley de Peirce ((A→B)→A)→A, que se pueden añadir sin que la lógica sea inconsistente. Tiene el modus ponens como regla de inferencia y los siguientes axiomas:

A(BA){\displaystyle A\to (B\to A)}
(A(Bdo))((AB)(Ado)){\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}
(AB)A{\displaystyle (A\land B)\to A}
(AB)B{\displaystyle (A\land B)\to B}
A(B(AB)){\displaystyle A\to (B\to (A\land B))}
A(AB){\displaystyle A\to (A\lor B)}
B(AB){\displaystyle B\to (A\lor B)}
(Ado)((Bdo)((AB)do)){\displaystyle (A\to C)\to ((B\to C)\to ((A\lor B)\to C))}
A{\displaystyle \bot \to A}

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

(A¬A)¬A{\displaystyle (A\to \neg A)\to \neg A}
¬A(AB){\displaystyle \neg A\to (A\to B)}

Las lógicas intermedias se sitúan 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 ser axiomatizada por el sistema de axiomas intuicionista más el axioma [ 14 ].
¬A¬¬A.{\displaystyle \neg A\lor \neg \neg A.}
  • La lógica de Gödel-Dummett (LC) puede axiomatizarse sobre la lógica intuicionista añadiendo el axioma [ 14 ].
(AB)(BA).{\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 que se muestran a continuación utilizan el modus ponens como regla de inferencia.

El sistema axiomático de Łukasiewicz:

A(BA){\displaystyle A\to (B\to A)}
(A(Bdo))((AB)(Ado)){\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}

Sistemas axiomáticos de Meredith:

  • Primero:
    mi((AB)(((DA)(Bdo))(Ado))){\displaystyle E\to ((A\to B)\to (((D\to A)\to (B\to C))\to (A\to C)))}
  • Segundo:
    A(BA){\displaystyle A\to (B\to A)}
    (AB)((A(Bdo))(Ado)){\displaystyle (A\to B)\to ((A\to (B\to C))\to (A\to C))}
  • Tercero:
    ((AB)do)(D((B(domi))(Bmi))){\displaystyle ((A\to B)\to C)\to (D\to ((B\to (C\to E))\to (B\to E)))}[ 15 ]

Sistemas axiomáticos de Hilbert:

  • Primero:
    (A(AB))(AB){\displaystyle (A\to (A\to B))\to (A\to B)}
    (Bdo)((AB)(Ado)){\displaystyle (B\to C)\to ((A\to B)\to (A\to C))}
    (A(Bdo))(B(Ado)){\displaystyle (A\to (B\to C))\to (B\to (A\to C))}
    A(BA){\displaystyle A\to (B\to A)}
  • Segundo:
    (A(AB))(AB){\displaystyle (A\to (A\to B))\to (A\to B)}
    (AB)((Bdo)(Ado)){\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}
    A(BA){\displaystyle A\to (B\to A)}
  • Tercero:
    AA{\displaystyle A\to A}
    (AB)((Bdo)(Ado)){\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}
    (Bdo)((AB)(Ado)){\displaystyle (B\to C)\to ((A\to B)\to (A\to C))}
    (A(AB))(AB){\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 conectores (no funcionalmente completos).{,,}{\displaystyle \{\to ,\land ,\lor \}}. Puede ser axiomatizado por cualquiera de los cálculos mencionados anteriormente para el cálculo implicacional positivo junto con los axiomas

(AB)A{\displaystyle (A\land B)\to A}
(AB)B{\displaystyle (A\land B)\to B}
A(B(AB)){\displaystyle A\to (B\to (A\land B))}
A(AB){\displaystyle A\to (A\lor B)}
B(AB){\displaystyle B\to (A\lor B)}
(Ado)((Bdo)((AB)do)){\displaystyle (A\to C)\to ((B\to C)\to ((A\lor B)\to C))}

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

(AB)(AB){\displaystyle (A\leftrightarrow B)\to (A\to B)}
(AB)(BA){\displaystyle (A\leftrightarrow B)\to (B\to A)}
(AB)((BA)(AB)){\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 axiomáticos para el cálculo proposicional positivo y expandiendo su lenguaje con el conector nulo.{\displaystyle \bot }, sin esquemas axiomáticos adicionales. Alternativamente, también puede axiomatizarse en el lenguaje.{,,,¬}{\displaystyle \{\to ,\land ,\lor ,\neg \}}al expandir el cálculo proposicional positivo con el axioma

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

o el par de axiomas

(AB)(¬B¬A){\displaystyle (A\to B)\to (\neg B\to \neg A)}
A¬¬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

(A¬B)(B¬A){\displaystyle (A\to \neg B)\to (B\to \neg A)}
¬A(AB){\displaystyle \neg A\to (A\to B)}

o el par de axiomas [ 16 ]

(A¬A)¬A{\displaystyle (A\to \neg A)\to \neg A}
¬A(AB){\displaystyle \neg A\to (A\to B)}

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

(¬A¬B)(BA){\displaystyle (\neg A\to \neg B)\to (B\to A)}

o el par de axiomas

(A¬B)(B¬A){\displaystyle (A\to \neg B)\to (B\to \neg A)}
¬¬AA{\displaystyle \neg \neg A\to A}

El cálculo de Fitch toma cualquiera de los sistemas axiomáticos para el cálculo proposicional positivo y agrega los axiomas [ 16 ].

¬A(AB){\displaystyle \neg A\to (A\to B)}
A¬¬A{\displaystyle A\leftrightarrow \neg \neg A}
¬(AB)(¬A¬B){\displaystyle \neg (A\lor B)\leftrightarrow (\neg A\land \neg B)}
¬(AB)(¬A¬B){\displaystyle \neg (A\land B)\leftrightarrow (\neg A\lor \neg B)}

Cabe señalar que el primer y el tercer axioma también son válidos en la lógica intuicionista.

Cálculo de equivalencia

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

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

Sistema axiomático de Iséki: [ 17 ]

((Ado)(BA))(doB){\displaystyle ((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)}
(A(Bdo))((AB)do){\displaystyle (A\equiv (B\equiv C))\equiv ((A\equiv B)\equiv C)}

Sistema de axiomas de Iséki-Arai: [ 18 ]

AA{\displaystyle A\equiv A}
(AB)(BA){\displaystyle (A\equiv B)\equiv (B\equiv A)}
(AB)((Bdo)(Ado)){\displaystyle (A\equiv B)\equiv ((B\equiv C)\equiv (A\equiv C))}

Los sistemas axiomáticos de Arai;

  • Primero:
    (A(Bdo))((AB)do){\displaystyle (A\equiv (B\equiv C))\equiv ((A\equiv B)\equiv C)}
    ((Ado)(BA))(doB){\displaystyle ((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)}
  • Segundo:
    (AB)(BA){\displaystyle (A\equiv B)\equiv (B\equiv A)}
    ((Ado)(BA))(doB){\displaystyle ((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)}

Sistemas de axiomas de Łukasiewicz: [ 19 ]

  • Primero:
    (AB)((doB)(Ado)){\displaystyle (A\equiv B)\equiv ((C\equiv B)\equiv (A\equiv C))}
  • Segundo:
    (AB)((Ado)(doB)){\displaystyle (A\equiv B)\equiv ((A\equiv C)\equiv (C\equiv B))}
  • Tercero:
    (AB)((doA)(Bdo)){\displaystyle (A\equiv B)\equiv ((C\equiv A)\equiv (B\equiv C))}

Sistemas axiomáticos de Meredith: [ 19 ]

  • Primero:
    ((AB)do)(B(doA)){\displaystyle ((A\equiv B)\equiv C)\equiv (B\equiv (C\equiv A))}
  • Segundo:
    A((B(Ado))(doB)){\displaystyle A\equiv ((B\equiv (A\equiv C))\equiv (C\equiv B))}
  • Tercero:
    (A(Bdo))(do(AB)){\displaystyle (A\equiv (B\equiv C))\equiv (C\equiv (A\equiv B))}
  • Cuatro:
    (AB)(do((Bdo)A)){\displaystyle (A\equiv B)\equiv (C\equiv ((B\equiv C)\equiv A))}
  • Quinto:
    (AB)(do((doB)A)){\displaystyle (A\equiv B)\equiv (C\equiv ((C\equiv B)\equiv A))}
  • Sexto:
    ((A(Bdo))do)(BA){\displaystyle ((A\equiv (B\equiv C))\equiv C)\equiv (B\equiv A)}
  • Séptimo:
    ((A(Bdo))B)(doA){\displaystyle ((A\equiv (B\equiv C))\equiv B)\equiv (C\equiv A)}

Sistema axiomático de Kalman : [ 19 ]

A((B(doA))(doB)){\displaystyle A\equiv ((B\equiv (C\equiv A))\equiv (C\equiv B))}

Sistemas de axiomas de Winker : [ 19 ]

  • Primero:
    A((Bdo)((Ado)B)){\displaystyle A\equiv ((B\equiv C)\equiv ((A\equiv C)\equiv B))}
  • Segundo:
    A((Bdo)((doA)B)){\displaystyle A\equiv ((B\equiv C)\equiv ((C\equiv A)\equiv B))}

Sistema axiomático XCB: [ 19 ]

A(((AB)(doB))do){\displaystyle A\equiv (((A\equiv B)\equiv (C\equiv B))\equiv C)}

Véase también

Referencias

  1. 1 2 3 4 5 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. Ley de Peirce
  6. 1 2 3 4 5 6 [Fitelson, 2001] "Nuevas y elegantes axiomatizaciones de algunas lógicas sentenciales" por Branden Fitelson
  7. (El análisis informático realizado por Argonne ha revelado que este es el axioma individual más corto con el menor número de variables para el cálculo proposicional).
  8. 1 2 "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
  9. C. Meredith, Axiomas únicos para los sistemas (C, N), (C, 0) y (A, N) del cálculo proposicional bivaluado , Journal of Computing Systems, págs. 155–164, 1954.
  10. Rosser J. Barkley, "Lógica para matemáticos", Nueva York, McGraw-Hill, 1953.
  11. , pág. 9, Un espectro de aplicaciones del razonamiento automatizado , Larry Wos; arXiv:cs/0205078v1
  12. 1 2 3 4 Investigaciones sobre el cálculo proposicional en lógica, semántica y metamatemáticas: Artículos de 1923 a 1938 de Alfred Tarski , editado por J. Corcoran y Hackett. 1.ª edición editada y traducida por J.H. Woodger, Oxford University Press. (1956)
  13. Łukasiewicz, Jan (1948). "El axioma más breve del cálculo implicacional de proposiciones" . Actas de la Real Academia Irlandesa. Sección A: Ciencias Matemáticas y Físicas . 52 : 25–33 . ISSN 0035-8975 . JSTOR 20488489 .  
  14. 1 2 A. Chagrov, M. Zakharyaschev, Lógica modal , Oxford University Press, 1997.
  15. C. Meredith, Un axioma único de la lógica positiva , Journal of Computing Systems, págs. 169-170, 1954.
  16. 1 2 L. H. Hackstaff, Sistemas de lógica formal , Springer, 1966.
  17. 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.
  18. Yoshinari Arai, Sobre sistemas axiomáticos de cálculos proposicionales, XVII, Actas de la Academia Japonesa. Volumen 42, Número 4 (1966), 351 354.
  19. 1 2 3 4 5 XCB, el último de los axiomas individuales más cortos para el cálculo de equivalencia clásico , LARRY WOS, DOLPH ULRICH, BRANDEN FITELSON; arXiv:cs/0211015v1