Liste de systèmes logiques

Le calcul propositionnel classique, aussi appelé logique propositionnelle standard a une sémantique est bivalente, et possède une propriété principale selon laquelle celle-ci est syntaxiquement complète. De nombreux systèmes d'axiomes équivalents complets ont été formulés. Ils diffèrent dans le choix des connecteurs de base utilisé, qui dans tous les cas doivent être fonctionnellement complets (à savoir, capable d'exprimer la composition de toutes les tables de vérité n-aire).

Le calcul propositionnel implicationnel est le fragment du calcul propositionnel classique qui n'admet que le connecteur de l'implication. Il n'est pas fonctionnellement complet (car il n'a pas la capacité d'exprimer la fausseté et la négation), mais il est cependant syntaxiquement complet. Le calcul implicationnel ci-dessous utilisent le modus ponens comme règle d'inférence.

Système d'axiomes 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}$

Systèmes d'axiomes Łukasiewicz et Tarski:

• Premier[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}$

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

• Troisième:

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

• Quatrième:

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

Système d'axiomes Łukasiewicz[10] - [9]:

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

${\displaystyle \{\to ,\land ,\lor ,\bot \}}$ comme l'ensemble (fonctionnellement complet) des conjonctions de base. Celui-ci n'est pas syntaxiquement complet car il lui manque le tiers exclu A∨¬A ou la loi de Peirce ((A→B)→A)→A, qui peut être ajouté sans rendre la logique incohérente. Il possède modus ponens comme règle d'inférence, et les axiomes suivants:

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

Sinon, la logique intuitionniste peut être axiomatisé en utilisant${\displaystyle \{\to ,\land ,\lor ,\neg \}}$comme l'ensemble des conjonctions de base, en remplaçant le dernier axiome

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

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

Les logiques intermédiaires se situent entre la logique intuitionniste et la logique classique. Voici quelques logiques intermédiaires:

• La logique de Jankov (KC) est une extension de la logique intuitionniste, qui peut être axiomatisée par le système d'axiomes intuitionniste plus l'axiome[11]

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

• La logique de Gödel–Dummett (LC) peut être axiomatisée sur la logique intuitionniste en ajoutant l'axiome[11]

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

Le calcul implicationnel positif est le fragment implicationnel de la logique intuitionniste. Les systèmes ci-dessous utilisent le modus ponens comme règle d'inférence.

Système d'axiomes de Łukasiewicz:

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

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

Système d'axiomes de Meredith:

• Premier:

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

• Second:

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

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

• Troisième:

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

Système d'axiomes de Hilbert:

• Premier:

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

• Second:

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

• Troisième:

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

Le calcul propositionnel positif est le fragment de la logique intuitionniste en utilisant uniquement les connecteurs (non fonctionnellement complets) ${\displaystyle \{\to ,\land ,\lor \}}$. Il peut être axiomatisé par aucun des calculs mentionnés ci-dessus, pour le calcul implicationnel positif:

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

On peut également inclure le connecteur ${\displaystyle \leftrightarrow }$ et les axiomes

${\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 logique minimale de Johansson peut être axiomatisée par l'un des systèmes d'axiome pour le calcul propositionnel positif et l'élargir avec le connecteur d'arité ${\displaystyle \bot }$, ${\displaystyle \{\to ,\land ,\lor ,\neg \}}$ par expention du calcul propositionnel positif avec l'axiome

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

ou la pair d'axiomes

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

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

La logique intuitionniste avec la négation peut être axiomatisée sur le calcul positif par la paire d'axiomes

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

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

ou la pair d'axiomes[13]

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

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

La logique classique dans la langue ${\displaystyle \{\to ,\land ,\lor ,\neg \}}$ peut être obtenue du calcul propositionnel positif en ajoutant l'axiome

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

ou la pair d'axiomes

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

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

Le calcul de Fitch calcul prend l'un des systèmes d'axiomes pour le calcul propositionnel positif et ajoute les axiomes[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)}$

On notera que le premier et le troisième axiomes sont également valables en logique intuitionniste.

Le calcul équivalentiel est le sous-système du calcul propositionnel classique qui ne permet (fonctionnellement incomplet) pas l'équivalence, noté ${\displaystyle \equiv }$. La règle d'inférence utilisée dans ces systèmes est la suivante:

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

Système d'axiomes 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)}$

Système d'axiomes 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))}$

Systèmes d'axiomes d'Arai:

• Premier:

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

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

• Second:

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

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

Systèmes d'axiomes de Łukasiewicz[16]:

• Premier:

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

• Second:

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

• Troisième:

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

Systèmes d'axiomes de Meredith[16]:

• Premier:

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

• Second:

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

• Troisième:

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

• Quatrième:

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

• Cinquième:

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

• Sixième:

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

• Septième:

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

Système d'axiomes de Kalman[16]:

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

Systèmes d'axiomes de Winker[16]:

• Premier:

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

• Second:

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

Système d'axiomes de XCB[16]:

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