Skip to main content

foundations · Essay 7 · 18 min

Propositional Logic

Propositional logic is the formal study of inference among atomic propositions joined by truth-functional connectives. It is the simplest non-trivial logical system, sound and complete, decidable in time exponential in the number of atoms. The page gives the alphabet, formation rules, truth-functional semantics, the four standard equivalences, the natural-deduction proof system, and three worked exercises with answers.

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:

SymbolRead asOperation
¬\negnotnegation
\landandconjunction
\loror (inclusive)disjunction
\toif ... thenmaterial conditional
\leftrightarrowif and only ifbiconditional

A propositional-logic formula is built recursively from atomic propositional letters (p,q,r,p, q, r, \ldots) 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: p,q,r,p1,p2,p, q, r, p_1, p_2, \ldots.
  • The connectives: ¬,,,,\neg, \land, \lor, \to, \leftrightarrow.
  • Auxiliary punctuation: (( and )).

The formation rules define which strings count as well-formed formulas (wffs):

  1. Every atomic letter is a wff.
  2. If φ\varphi is a wff, so is ¬φ\neg \varphi.
  3. If φ\varphi and ψ\psi are wffs, so are (φψ)(\varphi \land \psi), (φψ)(\varphi \lor \psi), (φψ)(\varphi \to \psi), (φψ)(\varphi \leftrightarrow \psi).
  4. Nothing else is a wff.

Outer parentheses on the topmost connective are conventionally omitted: write pqp \land q rather than (pq)(p \land q). Standard precedence runs ¬>>>>\neg > \land > \lor > \to > \leftrightarrow, with \to right-associative.

By these rules:

  • ¬pq\neg p \land q is a wff (parses as (¬p)q(\neg p) \land q, by precedence).
  • ((pq)r)((p \to q) \to r) is a wff.
  • pqp \lor \to q is not a wff (connectives must have arguments).

Truth-Functional Semantics

A valuation vv assigns each atomic letter a value in {T,F}\{\text{T}, \text{F}\}. The valuation extends recursively to all wffs by the truth tables:

φ\varphiψ\psi¬φ\neg \varphiφψ\varphi \land \psiφψ\varphi \lor \psiφψ\varphi \to \psiφψ\varphi \leftrightarrow \psi
TTFTTTT
TFFFTFF
FTTFTTF
FFTFFTT

The conditional φψ\varphi \to \psi 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 φψ\varphi \to \psi 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 φ\varphi is:

  • A tautology if every valuation makes φ\varphi true. Notation: φ\models \varphi.
  • A contradiction if every valuation makes φ\varphi 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.

NameEquivalence
Double negation¬¬φφ\neg \neg \varphi \equiv \varphi
De Morgan (1)¬(φψ)¬φ¬ψ\neg (\varphi \land \psi) \equiv \neg \varphi \lor \neg \psi
De Morgan (2)¬(φψ)¬φ¬ψ\neg (\varphi \lor \psi) \equiv \neg \varphi \land \neg \psi
Material conditionalφψ¬φψ\varphi \to \psi \equiv \neg \varphi \lor \psi

The last is particularly useful. It shows that the conditional is definable from negation and disjunction, which means the connective set {¬,}\{\neg, \to\} alone (or {¬,}\{\neg, \lor\}, or {¬,}\{\neg, \land\}) 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:

  1. List all atomic letters appearing in the argument.
  2. Construct a truth table with 2n2^n rows for nn atoms.
  3. Compute the truth value of each premise and the conclusion in each row.
  4. 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 2n2^n rows; for n=30n = 30 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 (Γφ    Γφ\Gamma \vdash \varphi \iff \Gamma \models \varphi), and there is a finite procedure that decides which side of the line any given φ\varphi 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).

ConnectiveIntroductionElimination
\landFrom φ\varphi and ψ\psi, infer φψ\varphi \land \psi.From φψ\varphi \land \psi, infer φ\varphi (or ψ\psi).
\lorFrom φ\varphi, infer φψ\varphi \lor \psi (or ψφ\psi \lor \varphi).From φψ\varphi \lor \psi, φχ\varphi \to \chi, ψχ\psi \to \chi, infer χ\chi.
\toAssume φ\varphi; derive ψ\psi; discharge the assumption to obtain φψ\varphi \to \psi.From φ\varphi and φψ\varphi \to \psi, infer ψ\psi (modus ponens).
¬\negAssume φ\varphi; derive \bot (a contradiction); discharge to obtain ¬φ\neg \varphi.From φ\varphi and ¬φ\neg \varphi, infer \bot.
\bot(no introduction; \bot is a primitive contradiction)From \bot, infer any φ\varphi (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 (¬¬φφ\neg \neg \varphi \vdash \varphi) or its equivalents (excluded middle, reductio ad absurdum); intuitionistic logic does not.

A worked derivation. To show pq,qrprp \to q,\, q \to r \vdash p \to r:

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 prp \to r is established without invoking truth tables.

Soundness, Completeness, Decidability

Three results that together characterize the relationship between propositional-logic syntax and semantics.

Soundness. If Γφ\Gamma \vdash \varphi in natural deduction, then Γφ\Gamma \models \varphi. Anything provable is true in every model of the premises.

Completeness (Post 1921; later by Kalmár).2 If Γφ\Gamma \models \varphi, then Γφ\Gamma \vdash \varphi. Anything true in every model of the premises has a proof.

Decidability. There is an algorithm (the truth-table method) that decides, for any φ\varphi, whether φ\models \varphi. The algorithm runs in time Θ(2nsize(φ))\Theta(2^n \cdot \text{size}(\varphi)) where nn is the number of atomic letters. The associated decision problem is the satisfiability problem SAT: given φ\varphi, 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.

  1. 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.
  2. Modal qualifications. "It is necessary that pp" or "It is possible that pp" require modal operators not present in propositional logic. This is the gap modal logic fills.
  3. 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 pqp \to q is true whenever pp is false, regardless of qq. 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 \to only when the truth-functional reading is intended.

Confusion 2: "or" inclusive vs exclusive. Propositional disjunction pqp \lor q 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 (pq)¬(pq)(p \lor q) \land \neg (p \land q), 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:

(pq)(¬q¬p)(p \to q) \to (\neg q \to \neg p)

Exercise 2. Decide whether the argument is valid:

Premise 1: pqp \lor q. Premise 2: prp \to r. Premise 3: qrq \to r. Conclusion: rr.

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 {¬,}\{\neg, \to\}, write a propositional formula that is logically equivalent to pqp \land q. (Hint: start from the equivalence φψ¬φψ\varphi \to \psi \equiv \neg \varphi \lor \psi and work backward to express \land in terms of ¬\neg and \to.)

Answers

Answer 1: tautology. This is the contrapositive equivalence: pqp \to q and ¬q¬p\neg q \to \neg p are logically equivalent. The full conditional (pq)(¬q¬p)(p \to q) \to (\neg q \to \neg p) is therefore true under every valuation. Verify by truth table:

ppqqpqp \to q¬q¬p\neg q \to \neg p(pq)(¬q¬p)(p \to q) \to (\neg q \to \neg p)
TTTTT
TFFFT
FTTTT
FFTTT

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 pqp \lor q, combined with the corresponding conditional, yields rr.

Answer 3. Use the equivalence pq¬(p¬q)p \land q \equiv \neg (p \to \neg q).

To verify by truth table:

ppqq¬q\neg qp¬qp \to \neg q¬(p¬q)\neg (p \to \neg q)pqp \land q
TTFFTT
TFTTFF
FTFTFF
FFTTFF

The two rightmost columns agree on every valuation.

The fact that {¬,}\{\neg, \to\} suffices to express conjunction (and, similarly, all other Boolean operations) is the functional completeness of that connective set. Other complete sets include {¬,}\{\neg, \land\}, {¬,}\{\neg, \lor\}, 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

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

Footnotes

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

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