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  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 :

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

Système d'axiomes de FregeYasuyuki Imai, Kiyoshi Iséki, On axiom systems of propositional calculi, I, Proceedings of the Japan Academy. :

Système d'axiomes de Hilbert :

Systèmes d'axiomes de Łukasiewicz : Premier :

Second :

Troisième :

Quatrième :

Système d'axiomes de Łukasiewicz et TarskiPart XIII: Shôtarô Tanaka. :

Système d'axiomes de Meredith :

Système d'axiomes de MendelsonElliott Mendelson, Introduction to Mathematical Logic, Van Nostrand, New York, 1979, . :

Système d'axiomes de Russell :

Systèmes d'axiomes de Sobociński : Premier :

Second :

Implication et faux Au lieu de la négation, la logique classique peut également être formulée en utilisant un ensemble fonctionnel complet  de connecteurs.

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

Système d'axiomes de Church :

Systèmes d'axiomes de Meredith : Premier[Fitelson, 2001] "New Elegant Axiomatizations of Some Sentential Logics" par Branden Fitelson(L'analyse informatique d'Argonne a révélé que c'est l'axiome seul le plus court avec le moins variables pour le calcul propositionnel)."Some New Results in Logical Calculi Obtained Using Automated Reasoning", Zac Ernst, Ken Harris, & Branden Fitelson, http://www.mcs.anl.gov/research/projects/AR/award-2001/fitelson.pdf :

Second :

Négation et disjonction Au lieu de l'implication, la logique classique peut également être formulée en utilisant un ensemble fonctionnel complet de connecteurs. Ces formulations utilisent la règle d'inférence suivante;

Système d'axiomes Russell–Bernays :

Système d'axiomes MeredithC. Meredith, Single axioms for the systems (C, N), (C, 0) and (A, N) of the two-valued propositional calculus, Journal of Computing Systems, , 1954. : Premier :

Second :

Troisième :

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 :

Système d'axiomes de Nicod :

Systèmes d'axiomes de Łukasiewicz : Premier :

Second :

Système d'axiomes de Wajsberg :

Systèmes d'axiomes de Argonne : Premier :

Second : , , A Spectrum of Applications of Automated Reasoning, Larry Wos; arXiv:cs/0205078v1 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–TarskiInvestigations into the Sentential Calculus in Logic, Semantics, Metamathematics: Papers from 1923 to 1938 by Alfred Tarski, Corcoran, J., ed. :

Systèmes d'axiomes Łukasiewicz et Tarski : Premier :

Second :

Troisième :

Quatrième :

Système d'axiomes ŁukasiewiczŁukasiewicz, J.. (1948). :

Logiques intuitionnistes et intermédiaires 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 :

Sinon, la logique intuitionniste peut être axiomatisé en utilisantcomme l'ensemble des conjonctions de base, en remplaçant le dernier axiome

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'axiomeA. Chagrov, M. Zakharyaschev, Modal logic, Oxford University Press, 1997.

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

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 :

Système d'axiomes de Meredith : Premier :

Second :

Troisième : C. Meredith, A single axiom of positive logic, Journal of Computing Systems, , 1954. Système d'axiomes de Hilbert : Premier :

Second :

Troisième :

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

On peut également inclure le connecteur  et les axiomes

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é ,  par expention du calcul propositionnel positif avec l'axiome

ou la paire d'axiomes

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

ou la paire d'axiomesL. H. Hackstaff, Systems of Formal Logic, Springer, 1966.

La logique classique dans la langue  peut être obtenue du calcul propositionnel positif en ajoutant l'axiome

ou la paire d'axiomes

Le calcul de Fitch calcul prend l'un des systèmes d'axiomes pour le calcul propositionnel positif et ajoute les axiomes

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é . La règle d'inférence utilisée dans ces systèmes est la suivante :

Système d'axiomes de IsékiKiyoshi Iséki, On axiom systems of propositional calculi, XV, Proceedings of the Japan Academy. :

Système d'axiomes de Iséki–AraiYoshinari Arai, On axiom systems of propositional calculi, XVII, Proceedings of the Japan Academy. :

Systèmes d'axiomes d'Arai : Premier :

Second :

Systèmes d'axiomes de ŁukasiewiczXCB, the Last of the Shortest Single Axioms for the Classical Equivalential Calculus, LARRY WOS, DOLPH ULRICH, BRANDEN FITELSON; : Premier :

Second :

Troisième :

Systèmes d'axiomes de Meredith : Premier :

Second :

Troisième :

Quatrième :

Cinquième :

Sixième :

Septième :

Système d'axiomes de Kalman :

Systèmes d'axiomes de Winker : Premier :

Second :

Système d'axiomes de XCB :

Références

Catégorie:Logique mathématique Catégorie:Logique propositionnelle