What It Is
Propositional logic is the simplest non-trivial formal logical system. It studies inference at the level of whole atomic propositions joined by truth-functional connectives. "Atomic" here means: each proposition is treated as a single unit that is either true or false; the internal structure of the proposition (subject, predicate, quantifier) is invisible at this level. That internal structure is the subject of predicate logic.
The five standard connectives are:
| Symbol | Read as | Operation |
|---|---|---|
| not | negation | |
| and | conjunction | |
| or (inclusive) | disjunction | |
| if ... then | material conditional | |
| if and only if | biconditional |
A propositional-logic formula is built recursively from atomic propositional letters () using these connectives.
This page assumes the framework laid out in What Is Logic?, Validity vs Soundness, and Syntax vs Semantics in Formal Systems. It is also the canonical instance of the abstract triple defined in What Is a Symbolic System?: alphabet, formation rules, interpretation.
Notation and Formation Rules
The alphabet is:
- A countable set of atomic propositional letters: .
- The connectives: .
- Auxiliary punctuation: and .
The formation rules define which strings count as well-formed formulas (wffs):
- Every atomic letter is a wff.
- If is a wff, so is .
- If and are wffs, so are , , , .
- Nothing else is a wff.
Outer parentheses on the topmost connective are conventionally omitted: write rather than . Standard precedence runs , with right-associative.
By these rules:
- is a wff (parses as , by precedence).
- is a wff.
- is not a wff (connectives must have arguments).
Truth-Functional Semantics
A valuation assigns each atomic letter a value in . The valuation extends recursively to all wffs by the truth tables:
| T | T | F | T | T | T | T |
| T | F | F | F | T | F | F |
| F | T | T | F | T | T | F |
| F | F | T | F | F | T | T |
The conditional is the material conditional. It is false only when the antecedent is true and the consequent is false. The cases where the antecedent is false (rows 3, 4) make vacuously true. This is sometimes counterintuitive when reading natural-language conditionals, where "if" often carries causal or evidential implication. The material conditional is what is needed for clean truth-functional semantics; everything else is built around it.
A formula is:
- A tautology if every valuation makes true. Notation: .
- A contradiction if every valuation makes false.
- Contingent if some valuations make it true and some make it false.
The set of tautologies is closed under substitution and modus ponens; that is the central technical fact making propositional logic well-behaved.
Four Standard Equivalences
These are the equivalences used most often in propositional manipulation. Each can be verified by truth table.
| Name | Equivalence |
|---|---|
| Double negation | |
| De Morgan (1) | |
| De Morgan (2) | |
| Material conditional |
The last is particularly useful. It shows that the conditional is definable from negation and disjunction, which means the connective set alone (or , or ) is functionally complete: any propositional truth function can be expressed using just those two connectives. This is one reason propositional logic is so well-behaved compared to richer systems.
The Truth-Table Method
Truth tables decide validity in propositional logic. The procedure:
- List all atomic letters appearing in the argument.
- Construct a truth table with rows for atoms.
- Compute the truth value of each premise and the conclusion in each row.
- The argument is valid iff every row in which all premises are T also has the conclusion T.
This is mechanical. A computer can run it for any propositional argument. The catch is that the table has rows; for atoms, that is roughly a billion rows. Validity in propositional logic is a decidable problem (you can always reach an answer in finite time) but not in general tractable (the time grows exponentially in the number of atoms).
This is the cleanest concrete instance of the soundness-completeness-decidability triple introduced in Syntax vs Semantics: for propositional logic, syntactic provability and semantic validity coincide (), and there is a finite procedure that decides which side of the line any given falls on.
Natural Deduction
Truth tables decide validity but they do not produce a proof in the syntactic sense. For that we need a proof system. Natural deduction (Gentzen 1934, Prawitz 1965)1 is the most widely taught.
Each connective has an introduction rule (how to derive a formula with that connective at the top) and an elimination rule (how to use such a formula).
| Connective | Introduction | Elimination |
|---|---|---|
| From and , infer . | From , infer (or ). | |
| From , infer (or ). | From , , , infer . | |
| Assume ; derive ; discharge the assumption to obtain . | From and , infer (modus ponens). | |
| Assume ; derive (a contradiction); discharge to obtain . | From and , infer . | |
| (no introduction; is a primitive contradiction) | From , infer any (ex falso quodlibet). |
A natural-deduction derivation is a finite tree of applications of these rules whose leaves are either premises or discharged assumptions and whose root is the conclusion. The classical-logic system additionally permits double-negation elimination () or its equivalents (excluded middle, reductio ad absurdum); intuitionistic logic does not.
A worked derivation. To show :
1. p → q premise
2. q → r premise
3. p assumption (for →-introduction)
4. q modus ponens on 1, 3
5. r modus ponens on 2, 4
6. p → r →-introduction, discharging assumption 3
The derivation is sound (every step preserves truth) and uses only natural-deduction rules. The conclusion is established without invoking truth tables.
Soundness, Completeness, Decidability
Three results that together characterize the relationship between propositional-logic syntax and semantics.
Soundness. If in natural deduction, then . Anything provable is true in every model of the premises.
Completeness (Post 1921; later by Kalmár).2 If , then . Anything true in every model of the premises has a proof.
Decidability. There is an algorithm (the truth-table method) that decides, for any , whether . The algorithm runs in time where is the number of atomic letters. The associated decision problem is the satisfiability problem SAT: given , does there exist a valuation making it true? SAT is the canonical NP-complete problem (Cook 1971). Whether SAT can be decided in polynomial time is the famous P vs NP question.
The combination of soundness and completeness means propositional logic is adequate: anything that is logically true has a proof, and any proof produces a logical truth. Decidability adds: that proof can in principle be found by a finite mechanical procedure. Few logical systems satisfy all three. First-order logic (predicate logic) is sound and complete but undecidable. Higher-order logic loses completeness.
What Propositional Logic Cannot Express
Three things propositional logic cannot say, that more expressive systems can.
- Relations among objects. "All cats are mammals" requires a quantifier and a predicate; in propositional logic it can only be encoded as a single atomic letter, losing all internal structure. This is the gap predicate logic fills.
- Modal qualifications. "It is necessary that " or "It is possible that " require modal operators not present in propositional logic. This is the gap modal logic fills.
- Quantification over predicates. "There is a property that all natural numbers share" requires quantifying over predicates; propositional and first-order logic cannot. Higher-order logic (typed lambda calculus, type theory) is needed.
These are not failures of propositional logic. Propositional logic is the well-behaved layer; the cost of expressive extensions is some combination of decidability, completeness, or simplicity.
Common Confusions
Confusion 1: material conditional vs natural-language "if". The material conditional is true whenever is false, regardless of . Natural-language "if" often carries causal or evidential weight that the material conditional does not. A common pedagogical example: "If the moon is made of cheese, then 2 + 2 = 4" is true under the material conditional reading (vacuously), although it sounds odd in natural language. The discipline is to use only when the truth-functional reading is intended.
Confusion 2: "or" inclusive vs exclusive. Propositional disjunction is inclusive: true when at least one disjunct is true. Natural-language "or" is sometimes exclusive ("you can have soup or salad" usually excludes both). Exclusive disjunction is expressible in propositional logic as , but it is not one of the standard connectives.
Confusion 3: validity vs soundness. Truth tables establish validity in propositional logic, not soundness. An argument can be propositionally valid with a false premise; the argument's conclusion may then also be false. See Validity vs Soundness for the full distinction.
Confusion 4: tautology vs contingent truth. A tautology is true under every valuation, by virtue of its propositional form. A contingent truth is true under the actual valuation but false under others. "All cats are mammals" is contingently true: there is a valuation in which the relevant atom is false. Tautologies are logical truths; contingent truths are empirical truths that happen to hold.
Three Exercises
Exercise 1. Use a truth table to determine whether the following formula is a tautology, a contradiction, or contingent:
Exercise 2. Decide whether the argument is valid:
Premise 1: . Premise 2: . Premise 3: . Conclusion: .
If valid, give a natural-deduction derivation. If invalid, give a valuation that makes the premises true and the conclusion false.
Exercise 3. Using only the connectives , write a propositional formula that is logically equivalent to . (Hint: start from the equivalence and work backward to express in terms of and .)
Answers
Answer 1: tautology. This is the contrapositive equivalence: and are logically equivalent. The full conditional is therefore true under every valuation. Verify by truth table:
| T | T | T | T | T |
| T | F | F | F | T |
| F | T | T | T | T |
| F | F | T | T | T |
Every row in the final column is T.
Answer 2: valid. This is constructive dilemma. Natural-deduction derivation:
1. p ∨ q premise
2. p → r premise
3. q → r premise
4. | p assumption (for ∨-elim case 1)
5. | r modus ponens on 2, 4
6. | q assumption (for ∨-elim case 2)
7. | r modus ponens on 3, 6
8. r ∨-elimination on 1, 4-5, 6-7
The argument is valid because either disjunct of , combined with the corresponding conditional, yields .
Answer 3. Use the equivalence .
To verify by truth table:
| T | T | F | F | T | T |
| T | F | T | T | F | F |
| F | T | F | T | F | F |
| F | F | T | T | F | F |
The two rightmost columns agree on every valuation.
The fact that suffices to express conjunction (and, similarly, all other Boolean operations) is the functional completeness of that connective set. Other complete sets include , , and the single Sheffer stroke (NAND).
Where Propositional Logic Lives in Practice
Three concrete uses.
Digital circuits. Every Boolean circuit (AND, OR, NOT gates) computes a propositional formula. Logic synthesis is the engineering practice of finding small circuits equivalent to given propositional formulas. The connection runs both ways: hardware verification reduces to propositional satisfiability checking on circuit-level formulas.
SAT solvers. Modern satisfiability solvers (MiniSat, CaDiCaL, Glucose) decide propositional SAT instances with millions of variables in practical time. They are used in formal verification, AI planning, software model checking, and hardware design. SAT is NP-complete in worst case, but real-world instances often have structure that solvers exploit.
Proof verification and program analysis. Lean, Coq, and Isabelle implement richer logics whose propositional fragment is exactly classical or intuitionistic propositional logic. Static analyzers and type checkers reduce many decidable subproblems to propositional satisfiability.
The point: propositional logic looks austere, but it is the substrate of substantial parts of modern computer science and verification engineering. Its decidability is what makes it useful.
Prerequisites and Next Pages
- Prerequisites: What Is Logic?, Validity vs Soundness, Syntax vs Semantics in Formal Systems, What Is a Symbolic System?.
- Next: Predicate Logic, the natural extension that adds quantifiers and predicates.
- Next: Modal Logic, the natural extension that adds operators for necessity and possibility.
- Next: The Liar Paradox, which exploits self-reference to generate a contradiction in any system rich enough to express its own truth predicate.
References
Primary texts:
- Boole, George. An Investigation of the Laws of Thought. Walton and Maberly, 1854. The founding work of algebraic logic.
- Frege, Gottlob. Begriffsschrift. 1879. Introduces the modern formal notation; the propositional fragment is implicit in the larger system.
- Post, Emil L. "Introduction to a General Theory of Elementary Propositions." American Journal of Mathematics 43, no. 3 (1921): 163-185. The completeness theorem for classical propositional logic.
- Gentzen, Gerhard. "Untersuchungen über das logische Schließen." 1934. The introduction of natural deduction.
Modern reference:
- Hurley, Patrick, and Lori Watson. A Concise Introduction to Logic. Cengage, 13th ed., 2017. Standard introductory textbook coverage of propositional logic.
- Smith, Peter. An Introduction to Formal Logic. Cambridge, 2nd ed., 2020. Open-access at logicmatters.net. Cleaner mathematical depth than Hurley.
- Mendelson, Elliott. Introduction to Mathematical Logic. CRC Press, 6th ed., 2015. Graduate-level treatment with full soundness and completeness proofs.
- Sipser, Michael. Introduction to the Theory of Computation. Cengage, 3rd ed., 2013. SAT, NP-completeness, and the computational view of propositional satisfiability.
Stanford Encyclopedia entries (link, do not paraphrase):
- "Classical Logic."
- "Propositional Logic" (within Classical Logic).
- "Truth Tables."
Footnotes
-
Gentzen, Gerhard. "Untersuchungen über das logische Schließen." Mathematische Zeitschrift 39 (1934): 176-210, 405-431. English translation in M. E. Szabo, ed., The Collected Papers of Gerhard Gentzen, North-Holland, 1969. ↩
-
Post, Emil L. "Introduction to a General Theory of Elementary Propositions." American Journal of Mathematics 43, no. 3 (1921): 163-185. The completeness theorem for classical propositional logic. ↩