Liste de systèmes logiques

Cet article contient une liste de systèmes déductifs à la Hilbert pour la logique propositionnelle. 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). 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 Frege: 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 Tarski: Système d'axiomes de Meredith: Système d'axiomes de Mendelson: Système d'axiomes de Russell: Systèmes d'axiomes de Sobociński: Premier: Second: 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: Second: 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 Meredith: Premier: Second: Troisième: La logique propositionnelle classique peut être définie en utilisant uniquement la conjonction et la négation. 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.