calcul des propositions

Partie fondamentale de la logique, qui consiste à opérer des calculs sur des propositions à l'aide de règles d'inférence ne faisant pas intervenir de quantificateur.

LOGIQUE

Le calcul des propositions est considéré comme la version moderne de la logique des stoïciens. La première formalisation en a été donnée par Frege en 1879, au moyen des axiomes suivants :
P1 : p → (q → p)
P2 : (s → (p → q)) → ((s → p) → (s → q))
P3 : (p → (q → r)) → (q → (p → r))
P4 : (p → q) → (¬ q → ¬ p)
P5 : ¬ ¬ p → p (tiers exclu)
P6 : p → ¬ ¬ p (tiers exclu).