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.

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