Propositional logic
Propositional logic deals with propositions, the kind of statement that can be true or false. "If it's raining, then it's cloudy. It's raining. Therefore, it's cloudy." That short chain has a name in this branch of logic. It is called modus ponens, and it is one of the classically valid forms. Strip away what raining and clouds actually mean, replace them with the letters P and Q, and the reasoning still holds. That stubborn validity, independent of subject matter, is what this field studies.
The subject goes by many names. Some call it statement logic, others sentential calculus, propositional calculus, sentential logic, or zeroth-order logic. Occasionally it is labeled first-order propositional logic to set it apart from System F, though it must not be confused with first-order logic. Behind the tangle of names sits one branch of classical logic with a narrow, powerful focus. Who first built it into a system? Why did its symbols multiply into rival notations? And how can a logic so simple still drive algorithms running today? Those questions wait ahead.
In the 3rd century BC, Chrysippus is often credited with developing a deductive system for propositional logic as his main achievement, work later expanded by his successor Stoics. His logic focused on propositions. That set it apart from traditional syllogistic logic, which focused on terms. The difference was foundational, a choice about what reasoning is even made of.
Most of those original writings were lost. Somewhere between the 3rd and 6th century CE, Stoic logic faded into oblivion. It would not return until the 20th century, resurrected in the wake of the rediscovery of propositional logic itself. For more than a thousand years, a working theory of inference simply vanished from view.
Gottfried Leibniz, the 17th-18th-century mathematician, first developed symbolic logic, the tool that would later refine the field. His calculus ratiocinator stayed unknown to the larger logical community. Because of that obscurity, many of his advances were recreated from scratch. George Boole and Augustus De Morgan arrived at them completely independent of Leibniz.
Gottlob Frege's predicate logic builds on propositional logic. It has been described as combining "the distinctive features of syllogistic logic and propositional logic." That fusion opened a new era. Yet propositional logic kept advancing after Frege, gaining natural deduction, truth trees, and truth tables. Natural deduction was invented by Gerhard Gentzen and Stanisław Jaśkowski, and truth trees by Evert Willem Beth. The truth table, by contrast, has a far murkier origin.
Ludwig Wittgenstein or Emil Post, or both independently, are generally credited with the actual tabular structure of the truth table, its formatting as a grid. The ideas behind it run deeper still. Within the works of Frege and Bertrand Russell sit notions influential to its invention. Besides those two, others credited with preceding ideas include Philo, Boole, Charles Sanders Peirce, and Ernst Schröder.
The roster of contributors keeps growing once you ask who shaped the table's grid form. Jan Łukasiewicz, Alfred North Whitehead, William Stanley Jevons, John Venn, and Clarence Irving Lewis all appear among those credited with the tabular structure. So many names attach to one small invention that assigning a single inventor becomes impossible.
John Shosky reached exactly that conclusion. "It is far from clear," he wrote, "that any one person should be given the title of 'inventor' of truth-tables." The tool is now central to the field, yet it belongs to no one. That ambiguity sits oddly beside the precision the table itself delivers.
"London is the capital of England" is the kind of sentence this logic accepts. It is a declarative sentence with a truth value, what the field calls a statement. Questions like "What is Wikipedia?" do not qualify. Imperatives such as "Please add citations to support the claims in this article" do not either. Those non-declarative sentences carry no truth value, and only nonclassical fields, called erotetic and imperative logics, handle them.
Logical connectives are the words that bolt simple statements together. In English they are "and" for conjunction, "or" for disjunction, "not" for negation, "if" for the material conditional, and "if and only if" for the biconditional. A sentence with no connectives is simple, or atomic. One built with connectives is compound, or molecular.
Sentential connectives form a broader category than logical ones. A sentential connective is any linguistic particle that binds sentences into a new compound, or inflects a single sentence into a new one. A logical connective is the special kind whose output is still a proposition whenever its inputs are propositions. Philosophers disagree about what exactly a proposition is. They also disagree about which natural-language connectives should count as logical at all. Sentential connectives are also called sentence-functors, and logical connectives are also called truth-functors, terms that hint at the truth-value machinery underneath.
Propositional variables, the letters that stand in for whole statements, are the starting atoms of the formal language. Because the field ignores any structure inside a statement, it replaces indivisible statements with letters of the alphabet. When P means "It's raining" and Q means "it's cloudy," the symbolic premises correspond exactly with the natural-language argument, and with any other inference of the same form.
Three definitions build every formula by recursion. Atomic propositional variables are formulas. Applying a connective to a sequence of formulas yields a formula. And, by the closure clause, nothing else is a formula. That final rule excludes infinitely long formulas from being well-formed. Colin Howson calls the composition step the principle of composition, and it is what justifies the word "atomic" for the variables, since every formula is built from atoms as ultimate building blocks. Composite formulas are called molecules, an imperfect analogy with chemistry, since a chemical molecule may have only one atom, as in monatomic gases.
Computer science often prefers a context-free grammar written in Backus-Naur form. For the common set of five connectives, a single self-referential clause can specify the entire language, and adding modal operators means only appending to that clause. Mathematicians sometimes split symbols into three kinds. Propositional constants represent particular propositions, written A, B, and C. Propositional variables range over all atomic propositions, written P, Q, and R. Schemata range over all formulas, often the Greek letters φ, ψ, and χ. Some authors keep only two constants, a symbol for truth that always evaluates True and one for falsity that always evaluates False, treating them as zero-place truth-functors.
True or False, exactly one of the two, is what every proposition evaluates to in classical logic. "Wikipedia is a free online encyclopedia that anyone can edit" comes out True, while "Wikipedia is a paper encyclopedia" comes out False. Three assumptions mark this approach as classical: bivalence, that there are only two values; noncontradiction, that only one is assigned to each formula; and excluded middle, that every formula gets a value. Drop those, and you reach many-valued, three-valued, finite-valued, or infinite-valued logics.
An interpretation, also called a valuation, Boolean valuation, or case, assigns a truth value to every formula. A single propositional symbol has two possible interpretations, T or F. A pair of symbols has four. Because the language has denumerably many propositional symbols, there are uncountably many distinct possible interpretations of the language as a whole.
Truth-functionality governs how compound formulas get their values. The truth value of a sentence built from atoms depends only on the truth values of those atoms, an assumption Colin Howson names. The five main connectives, conjunction, disjunction, implication, biconditional, and negation, are each defined by a truth table. Some authors write the same definitions as lists of statements rather than grids.
Not every connective needs its own primitive definition. Implication can be defined from disjunction and negation, and disjunction from negation and conjunction. A truth-functionally complete system can be built from disjunction and negation, as Russell, Whitehead, and Hilbert did, or from implication and negation, as Frege did. Jean Nicod used a single connective, the Sheffer stroke for "not and." A joint denial connective, logical NOR, also suffices alone. Besides NOR and NAND, no other connectives have that property. Howson and Cunningham even separate equivalence, a metalanguage symbol, from the biconditional, a connective in the object language.
Semantic and syntactic, those are the two broad families of proof systems, divided by the kind of consequence they trust. Semantic systems rest on semantic consequence, dealing with truth values across all interpretations. Syntactic systems rest on syntactic consequence, deriving conclusions from premises by rules and axioms inside a formal system. The split runs through everything that follows.
Truth tables and semantic tableaux are the semantic methods. A truth table determines a formula's value in every possible scenario, but it has 2 to the n lines for n variables, which grows tiresomely long. Analytic tableaux are more efficient and still mechanical. They use signed formulas, exploiting the fact that only the truth-value distributions making the premises true or the conclusion false matter for deductive validity. When every branch of the tree closes on a contradiction, the original set is proved self-contradictory.
Axiomatic proof in propositional logic dates back to Gottlob Frege's 1879 Begriffsschrift, which used only implication and negation and had six axioms. Jan Łukasiewicz showed that Frege's third axiom was superfluous, derivable from the first two, and that the last three could be replaced by a single sentence. That left a system of three axioms. Alonzo Church gave the exact same system, called it P2, and helped popularize it. The schematic form of P2 is attributed to John von Neumann, has also been attributed to Hilbert, and is used in the Metamath "set.mm" formal proof database.
Natural deduction takes a different path, using ten primitive inference rules and no axioms beyond them. Its rules pair introduction and elimination for each binary connective, plus reductio ad absurdum. Notation styles vary widely. Gentzen's tree style can be stacked into large tree-shaped proofs. Stanisław Jaśkowski nested formulas inside boxes, a style Fredric Fitch simplified into horizontal and vertical lines. The article itself uses the Suppes-Lemmon style, due to Patrick Suppes and popularized by E.J. Lemmon and Benson Mates, chosen because it is the least graphically intensive to produce.
Soundness and completeness are the well-behaved properties classical propositional logic enjoys. Whenever a formula is derivable it is also valid, and whenever it is valid it is derivable, indeed strongly complete for arbitrary sets of premises. A formula is a theorem if and only if it is logically valid. Compactness adds that a set of formulas is satisfiable if and only if every finite subset is. Syntactic consistency coincides with satisfiability, so the semantic and proof-theoretic notions line up exactly.
Decidability is the property that carries the field out of philosophy and into machines. Because each formula contains only finitely many propositional variables, one can determine in finitely many steps whether it is satisfiable, unsatisfiable, or valid, for example by truth tables. This is a notable difference from predicate calculus. Deciding satisfiability is an NP-complete problem, yet practical methods run fast on many useful cases.
The DPLL algorithm arrived in 1962, and the Chaff algorithm in 2001. Recent work has extended SAT solver algorithms to propositions containing arithmetic expressions, producing the SMT solvers. A logic that Chrysippus sketched in the 3rd century BC, that vanished for over a millennium, now decides formulas inside software, its ancient validity preserved in code.
Common questions
What is propositional logic in classical logic?
Propositional logic is a branch of classical logic that deals with propositions, which can be true or false, and the relations between them. It is also called statement logic, sentential calculus, propositional calculus, sentential logic, or zeroth-order logic. It studies compound propositions formed by logical connectives representing conjunction, disjunction, implication, biconditional, and negation.
Who developed propositional logic?
Chrysippus is often credited with developing a deductive system for propositional logic in the 3rd century BC, work later expanded by his successor Stoics. His logic focused on propositions rather than terms, setting it apart from traditional syllogistic logic. Most of the original writings were lost, and Stoic logic faded into oblivion between the 3rd and 6th century CE before being resurrected in the 20th century.
What is the difference between propositional logic and first-order logic?
Propositional logic does not deal with non-logical objects, predicates about them, or quantifiers, while first-order logic does. All the machinery of propositional logic is included in first-order and higher-order logics, making propositional logic their foundation. By comparison, truth-functional propositional logic is considered zeroth-order logic.
How do truth tables work in propositional logic?
A truth table is a semantic proof method that determines the truth value of a propositional logic expression in every possible scenario by exhaustively listing the truth values of its constituent atoms. A formula is semantically valid if and only if all the lines of its truth table come out true. Truth tables have 2 to the n lines for n variables, so they can become very long for large values of n.
Who invented the truth table?
The truth table's invention is of uncertain attribution. The tabular structure is generally credited to either Ludwig Wittgenstein or Emil Post, or both independently, while ideas influential to its invention appear in the works of Frege and Bertrand Russell. John Shosky concluded that it is far from clear that any one person should be given the title of inventor of truth-tables.
Why is propositional logic decidable and used in computing?
Classical propositional logic is decidable because each formula contains only finitely many propositional variables, so one can determine in finitely many steps whether it is satisfiable, unsatisfiable, or valid. Deciding satisfiability is an NP-complete problem, but practical methods such as the DPLL algorithm from 1962 and the Chaff algorithm from 2001 run fast on many useful cases. Recent work extended SAT solvers to arithmetic expressions, creating SMT solvers.
All sources
116 references cited across the entry
- 1bookBeginning LogicE. J. Lemmon — CRC Press — 1971-09-30
- 2bookSymbolic LogicOdysseus Makridis — 2022
- 3bookSemantics: a readerOxford University Press — 2004
- 4bookApplied Logic for Computer ScientistsMauricio Ayala-Rincón et al. — Springer — 2017
- 5encyclopediaPropositional LogicKevin C. Klement
- 6bookFuzzy logic and mathematics: a historical perspectiveRadim Bělohlávek et al. — Oxford University Press — 2017
- 7bookExtensions of first order logicMaría Manzano — Cambridge University Press — 2005
- 9bookLogic with trees: an introduction to symbolic logicColin Howson — Routledge — 1997
- 11webSequent CalculusEric W. Weisstein
- 12bookA dictionary of philosophical logicRoy T. Cook — Edinburgh University Press — 2009
- 13webPropositional CalculusEric W. Weisstein
- 14bookFundamentals of Artificial IntelligenceK.R. Chowdhary — 2020
- 15encyclopediaPropositional LogicCurtis Franks — Metaphysics Research Lab, Stanford University — 2024
- 16bookMathematical Logic and Formalized TheoriesRobert L. Rogers — Elsevier — 1971
- 17bookLogic: the basicsJeffrey C. Beall — Routledge — 2010
- 18citationPropositionsMatthew McGrath et al. — Metaphysics Research Lab, Stanford University — 2023
- 19webConnectiveEric W. Weisstein
- 20bookStructures for SemanticsFred Landman — 1991
- 21citationLogic and ProbabilityLorenz Demey et al. — Metaphysics Research Lab, Stanford University — 2023
- 22citationTruth ValuesYaroslav Shramko et al. — Metaphysics Research Lab, Stanford University — 2021
- 23webMathematicalLogic
- 24bookLogicWilfrid Hodges — Penguin Books — 2001
- 25bookFirst-Order LogicRaymond M. Smullyan — Dover Publications — 1995
- 26bookElements of logical reasoningJan von Plato — Cambridge University press — 2013
- 27web1.4: Tautologies and contradictions2021-09-09
- 28bookEF Tautologies and contradictionsJeremy Sylvestre
- 29bookElementary Formal LogicCraig DeLancey et al. — Pressbooks — 2017
- 30bookThe connectivesLloyd Humberstone — MIT Press — 2011
- 31citationSubstructural LogicsGreg Restall — Metaphysics Research Lab, Stanford University — 2018
- 32bookLogic primerColin Allen et al. — The MIT Press — 2022
- 34bookLogic: an introductionGreg Restall — Routledge — 2010
- 35bookBeginning logicEdward John Lemmon — Chapman & Hall/CRC — 1998
- 36bookAn introduction to logic: using natural deduction, real arguments, a little history, and some humourRichard T. W. Arthur — Broadview Press — 2017
- 38citationNatural Deduction Systems in LogicFrancis Jeffry Pelletier et al. — Metaphysics Research Lab, Stanford University — 2024
- 39bookLogicWilfrid Hodges — Penguin — 1977
- 40bookIntroduction to formal philosophySven Ove Hansson et al. — Springer — 2018
- 41bookLogical PluralismJ. C. Beall et al. — Clarendon Press — 2006
- 42bookA Beginner's Guide to Mathematical LogicRaymond M. Smullyan — Courier Corporation — 2014-07-23
- 43bookThe Philosophy of Gottlob FregeRichard L. Mendelsohn — Cambridge University Press — 2005-01-10
- 44bookJan Lukasiewicz: Selected WorksJan Łukasiewicz — North-Holland — 1970
- 45bookIntroduction to Mathematical LogicAlonzo Church — Princeton University Press — 1996
- 47bookIntroduction to mathematical logicMichał Walicki — World Scientific — 2017
- 51bookMathematical logicStephen Cole Kleene — Dover Publications — 2002
- 52bookClassical logic and its rabbit holes: a first courseNelson P. Lande — Hackett Publishing Co., Inc — 2013
- 53bookIntermediate logicDavid Bostock — Clarendon Press; Oxford University Press — 1997
- 54bookMetalogic: An Introduction to the Metatheory of Standard First-Order LogicGeoffrey Hunter — University of California Press — 1971
- 56citationAn introduction to formal logicPeter Smith — Cambridge University Press — 2003
- 57citationAn epsilon of room, IITerence Tao — American Mathematical Society — 2010
- 58inlineTruth in Frege
- 59bookPrinciples of Mathematical LogicD. Hilbert et al. — Chelsea Publishing Company — 1950
- 60bookThe Stanford Encyclopedia of PhilosophySusanne Bobzien — Metaphysics Research Lab, Stanford University — 1 January 2016
- 62citationAncient LogicSusanne Bobzien — Metaphysics Research Lab, Stanford University — 2020
- 63bookThe Stanford Encyclopedia of PhilosophyVolker Peckhaus — Metaphysics Research Lab, Stanford University — 1 January 2014
- 64bookA Concise Introduction to Logic 10th editionPatrick Hurley — Wadsworth Publishing — 2007
- 65journalPeirce's Truth-functional Analysis and the Origin of the Truth TableIrving H. Anellis — 2012
- 68webLogical Connectives
- 69webLecture1
- 70webWatson
- 72journalOne's Modus Ponens: Modality, Coherence and LogicUna Stojnić — 2017
- 73citationArgument and ArgumentationCatarina Dutilh Novaes — Metaphysics Research Lab, Stanford University — 2022
- 74citationDeductivism in the Philosophy of MathematicsAlexander Paseau et al. — Metaphysics Research Lab, Stanford University — 2023
- 75bookPrinciples of mathematicsBertrand Russell — Routledge — 2010
- 76bookPropositional and predicate calculus: a model of argumentDerek Goldrei — Springer — 2005
- 77webPropositional Logic
- 81citationClassical LogicStewart Shapiro et al. — Metaphysics Research Lab, Stanford University — 2024
- 82bookFirst-Order Logic and Automated Theorem ProvingMelvin Fitting — Springer Science & Business Media — 2012-12-06
- 83bookFrontiers in quantum methods and applications in chemistry and physics: selected proceedings of QSCP-XVIII (Paraty, Brazil, December, 2013)Marco Antonio Chaer Nascimento — Springer — 2015
- 84bookLogical MethodsGreg Restall et al. — MIT Press — 2023-01-03
- 85citationDisjunctionMaria Aloni — Metaphysics Research Lab, Stanford University — 2023
- 86bookSymbolic logicOdysseus Makridis — Palgrave Macmillan — 2022
- 87bookPhilosophical logicJohn P. Burgess — Princeton University Press — 2009
- 88bookPropositional LogicOscar Levin
- 89bookSet theory: a first courseDaniel W. Cunningham — Cambridge University Press — 2016
- 90bookIntroduction to LogicMichael Genesereth et al. — Springer International Publishing — 2017
- 94bookComputational models of argument: proceedings of comma 2020IOS Press — 2020
- 95bookAdvances in Mathematics Education Research on Proof and Proving: An International PerspectiveSpringer International Publishing : Imprint: Springer — 2018
- 96journalA Concise Introduction to Logic: §4. ProofsCraig DeLancey — 2017
- 97citationsemantic consequenceThomas Macaulay Ferguson et al. — Oxford University Press — 2016-06-23
- 98citationsyntactic consequenceThomas Macaulay Ferguson et al. — Oxford University Press — 2016-06-23
- 99webTruth table Boolean, Operators, Rules Britannica2024-03-14
- 100webAnalytic Tableaux
- 103webPropositional Logic
- 105bookA first course in logicMark V. Lawson — CRC Press, Taylor & Francis Group — 2019
- 106bookLogic and languageNeville Dean — Palgrave Macmillan — 2003
- 107bookMathematical logicIan Chiswell et al. — Oxford university press — 2007
- 108webProof of ImplicationsShunichi Toida — Department of Computer Science, Old Dominion University — 2 August 2009
- 110citationAn introduction to mathematical logic and type theory: to truth through proofPeter B. Andrews — Kluwer Academic Publishers, Dordrecht — 2002
- 111bookExtensions of System F by Iteration and Primitive Recursion on Monotone Inductive TypesRalph Matthes — Herbert Utz Verlag — 1999
- 112webPredicate Logic
- 115bookMathematical LogicW. V. O. Quine — Harvard University Press — 1980
- 116bookRudolf Carnap: studies in semantics: the collected works of rudolf carnap, volume 7Oxford University Press — 2024
- 117bookPrinciples of expert systemsPeter Lucas et al. — Addison-Wesley — 1991
- 118webCSE541 Logic in Computer ScienceLeo Bachmair — 2009