Liste de systèmes logiques

Cet article contient une liste de systèmes déductifs à la Hilbert pour la logique propositionnelle.

Systèmes de calcul propositionnel classiques

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).

Implication et négation

Les formulations ici utilisent l'implication et la négation $\{\to ,\neg \}$ comme un ensemble fonctionnel complet de connecteurs de base. Chaque système logique nécessite au moins une règle d'inférence non-unaire. Le calcul propositionnel classique utilise généralement la règle du modus ponens:

$A,A\to B\vdash B.$

Nous supposons que cette règle est inclus dans tous les systèmes ci-dessous, sauf indication contraire.

Système d'axiomes de Frege:

$A\to (B\to A)$

$(A\to (B\to C))\to ((A\to B)\to (A\to C))$

$(A\to B)\to (\neg B\to \neg A)$

$\neg \neg A\to A$

$A\to \neg \neg A$

Système d'axiomes de Hilbert:

$A\to (B\to A)$

$(A\to (B\to C))\to (B\to (A\to C))$

$(B\to C)\to ((A\to B)\to (A\to C))$

$A\to (\neg A\to B)$

$(A\to B)\to ((\neg A\to B)\to B)$

Systèmes d'axiomes de Łukasiewicz:

• Premier:

$(A\to B)\to ((B\to C)\to (A\to C))$

$(\neg A\to A)\to A$

$A\to (\neg A\to B)$

• Second:

$((A\to B)\to C)\to (\neg A\to C)$

$((A\to B)\to C)\to (B\to C)$

$(\neg A\to C)\to ((B\to C)\to ((A\to B)\to C))$

• Troisième:

$A\to (B\to A)$

$(A\to (B\to C))\to ((A\to B)\to (A\to C))$

$(\neg A\to \neg B)\to (B\to A)$

• Quatrième:

$(A\to B)\to ((B\to C)\to (A\to C))$

$A\to (\neg A\to B)$

$(\neg A\to B)\to ((B\to A)\to A)$

Système d'axiomes de Łukasiewicz et Tarski:

$[(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)$

Système d'axiomes de Meredith:

$((((A\to B)\to (\neg C\to \neg D))\to C)\to E)\to ((E\to A)\to (D\to A))$

Système d'axiomes de Mendelson:

$A\to (B\to A)$

$(A\to (B\to C))\to ((A\to B)\to (A\to C))$

$(\neg A\to \neg B)\to ((\neg A\to B)\to A)$

Système d'axiomes de Russell:

$A\to (B\to A)$

$(A\to B)\to ((B\to C)\to (A\to C))$

$(A\to (B\to C))\to (B\to (A\to C))$

$\neg \neg A\to A$

$(A\to \neg A)\to \neg A$

$(A\to \neg B)\to (B\to \neg A)$

Systèmes d'axiomes de Sobociński:

• Premier:

$(A\to B)\to (\neg B\to (A\to C))$

$A\to (B\to (C\to A))$

$(\neg A\to B)\to ((A\to B)\to B)$

• Second:

$\neg A\to (A\to B)$

$A\to (B\to (C\to A))$

$(\neg A\to C)\to ((B\to C)\to ((A\to B)\to C))$

Implication et faux

Au lieu de la négation, la logique classique peut également être formulée en utilisant un ensemble fonctionnel complet $\{\to ,\bot \}$ de connecteurs.

Système d'axiomes Tarski–Bernays–Wajsberg:

$(A\to B)\to ((B\to C)\to (A\to C))$

$A\to (B\to A)$

$((A\to B)\to A)\to A$

$\bot \to A$

Système d'axiomes de Church:

$A\to (B\to A)$

$(A\to (B\to C))\to ((A\to B)\to (A\to C))$

$((A\to \bot )\to \bot )\to A$

Systèmes d'axiomes de Meredith:

• Premier:

$((((A\to B)\to (C\to \bot ))\to D)\to E)\to ((E\to A)\to (C\to A))$

• Second:

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

Négation et disjonction

Au lieu de l'implication, la logique classique peut également être formulée en utilisant un ensemble fonctionnel complet $\{\neg ,\lor \}$ de connecteurs. Ces formulations utilisent la règle d'inférence suivante;

$A,\neg A\lor B\vdash B.$

Système d'axiomes Russell–Bernays:

$\neg (\neg B\lor C)\lor (\neg (A\lor B)\lor (A\lor C))$

$\neg (A\lor B)\lor (B\lor A)$

$\neg A\lor (B\lor A)$

$\neg (A\lor A)\lor A$

Système d'axiomes Meredith:

• Premier:

$\neg (\neg (\neg A\lor B)\lor (C\lor (D\lor E)))\lor (\neg (\neg D\lor A)\lor (C\lor (E\lor A)))$

• Second:

$\neg (\neg (\neg A\lor B)\lor (C\lor (D\lor E)))\lor (\neg (\neg E\lor D)\lor (C\lor (A\lor D)))$

Troisième:

$\neg (\neg (\neg A\lor B)\lor (C\lor (D\lor E)))\lor (\neg (\neg C\lor A)\lor (E\lor (D\lor A)))$

La logique propositionnelle classique peut être définie en utilisant uniquement la conjonction et la négation.

Barre de Sheffer

Parce que la barre de Sheffer (également connu sous le nom de l'opérateur NAND) est fonctionnellement complet, il peut être utilisé pour créer une formulation complète de calcul propositionnel. Les formulations NON-ET utilisent une règle d'inférence appelé le modus ponens de Nicod:

$A,A\mid (B\mid C)\vdash C.$

Système d'axiomes de Nicod:

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

Systèmes d'axiomes de Łukasiewicz:

• Premier:

$(A\mid (B\mid C))\mid [(D\mid (D\mid D))\mid ((D\mid B)\mid [(A\mid D)\mid (A\mid D)])]$

• Second:

$(A\mid (B\mid C))\mid [(A\mid (C\mid A))\mid ((D\mid B)\mid [(A\mid D)\mid (A\mid D)])]$

Système d'axiomes  de Wajsberg:

$(A\mid (B\mid C))\mid [((D\mid C)\mid [(A\mid D)\mid (A\mid D)])\mid (A\mid (A\mid B))]$

Systèmes d'axiomes de Argonne:

• Premier:

$(A\mid (B\mid C))\mid [(A\mid (B\mid C))\mid ((D\mid C)\mid [(C\mid D)\mid (A\mid D)])]$

• Second:

$(A\mid (B\mid C))\mid [([(B\mid D)\mid (A\mid D)]\mid (D\mid B))\mid ((C\mid B)\mid A)]$

L'analyse informatique par Argonne a révélé > 60 systèmes à un seul axiome supplémentaires qui peuvent être utilisés pour formuler un calcul propositionnel NON-ET.

Calcul propositionnel implicationnel

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:

$A\to (B\to A)$

$(A\to B)\to ((B\to C)\to (A\to C))$

$((A\to B)\to A)\to A$

Systèmes d'axiomes Łukasiewicz et Tarski:

• Premier:

$[(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:

$[(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:

$((A\to B)\to (C\to D))\to (E\to ((D\to A)\to (C\to A)))$

• Quatrième:

$((A\to B)\to (C\to D))\to ((D\to A)\to (E\to (C\to A)))$

Système d'axiomes Łukasiewicz:

$((A\to B)\to C)\to ((C\to A)\to (D\to A))$

Logiques intuitionnistes et intermédiaires

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

$A\to (B\to A)$

$(A\to (B\to C))\to ((A\to B)\to (A\to C))$

$(A\land B)\to A$

$(A\land B)\to B$

$A\to (B\to (A\land B))$

$A\to (A\lor B)$

$B\to (A\lor B)$

$(A\to C)\to ((B\to C)\to ((A\lor B)\to C))$

$\bot \to A$

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

$(A\to \neg A)\to \neg A$

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

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

$(A\to B)\lor (B\to A).$

Calcul implicationnel positif

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:

$A\to (B\to A)$

$(A\to (B\to C))\to ((A\to B)\to (A\to C))$

Système d'axiomes de Meredith:

• Premier:

$E\to ((A\to B)\to (((D\to A)\to (B\to C))\to (A\to C)))$

• Second:

$A\to (B\to A)$

$(A\to B)\to ((A\to (B\to C))\to (A\to C))$

• Troisième:

$((A\to B)\to C)\to (D\to ((B\to (C\to E))\to (B\to E)))$

Système d'axiomes de Hilbert:

• Premier:

$(A\to (A\to B))\to (A\to B)$

$(B\to C)\to ((A\to B)\to (A\to C))$

$(A\to (B\to C))\to (B\to (A\to C))$

$A\to (B\to A)$

• Second:

$(A\to (A\to B))\to (A\to B)$

$(A\to B)\to ((B\to C)\to (A\to C))$

$A\to (B\to A)$

• Troisième:

$A\to A$

$(A\to B)\to ((B\to C)\to (A\to C))$

$(B\to C)\to ((A\to B)\to (A\to C))$

$(A\to (A\to B))\to (A\to B)$

Calcul propositionnel positif

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

$(A\land B)\to A$

$(A\land B)\to B$

$A\to (B\to (A\land B))$

$A\to (A\lor B)$

$B\to (A\lor B)$

$(A\to C)\to ((B\to C)\to ((A\lor B)\to C))$

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

$(A\leftrightarrow B)\to (A\to B)$

$(A\leftrightarrow B)\to (B\to A)$

$(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é $\bot$, $\{\to ,\land ,\lor ,\neg \}$ par expention du calcul propositionnel positif avec l'axiome

$(A\to \neg B)\to (B\to \neg A)$

ou la pair d'axiomes

$(A\to B)\to (\neg B\to \neg A)$

$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

$(A\to \neg B)\to (B\to \neg A)$

$\neg A\to (A\to B)$

ou la pair d'axiomes

$(A\to \neg A)\to \neg A$

$\neg A\to (A\to B)$

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

$(\neg A\to \neg B)\to (B\to A)$

ou la pair d'axiomes

$(A\to \neg B)\to (B\to \neg A)$

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

$\neg A\to (A\to B)$

$A\leftrightarrow \neg \neg A$

$\neg (A\lor B)\leftrightarrow (\neg A\land \neg B)$

$\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.

Calcul équivalentiel

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

$A,A\equiv B\vdash B$

Système d'axiomes de Iséki:

$((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)$

$(A\equiv (B\equiv C))\equiv ((A\equiv B)\equiv C)$

Système d'axiomes de Iséki–Arai:

$A\equiv A$

$(A\equiv B)\equiv (B\equiv A)$

$(A\equiv B)\equiv ((B\equiv C)\equiv (A\equiv C))$

Systèmes d'axiomes d'Arai:

• Premier:

$(A\equiv (B\equiv C))\equiv ((A\equiv B)\equiv C)$

$((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)$

• Second:

$(A\equiv B)\equiv (B\equiv A)$

$((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)$

Systèmes d'axiomes de Łukasiewicz:

• Premier:

$(A\equiv B)\equiv ((C\equiv B)\equiv (A\equiv C))$

• Second:

$(A\equiv B)\equiv ((A\equiv C)\equiv (C\equiv B))$

• Troisième:

$(A\equiv B)\equiv ((C\equiv A)\equiv (B\equiv C))$

Systèmes d'axiomes de Meredith:

• Premier:

$((A\equiv B)\equiv C)\equiv (B\equiv (C\equiv A))$

• Second:

$A\equiv ((B\equiv (A\equiv C))\equiv (C\equiv B))$

• Troisième:

$(A\equiv (B\equiv C))\equiv (C\equiv (A\equiv B))$

• Quatrième:

$(A\equiv B)\equiv (C\equiv ((B\equiv C)\equiv A))$

• Cinquième:

$(A\equiv B)\equiv (C\equiv ((C\equiv B)\equiv A))$

• Sixième:

$((A\equiv (B\equiv C))\equiv C)\equiv (B\equiv A)$

• Septième:

$((A\equiv (B\equiv C))\equiv B)\equiv (C\equiv A)$

Système d'axiomes de Kalman:

$A\equiv ((B\equiv (C\equiv A))\equiv (C\equiv B))$

Systèmes d'axiomes de Winker:

• Premier:

$A\equiv ((B\equiv C)\equiv ((A\equiv C)\equiv B))$

• Second:

$A\equiv ((B\equiv C)\equiv ((C\equiv A)\equiv B))$

Système d'axiomes de XCB:

$A\equiv (((A\equiv B)\equiv (C\equiv B))\equiv C)$

Références

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « List of logic systems » (voir la liste des auteurs).