Propositional logic and truth tables

Lens

MotivationH

Four cards

Four cards lie on a table. Each card has a letter on one side and a whole number on the other. You can see

\boxed{\mathrm{A}} \qquad \boxed{\mathrm{K}} \qquad \boxed{4} \qquad \boxed{7}

Someone claims: "If a card has a vowel on one side, then it has an even number on the other side." Which cards must you turn over to find out whether the claim is false?

Take a moment and decide before reading on.

This is the selection task devised by the psychologist Peter Wason in 1966. In experiment after experiment, only a small minority of people answer it correctly the first time — usually people turn over the A and the 4, or just the A. The difficulty is not cleverness; it is that the everyday word "if" is slippery. In this lesson we make "and", "or", "not" and "if … then" completely precise, and the puzzle will become easy.

IntuitionH

A promise and when it is broken

Suppose your teacher says: "If you hand in your project by Friday, then you will get a free afternoon next week." Is the promise kept or broken? There are only four possibilities.

You hand it in by Friday	You get the free afternoon	Was the promise broken?
yes	yes	no — kept
yes	no	yes — broken
no	yes	no
no	no	no

The promise is broken in exactly one case: you did your part and the teacher did not. If you did not hand the project in, the promise says nothing about what happens — whatever the teacher does, the promise has not been broken.

Mathematicians read every "if $P$ then $Q$ " this way. It is a claim that rules out one situation only: $P$ true and $Q$ false.

DefinitionsH

Connectives and truth tables

Definition— proposition

A proposition (or statement) is a sentence that is either true or false. Propositional variables $P, Q, R, \dots$ stand for propositions whose truth value we leave open.

" $7$ is prime" and " $2 + 2 = 5$ " are propositions (true and false). "Close the door" and " $x > 3$ " are not: the first is not true or false, and the second becomes true or false only once $x$ is known — or once we say "for every $x$ " or "for some $x$ ".

Definition— the connectives

From propositions $P$ and $Q$ we build new ones, whose truth values are given by the table ( $\mathrm{T}$ = true, $\mathrm{F}$ = false):

$P$	$Q$	$\neg P$	$P \wedge Q$	$P \vee Q$	$P \to Q$	$P \leftrightarrow Q$
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

$\neg P$ , "not $P$ ", is true exactly when $P$ is false.
$P \wedge Q$ , " $P$ and $Q$ ", is true exactly when both are true.
$P \vee Q$ , " $P$ or $Q$ ", is true when at least one is true (inclusive or).
$P \to Q$ , "if $P$ then $Q$ " (the conditional), is false only when $P$ is true and $Q$ is false. $P$ is its hypothesis and $Q$ its conclusion.
$P \leftrightarrow Q$ , " $P$ if and only if $Q$ ", is true when $P$ and $Q$ have the same truth value.

The exclusive "or" — "one or the other but not both", written $P \oplus Q$ — is true in the middle two rows only. In mathematics a bare "or" always means the inclusive one.

Definition— formula, truth table

A formula is built from propositional variables with the connectives (and brackets). An assignment gives each variable the value T or F; the truth table of a formula lists its value under every assignment. A formula in $n$ variables has $2^n$ rows, because each variable doubles the number of cases.

Brackets are removed by a convention: $\neg$ binds most tightly, then $\wedge$ and $\vee$ , then $\to$ and $\leftrightarrow$ . So $\neg P \vee Q \to R$ means $\big((\neg P) \vee Q\big) \to R$ . When in doubt, write the brackets.

Definition— tautology, contradiction, equivalence

A formula is a tautology if it is true in every row of its truth table, a contradiction if it is false in every row, and contingent otherwise. Two formulas $\varphi$ and $\psi$ are logically equivalent, written $\varphi \equiv \psi$ , if they have the same truth value in every row — equivalently, if $\varphi \leftrightarrow \psi$ is a tautology.

Note that $\equiv$ is not a new connective: it is a statement about two formulas.

Definition— converse, inverse, contrapositive

For the conditional $P \to Q$ :

its converse is $Q \to P$ ;
its inverse is $\neg P \to \neg Q$ ;
its contrapositive is $\neg Q \to \neg P$ .

English has many ways to say $P \to Q$ , and it pays to learn them:

English	Formula
if $P$ then $Q$ ; $Q$ if $P$ ; $Q$ whenever $P$	$P \to Q$
$P$ only if $Q$	$P \to Q$
$P$ is sufficient for $Q$ ; $Q$ is necessary for $P$	$P \to Q$
$P$ if and only if $Q$ ("iff")	$P \leftrightarrow Q$
$Q$ unless $P$	$\neg P \to Q$ , which is equivalent to $P \vee Q$

Worked examplesH

Worked examples

Example— A truth table with sub-formulas

Let us show that $P \to Q$ is equivalent to $\neg P \vee Q$ :

$P$	$Q$	$\neg P$	$\neg P \vee Q$	$P \to Q$
T	T	F	T	T
T	F	F	F	F
F	T	T	T	T
F	F	T	T	T

The last two columns agree in all four rows, so $P \to Q \equiv \neg P \vee Q$ . In words: "if $P$ then $Q$ " says "either $P$ fails, or $Q$ holds".

Example— The four cards, solved

Write $V$ for "this card has a vowel" and $E$ for "this card has an even number". The claim, for each card, is $V \to E$ . It is broken only by a card with $V$ true and $E$ false — a vowel with an odd number.

A: $V$ is true. If the back is odd, the claim is broken. Turn it over.
K: $V$ is false, so $V \to E$ is true whatever is on the back. Leave it.
4: $E$ is true, so $V \to E$ is true whatever is on the back. Leave it. (Turning it is checking the converse $E \to V$ , which nobody claimed.)
7: $E$ is false. If the back is a vowel, the claim is broken. Turn it over. This is the contrapositive at work: $V \to E$ is the same claim as $\neg E \to \neg V$ .

The answer is A and 7.

Example— Necessary versus sufficient

"You may vote in the national election only if you are at least 18" is $V \to A$ , with $V$ = "you may vote" and $A$ = "you are at least 18". Being 18 is necessary. Its converse "if you are at least 18, you may vote" is a different claim — in many countries you must also be a citizen and registered. So being 18 is not sufficient.

Example— Negating a conditional

What is the negation of "If it is a public holiday, then the bakery is closed"? It is not "If it is a public holiday, then the bakery is open". The original claim is false exactly when there is a public holiday on which the bakery is open, so the negation is

"It is a public holiday and the bakery is open."

In symbols, $\neg(P \to Q) \equiv P \wedge \neg Q$ . The negation of an "if" statement is an "and" statement.

Example— Negating a quantified statement

"Every prime number is odd" means: for every number $n$ , if $n$ is prime then $n$ is odd — $\forall n\,\big(\mathrm{Prime}(n) \to \mathrm{Odd}(n)\big)$ . Its negation is "some prime is not odd":

\neg\, \forall n\,\big(\mathrm{Prime}(n) \to \mathrm{Odd}(n)\big) \;\equiv\; \exists n\,\big(\mathrm{Prime}(n) \wedge \neg\mathrm{Odd}(n)\big),

and this negation is true: $2$ is an even prime. The original statement is false, refuted by one counterexample. Quantifiers were introduced in set-builder notation and quantifiers.

Explore

Explore: truth tables that build themselves

Type any formula; the table, its sub-formula columns and its classification update as you type. The second box tests equivalence and marks the rows where two formulas differ.

A conditional and its contrapositive

Now change the second formula to q -> p (the converse) and then to ~p -> ~q (the inverse).

Formula

Read as: p → q

Compare with

Read as: ¬q → ¬p

Use the symbols ¬ ∧ ∨ → ↔, the words not, and, or, implies, iff, or ASCII ~ & | -> <->. Variables are single lowercase letters. ¬ binds tightest, then ∧, ∨, →, ↔; p → q → r means p → (q → r).

Try:

Contingent — true in 3 of 4 rows, false in the others.

Equivalent — the two formulas agree in all 4 rows.

p	q	p → q	¬q → ¬p
T	T	T	T
T	F	F	F
F	T	T	T
F	F	T	T

4 rows: one for every way of making the 2 variables true or false.

Things to try:

Replace the second formula by q -> p. Which rows differ? Is the converse equivalent to the inverse?
Check De Morgan's laws: compare not (p and q) with not p or not q, and not (p or q) with not p and not q. Then try the wrong version not p and not q against not (p and q).
Is (p -> q) -> (q -> p) a tautology? What about ((p -> q) and p) -> q?

A chain of implications

Three variables give 2³ = 8 rows. Is this argument form always valid?

Formula

Read as: ((p → q) ∧ (q → r)) → (p → r)

Try:

Tautology — true in all 8 rows.

p	q	r	(p → q) ∧ (q → r) → (p → r)
T	T	T	T
T	T	F	T
T	F	T	T
T	F	F	T
F	T	T	T
F	T	F	T
F	F	T	T
F	F	F	T

8 rows: one for every way of making the 3 variables true or false.

ProofH

The laws, and why they hold

For propositional formulas, a truth table is a proof: it checks every possible case, and there are only finitely many. But tables grow fast, and reasoning often explains more. We give both.

Theorem— Theorem 1 (contrapositive and converse)

$P \to Q \equiv \neg Q \to \neg P$ . But $P \to Q$ is not equivalent to its converse $Q \to P$ , nor to its inverse $\neg P \to \neg Q$ .

Proof

The truth table:

$P$	$Q$	$P \to Q$	$\neg Q \to \neg P$	$Q \to P$	$\neg P \to \neg Q$
T	T	T	T	T	T
T	F	F	F	T	T
F	T	T	T	F	F
F	F	T	T	T	T

The third and fourth columns agree in every row, so the conditional and its contrapositive are equivalent. In the row $P = \mathrm{F}$ , $Q = \mathrm{T}$ the conditional is true but the converse and inverse are false, so neither is equivalent to it. (The converse and inverse agree with each other: the inverse is the contrapositive of the converse.)

In words: $P \to Q$ is false exactly when $P$ is true and $Q$ is false; $\neg Q \to \neg P$ is false exactly when $\neg Q$ is true and $\neg P$ is false — the same situation.

∎

Theorem— Theorem 2 (De Morgan's laws)

$\neg(P \wedge Q) \equiv \neg P \vee \neg Q$ and $\neg(P \vee Q) \equiv \neg P \wedge \neg Q$ .

Proof

$\neg(P \wedge Q)$ is true exactly when $P \wedge Q$ is false, that is, when at least one of $P, Q$ is false, that is, when at least one of $\neg P, \neg Q$ is true — which is exactly when $\neg P \vee \neg Q$ is true. Similarly, $\neg(P \vee Q)$ is true exactly when $P \vee Q$ is false, that is, when both $P$ and $Q$ are false, that is, when $\neg P \wedge \neg Q$ is true. (Each argument checks all four rows at once; you can also write out the tables.)

∎

Theorem— Theorem 3 (negating a conditional)

$\neg(P \to Q) \equiv P \wedge \neg Q$ . Also $P \to Q \equiv \neg P \vee Q$ .

Proof

$P \to Q$ is false in exactly one row, $P = \mathrm{T}$ , $Q = \mathrm{F}$ . So $\neg(P \to Q)$ is true in exactly that row — and $P \wedge \neg Q$ is true in exactly that row too. For the second equivalence, see the first worked example; or apply De Morgan to the first: $P \to Q \equiv \neg\neg(P \to Q) \equiv \neg(P \wedge \neg Q) \equiv \neg P \vee \neg\neg Q \equiv \neg P \vee Q$ .

∎

Equivalences can be chained like equalities, which gives a second proof of Theorem 1 with no table at all:

P \to Q \;\equiv\; \neg P \vee Q \;\equiv\; Q \vee \neg P \;\equiv\; \neg(\neg Q) \vee \neg P \;\equiv\; \neg Q \to \neg P .

Here we used Theorem 3 (twice), that $\vee$ is commutative, and that $\neg\neg Q \equiv Q$ .

Theorem— Theorem 4 (negating quantifiers)

For any property $A(x)$ : $\;\neg\,\forall x\, A(x) \equiv \exists x\, \neg A(x)\;$ and $\;\neg\,\exists x\, A(x) \equiv \forall x\, \neg A(x)$ . Consequently

\neg\, \forall x\, \big(P(x) \to Q(x)\big) \;\equiv\; \exists x\, \big(P(x) \wedge \neg Q(x)\big).

Proof

"Not every $x$ has $A$ " says that at least one $x$ fails to have $A$ , which is $\exists x\, \neg A(x)$ ; and "no $x$ has $A$ " says that every $x$ fails to have $A$ . For the last line, apply the first rule with $A(x) = P(x) \to Q(x)$ and then Theorem 3 inside: $\neg\big(P(x) \to Q(x)\big) \equiv P(x) \wedge \neg Q(x)$ .

∎

Quantified statements about infinitely many $x$ cannot be checked by a finite truth table — this is one reason mathematics needs proofs, which the next lesson, proof techniques, is all about.

Valid arguments. An argument with premises $\varphi_1, \dots, \varphi_k$ and conclusion $\psi$ is valid when $(\varphi_1 \wedge \dots \wedge \varphi_k) \to \psi$ is a tautology: in every row where all the premises are true, so is the conclusion.

Argument form	Premises	Conclusion	Valid?
modus ponens	$P \to Q$ , $P$	$Q$	yes
modus tollens	$P \to Q$ , $\neg Q$	$\neg P$	yes
hypothetical syllogism	$P \to Q$ , $Q \to R$	$P \to R$	yes
affirming the consequent	$P \to Q$ , $Q$	$P$	no: row $P = \mathrm{F}$ , $Q = \mathrm{T}$
denying the antecedent	$P \to Q$ , $\neg P$	$\neg Q$	no: row $P = \mathrm{F}$ , $Q = \mathrm{T}$

Modus tollens is the contrapositive in action — exactly why the 7 in the card puzzle must be turned over.

Theorem— Theorem 5 (every truth table comes from a formula)

For every $n \ge 1$ and every way of filling in the final column of a truth table with $n$ variables, there is a formula using only $\neg$ , $\wedge$ and $\vee$ with exactly that truth table. In particular there are exactly $2^{2^n}$ different truth tables in $n$ variables, and each is the table of some formula.

Proof

For each row in which the final column is T, write the conjunction of $n$ literals describing that row: $P_i$ if $P_i$ is true in the row, $\neg P_i$ if it is false. This conjunction is true in that row and in no other. Now join all these conjunctions with $\vee$ . The result is true exactly in the rows marked T. If no row is marked T, use the contradiction $P_1 \wedge \neg P_1$ . (Such a formula is in disjunctive normal form.) Finally, a table has $2^n$ rows and each can be marked T or F independently, giving $2^{2^n}$ possible final columns.

∎

For example, the table of exclusive or (T only in the rows TF and FT) gives $(P \wedge \neg Q) \vee (\neg P \wedge Q)$ .

Formal mathematicsF

Truth tables and logic in Lean

We formalise propositional logic twice: once as computation (formulas whose truth values are calculated, exactly as in a table) and once inside Lean's own logic.

Formulas as data. A Formula n is a formula in $n$ variables. Its truth value in a row v (an assignment of true/false to the variables) is computed by Formula.eval. Notice how the conditional is evaluated: !a || b, "not $P$ , or $Q$ " — Theorem 3.

FormulaLean 4Formally verified

/-- Propositional formulas in `n` variables `x₀, …, xₙ₋₁`: variables, the constants true and
false, and the connectives not, and, or, implies and if-and-only-if. -/
inductive Formula (n : ℕ) : Type where
  | var : Fin n → Formula n
  | tt : Formula n
  | ff : Formula n
  | not : Formula n → Formula n
  | and : Formula n → Formula n → Formula n
  | or : Formula n → Formula n → Formula n
  | imp : Formula n → Formula n → Formula n
  | iff : Formula n → Formula n → Formula n

Axioms used: No axiomsformal/Lumenary/PropositionalLogic.leanTry it in the Lean web editor

evalLean 4Formally verified

/-- The truth value of a formula in one row of its truth table. A row (a *valuation*) `v`
assigns `true` or `false` to each variable. Note the conditional: `φ → ψ` is false only when
`φ` is true and `ψ` is false, i.e. it has the value `!φ || ψ`. -/
def Formula.eval {n : ℕ} (v : Fin n → Bool) : Formula n → Bool
  | .var i => v i
  | .tt => true
  | .ff => false
  | .not φ => !φ.eval v
  | .and φ ψ => φ.eval v && ψ.eval v
  | .or φ ψ => φ.eval v || ψ.eval v
  | .imp φ ψ => !φ.eval v || ψ.eval v
  | .iff φ ψ => φ.eval v == ψ.eval v

Axioms used: No axiomsformal/Lumenary/PropositionalLogic.leanTry it in the Lean web editor

The rows of a truth table are listed by valuations n. We prove two things about it: there are $2^n$ rows, and no row is missing. The second is what makes the truth-table method trustworthy.

valuationsLean 4Formally verified

/-- All rows of a truth table in `n` variables, in textbook order (the first variable is true
in the first half of the rows, false in the second half, and so on recursively). -/
def valuations : (n : ℕ) → List (Fin n → Bool)
  | 0 => [fun i => i.elim0]
  | n + 1 => [true, false].flatMap fun b => (valuations n).map (Fin.cons b)

Axioms used: propextformal/Lumenary/PropositionalLogic.leanTry it in the Lean web editor

length_valuationsLean 4Proved here from basic factsFormally verified

/-- A truth table in `n` variables has `2 ^ n` rows: each new variable doubles the number of
rows, once with the variable true and once with it false. Proved by induction on `n`. -/
theorem length_valuations (n : ℕ) : (valuations n).length = 2 ^ n := by
  induction n with
  | zero => rfl
  | succ n ih => simp [valuations, ih, pow_succ, Nat.mul_two]

Axioms used: propextformal/Lumenary/PropositionalLogic.leanTry it in the Lean web editor

mem_valuationsLean 4Proved here from basic factsFormally verified

/-- **Every row appears.** Any assignment of truth values to `n` variables is one of the rows
listed by `valuations n`. Proof by induction on `n`: an assignment to `n + 1` variables is its
value on the first variable followed by an assignment to the remaining `n`
(`Fin.cons_self_tail`). -/
theorem mem_valuations : ∀ (n : ℕ) (v : Fin n → Bool), v ∈ valuations n
  | 0, v => by
    simp only [valuations, List.mem_singleton]
    funext i
    exact i.elim0
  | n + 1, v => by
    simp only [valuations, List.mem_flatMap, List.mem_map]
    refine ⟨v 0, by cases v 0 <;> simp, Fin.tail v, mem_valuations n (Fin.tail v), ?_⟩
    exact Fin.cons_self_tail v

Axioms used: propext, Quot.soundformal/Lumenary/PropositionalLogic.leanTry it in the Lean web editor

isTautologyLean 4Formally verified

/-- The **truth-table test**: a formula passes when it is true in every row of its table. -/
def isTautology {n : ℕ} (φ : Formula n) : Bool := (valuations n).all fun v => φ.eval v

Axioms used: propextformal/Lumenary/PropositionalLogic.leanTry it in the Lean web editor

isTautology_iffLean 4Proved here from basic factsFormally verified

/-- **The truth-table method is correct.** The finite check `isTautology φ` succeeds exactly
when `φ` is true under *every* assignment, i.e. exactly when `φ` is a tautology. The forward
direction needs `mem_valuations`: no row has been forgotten. -/
theorem isTautology_iff {n : ℕ} (φ : Formula n) :
    isTautology φ = true ↔ ∀ v : Fin n → Bool, φ.eval v = true := by
  unfold isTautology
  rw [List.all_eq_true]
  exact ⟨fun h v => h v (mem_valuations n v), fun h v _ => h v⟩

Axioms used: propext, Quot.soundformal/Lumenary/PropositionalLogic.leanTry it in the Lean web editor

EquivalentLean 4Formally verified

/-- Two formulas are **logically equivalent** when they have the same truth value in every row
of the truth table. -/
def Equivalent {n : ℕ} (φ ψ : Formula n) : Prop := ∀ v : Fin n → Bool, φ.eval v = ψ.eval v

Axioms used: No axiomsformal/Lumenary/PropositionalLogic.leanTry it in the Lean web editor

equivalent_iff_tautologyLean 4Proved here from basic factsFormally verified

/-- `φ` and `ψ` are equivalent exactly when the biconditional `φ ↔ ψ` is a tautology, so the
truth-table test also decides equivalence. -/
theorem equivalent_iff_tautology {n : ℕ} (φ ψ : Formula n) :
    Equivalent φ ψ ↔ isTautology (.iff φ ψ) = true := by
  rw [isTautology_iff]
  simp [Equivalent, Formula.eval]

Axioms used: propext, Quot.soundformal/Lumenary/PropositionalLogic.leanTry it in the Lean web editor

With these in place, particular laws are proved by letting Lean evaluate their truth tables (decide). Here p and q are the two variables of Formula 2.

contrapositive_tableLean 4Proved here from basic factsFormally verified

/-- **Contrapositive.** `p → q` is equivalent to `¬q → ¬p`: the truth-table test passes on all
four rows (computed by `decide`). -/
theorem contrapositive_table : Equivalent (imp p q) (imp (not q) (not p)) := by
  rw [equivalent_iff_tautology]
  decide

Axioms used: propext, Quot.soundformal/Lumenary/PropositionalLogic.leanTry it in the Lean web editor

converse_tableLean 4Proved here from basic factsFormally verified

/-- **The converse is different.** `p → q` and `q → p` are *not* equivalent: they disagree in
the row `p = false`, `q = true`, where `p → q` is (vacuously) true but `q → p` is false. -/
theorem converse_table : ¬ Equivalent (imp p q) (imp q p) := by
  intro h
  have row := h (fun i => if i = 0 then false else true)
  revert row
  decide

Axioms used: propextformal/Lumenary/PropositionalLogic.leanTry it in the Lean web editor

de_morgan_tableLean 4Proved here from basic factsFormally verified

/-- **De Morgan's laws** as truth tables: `¬(p ∧ q) ≡ ¬p ∨ ¬q` and `¬(p ∨ q) ≡ ¬p ∧ ¬q`. -/
theorem de_morgan_table :
    Equivalent (not (and p q)) (or (not p) (not q)) ∧
      Equivalent (not (or p q)) (and (not p) (not q)) := by
  rw [equivalent_iff_tautology, equivalent_iff_tautology]
  decide

Axioms used: propext, Quot.soundformal/Lumenary/PropositionalLogic.leanTry it in the Lean web editor

not_imp_tableLean 4Proved here from basic factsFormally verified

/-- **Negating a conditional.** `¬(p → q) ≡ p ∧ ¬q`: a promise "if p then q" is broken exactly
when p happens and q does not. -/
theorem not_imp_table : Equivalent (not (imp p q)) (and p (not q)) := by
  rw [equivalent_iff_tautology]
  decide

Axioms used: propext, Quot.soundformal/Lumenary/PropositionalLogic.leanTry it in the Lean web editor

argument_formsLean 4Proved here from basic factsFormally verified

/-- **Valid and invalid argument forms.** *Modus ponens* `((p → q) ∧ p) → q` and *modus tollens*
`((p → q) ∧ ¬q) → ¬p` are tautologies; *affirming the consequent* `((p → q) ∧ q) → p` is not. -/
theorem argument_forms :
    isTautology (imp (and (imp p q) p) q) = true ∧
      isTautology (imp (and (imp p q) (not q)) (not p)) = true ∧
      isTautology (imp (and (imp p q) q) p) = false := by
  decide

Axioms used: propextformal/Lumenary/PropositionalLogic.leanTry it in the Lean web editor

Logic in Prop. From $P \to Q$ we can always get $\neg Q \to \neg P$ — the proof is a one-line function. But the way back uses proof by contradiction (by_contra), which relies on the law of excluded middle, $P \vee \neg P$ . Logicians who do not assume that law (constructive mathematics, many type theories) accept the first direction and not, in general, the second. Mathlib's one-line version applies its theorem not_imp_not.

contrapositiveLean 4Proved here from basic factsFormally verified

/-- From `p → q` we get `¬q → ¬p`: if `q` fails, then `p` must fail too, since `p` would give `q`.
This direction is *constructive*: it uses no law of excluded middle. -/
theorem contrapositive {p q : Prop} (h : p → q) : ¬q → ¬p :=
  fun hnq hp => hnq (h hp)

Axioms used: No axiomsformal/Lumenary/PropositionalLogic.leanTry it in the Lean web editor

contrapositive_iffLean 4Proved here from basic factsFormally verified

/-- **The contrapositive law** `(p → q) ↔ (¬q → ¬p)`. The way back, from `¬q → ¬p` to `p → q`,
argues by contradiction: given `p`, if `q` failed we would get `¬p`, which is absurd. That step
uses classical logic (`by_contra`). -/
theorem contrapositive_iff (p q : Prop) : (p → q) ↔ (¬q → ¬p) := by
  constructor
  · exact contrapositive
  · intro h hp
    by_contra hnq
    exact h hnq hp

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/PropositionalLogic.leanTry it in the Lean web editor

contrapositive_iff_libraryLean 4Applies a library theoremFormally verified

/-- The contrapositive law, by Mathlib's `not_imp_not : (¬a → ¬b) ↔ (b → a)`. -/
theorem contrapositive_iff_library (p q : Prop) : (p → q) ↔ (¬q → ¬p) :=
  not_imp_not.symm

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/PropositionalLogic.leanTry it in the Lean web editor

converse_failsLean 4Proved here from basic factsFormally verified

/-- **An implication does not imply its converse.** Take `p` false and `q` true: `p → q` holds
(its hypothesis is false), but `q → p` would turn a proof of `True` into a proof of `False`. -/
theorem converse_fails : ¬ ∀ p q : Prop, (p → q) → (q → p) := by
  intro h
  exact h False True (fun hf => hf.elim) trivial

Axioms used: No axiomsformal/Lumenary/PropositionalLogic.leanTry it in the Lean web editor

The same split happens for De Morgan: "neither $P$ nor $Q$ " is constructive, but to pass from "not both" to "one of them fails" we must decide which one, and Mathlib's not_and_or uses classical logic.

de_morgan_orLean 4Proved here from basic factsFormally verified

/-- **De Morgan** `¬(p ∨ q) ↔ ¬p ∧ ¬q`, proved constructively: "neither p nor q". -/
theorem de_morgan_or (p q : Prop) : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
  ⟨fun h => ⟨fun hp => h (Or.inl hp), fun hq => h (Or.inr hq)⟩,
    fun ⟨hnp, hnq⟩ h => h.elim hnp hnq⟩

Axioms used: No axiomsformal/Lumenary/PropositionalLogic.leanTry it in the Lean web editor

de_morgan_andLean 4Applies a library theoremFormally verified

/-- **De Morgan** `¬(p ∧ q) ↔ ¬p ∨ ¬q`, by Mathlib's `not_and_or`. Going from left to right
needs classical logic: to name *which* of `p`, `q` fails we must decide whether `p` holds. -/
theorem de_morgan_and (p q : Prop) : ¬(p ∧ q) ↔ ¬p ∨ ¬q :=
  not_and_or

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/PropositionalLogic.leanTry it in the Lean web editor

not_imp_iffLean 4Applies a library theoremFormally verified

/-- **Negating a conditional**: `¬(p → q) ↔ p ∧ ¬q`, by core Lean's `Classical.not_imp`. -/
theorem not_imp_iff (p q : Prop) : ¬(p → q) ↔ p ∧ ¬q :=
  Classical.not_imp

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/PropositionalLogic.leanTry it in the Lean web editor

Finally, negating quantified statements (Theorem 4), the prime-number example, and vacuous truth:

not_forall_impLean 4Proved here from basic factsFormally verified

/-- **Negating a quantified conditional**: "not every `x` with `P` has `Q`" means "some `x` has
`P` but not `Q`". It combines `Classical.not_forall` (`¬∀ ↔ ∃¬`) with the negation of a
conditional. -/
theorem not_forall_imp {α : Type*} (P Q : α → Prop) :
    (¬ ∀ x, P x → Q x) ↔ ∃ x, P x ∧ ¬ Q x := by
  rw [Classical.not_forall]
  exact exists_congr fun x => Classical.not_imp

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/PropositionalLogic.leanTry it in the Lean web editor

not_every_prime_oddLean 4Proved here from basic factsFormally verified

/-- "Every prime is odd" is false. By `not_forall_imp`, its negation is "some prime is not odd",
and `2` is a witness. -/
theorem not_every_prime_odd : ¬ ∀ n : ℕ, n.Prime → Odd n := by
  rw [not_forall_imp]
  exact ⟨2, Nat.prime_two, by decide⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/PropositionalLogic.leanTry it in the Lean web editor

vacuous_truthLean 4Proved here from basic factsFormally verified

/-- **Vacuous truth.** "If a natural number is negative, then it equals 17" is *true*: its
hypothesis never holds, so it can never be broken. -/
theorem vacuous_truth : ∀ n : ℕ, n < 0 → n = 17 :=
  fun n h => absurd h (Nat.not_lt_zero n)

Axioms used: No axiomsformal/Lumenary/PropositionalLogic.leanTry it in the Lean web editor

What is formalised: the syntax and truth-table semantics of propositional formulas, the correctness of the truth-table test, every law of this lesson as a truth-table computation, and the same laws for Lean propositions. What is not formalised here: Theorem 5 (disjunctive normal form) for general $n$ — it is checked for $n = 2$ by the Python experiment below.

ComputationC

Truth tables by machine

Truth tables: equivalence, connectives and normal formsPythonExact computationExhaustive finite checkComputationally tested

"""Truth tables by machine: equivalences, the 16 connectives, and completeness.

A propositional formula in n variables has a truth table with 2**n rows, so
whether two formulas are equivalent can be settled by checking every row. This
experiment builds truth tables for the conditional p -> q and its converse,
inverse and contrapositive, checks De Morgan's laws and the negation of a
conditional, and then shows that every one of the 16 possible two-variable
truth tables is the table of some formula built from "not", "and" and "or"
(its disjunctive normal form), and even from NAND alone.

Unlike checking a formula about integers on many examples, checking every row
of a truth table is a complete verification: there are no other cases.

Runs unchanged in the browser (Pyodide) using only the standard library.
"""

from itertools import product

def implies(a, b):
    """The material conditional: false only when a is true and b is false."""
    return (not a) or b

def nand(a, b):
    """NAND: 'not both'."""
    return not (a and b)

def rows(n):
    """All assignments of truth values to n variables, in textbook order
    (all true first, the first variable changing slowest)."""
    if n < 0:
        raise ValueError("n must be non-negative")
    return list(product([True, False], repeat=n))

def table(formula, n):
    """The truth table of ``formula`` (a function of n booleans) as a tuple."""
    return tuple(bool(formula(*row)) for row in rows(n))

def classify(formula, n):
    """'tautology', 'contradiction' or 'contingent'."""
    values = table(formula, n)
    if all(values):
        return "tautology"
    if not any(values):
        return "contradiction"
    return "contingent"

def differing_rows(f, g, n):
    """The rows on which two formulas take different values (empty iff
    the formulas are logically equivalent)."""
    return [row for row in rows(n) if bool(f(*row)) != bool(g(*row))]

def dnf_from_table(values, names=("p", "q")):
    """A formula in disjunctive normal form with the given truth table.

    For each row where the table is true, AND together the literals that
    describe that row; then OR these terms. A table that is never true gets
    the contradiction 'p and not p'."""
    n = len(names)
    terms = []
    for row, value in zip(rows(n), values):
        if value:
            lits = [v if b else "not " + v for v, b in zip(names, row)]
            terms.append("(" + " and ".join(lits) + ")")
    if not terms:
        return f"({names[0]} and not {names[0]})"
    return " or ".join(terms)

def evaluate_dnf(text, assignment):
    """Evaluate a DNF string produced by ``dnf_from_table`` without eval()."""
    for term in text.split(" or "):
        lits = term.strip("()").split(" and ")
        ok = True
        for lit in lits:
            if lit.startswith("not "):
                ok = ok and not assignment[lit[4:]]
            else:
                ok = ok and assignment[lit]
        if ok:
            return True
    return False

def nand_only(values):
    """Build the truth function with this two-variable table using only nand,
    following the DNF: not x = x nand x, x and y = not(x nand y),
    x or y = (not x) nand (not y). Returns a function of (p, q)."""
    def neg(x):
        return nand(x, x)

    def conj(x, y):
        return neg(nand(x, y))

    def disj(x, y):
        return nand(neg(x), neg(y))

    def f(p, q):
        result = conj(p, neg(p))                     # start from "false"
        for (a, b), value in zip(rows(2), values):
            if value:
                lit_p = p if a else neg(p)
                lit_q = q if b else neg(q)
                result = disj(result, conj(lit_p, lit_q))
        return result
    return f

def main():
    tf = {True: "T", False: "F"}
    forms = [
        ("p -> q", lambda p, q: implies(p, q)),
        ("converse q -> p", lambda p, q: implies(q, p)),
        ("inverse ~p -> ~q", lambda p, q: implies(not p, not q)),
        ("contrapositive ~q -> ~p", lambda p, q: implies(not q, not p)),
    ]
    print("p q | " + " | ".join(name for name, _ in forms))
    for p, q in rows(2):
        cells = [tf[f(p, q)].center(len(name)) for name, f in forms]
        print((f"{tf[p]} {tf[q]} | " + " | ".join(cells)).rstrip())
    print()
    cond = forms[0][1]
    for name, f in forms[1:]:
        diff = differing_rows(cond, f, 2)
        shown = ", ".join(tf[a] + tf[b] for a, b in diff)
        verdict = "equivalent" if not diff else f"differs in rows {shown}"
        print(f"p -> q versus {name}: {verdict}")
    checks = [
        ("~(p & q) = ~p | ~q", lambda p, q: (not (p and q)) == ((not p) or (not q))),
        ("~(p | q) = ~p & ~q", lambda p, q: (not (p or q)) == ((not p) and (not q))),
        ("~(p -> q) = p & ~q", lambda p, q: (not implies(p, q)) == (p and not q)),
    ]
    for name, f in checks:
        print(f"{name:22} is a {classify(f, 2)}")
    print()
    tables = list(product([True, False], repeat=4))
    dnf_ok = sum(
        table(lambda p, q, t=t: evaluate_dnf(dnf_from_table(t),
                                             {"p": p, "q": q}), 2) == t
        for t in tables)
    nand_ok = sum(table(nand_only(t), 2) == t for t in tables)
    print(f"Two-variable truth tables: {len(tables)} = 2^(2^2)")
    print(f"  rebuilt from not/and/or (DNF): {dnf_ok} of {len(tables)}")
    print(f"  rebuilt from NAND alone:       {nand_ok} of {len(tables)}")
    print("  e.g. exclusive or: " + dnf_from_table((False, True, True, False)))
    print("Truth tables in n variables: " + ", ".join(
        f"n={n}: {2 ** 2 ** n}" for n in range(1, 5)))
    print()
    print("Epistemic status: every row of every table was checked, so these")
    print("equivalences and constructions are verified completely (assuming")
    print("this short program is correct). For propositional formulas a truth")
    print("table is a proof; the lesson explains why the DNF method works for")
    print("any number of variables, which no finite run can show.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

This is a rare situation in which checking cases is a proof: a two-variable formula has only four rows, and the program checks all of them. The catch is size. A formula with $n$ variables has $2^n$ rows; with $300$ variables that is more than $10^{90}$ rows, far more than could ever be checked. Deciding whether some row makes a formula true — the satisfiability problem, SAT — was the first problem shown to be NP-complete (Stephen Cook, 1971, and independently Leonid Levin, 1973). Whether it can always be solved dramatically faster than by trying all rows is the famous open P versus NP problem; see computational complexity.

Exercises

1. Propositional logic and truth tables

Warm-upHuman

Is the statement “If $7$ is even, then $7$ is divisible by $4$ ” true or false?

Choose one

TrueFalse, because

7

is not divisible by

4

Neither: it is meaningless because

7

is odd

2. Propositional logic and truth tables

Warm-upHuman

Which statement is the contrapositive of “If a shape is a square, then it is a rectangle”?

Choose one

If a shape is not a rectangle, then it is not a square.If a shape is a rectangle, then it is a square.If a shape is not a square, then it is not a rectangle.A shape is a square and it is not a rectangle.

3. Propositional logic and truth tables

CoreHuman

Which statement is the negation of “If it is a public holiday, then the bakery is closed”?

Choose one

It is a public holiday and the bakery is open.If it is a public holiday, then the bakery is open.If it is not a public holiday, then the bakery is open.It is not a public holiday and the bakery is open.

4. Propositional logic and truth tables

CoreHuman

What is the negation of “Amara speaks Hausa and Yoruba”?

Choose one

Amara does not speak Hausa or she does not speak Yoruba.Amara speaks neither Hausa nor Yoruba.Amara speaks exactly one of Hausa and Yoruba.

5. Propositional logic and truth tables

Warm-upHuman

How many rows does the truth table of $(P \wedge Q) \to (R \vee \neg S) \leftrightarrow T$ have?

6. Propositional logic and truth tables

CoreHuman

Which of these formulas are tautologies? (Choose all that apply.)

Choose all that apply

P \vee \neg P

(P \to Q) \to (Q \to P)

\big((P \to Q) \wedge \neg Q\big) \to \neg P

P \to (P \vee Q)

\big((P \to Q) \wedge Q\big) \to P

7. Propositional logic and truth tables

CoreHuman

Each card has a letter on one side and a whole number on the other. You see E, M, 6 and 3. Rule: “If a card has a vowel on one side, then it has an even number on the other.” Which cards must you turn over to check the rule? (Choose all that apply.)

Choose all that apply

EM63

8. Propositional logic and truth tables

CoreHuman

Which statement is the negation of “Every whole number divisible by $4$ is divisible by $8$ ”?

Choose one

Some whole number is divisible by

4

but not by

8

.Every whole number divisible by

4

is not divisible by

8

.Every whole number divisible by

8

is divisible by

4

.No whole number divisible by

8

is divisible by

4

9. Propositional logic and truth tables

CoreFormal

Which Lean statement says that a conditional is equivalent to its contrapositive (for all propositions p and q)?

Choose one

(p → q) ↔ (¬q → ¬p)(p → q) ↔ (q → p)(p → q) ↔ (¬p → ¬q)¬(p → q) ↔ (p ∧ q)

10. Propositional logic and truth tables

StretchComputational

Write is_tautology(f, n), which returns True exactly when the Python function f of n boolean arguments returns True for every combination of arguments. Then write equivalent(f, g, n) using it. (Hint: itertools.product([True, False], repeat=n) lists all rows.)

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

"An implication with a false hypothesis is false." It is true. "If $7$ is even, then $7$ is divisible by $4$ " is a true statement, because its hypothesis is false and so it can never be broken. Such statements are called vacuously true. They matter: "every element of the empty set is even" is true for the same reason.

Misconception

"An implication and its converse say the same thing." "If a number is divisible by $4$ , it is even" is true; its converse "if a number is even, it is divisible by $4$ " is false ( $6$ ). Only the contrapositive is equivalent. Mixing up a statement and its converse is the fallacy of affirming the consequent.

Misconception

"If $P$ then $Q$ means $P$ causes $Q$ ." The mathematical conditional is only about truth values. "If $2 + 2 = 4$ , then the Nile flows through Africa" is true — both parts are true — although neither causes the other. Everyday "if" often carries extra meaning (cause, time, relevance); logicians study other kinds of conditional too, but in mathematics $P \to Q$ means exactly "not ( $P$ and not $Q$ )".

Misconception

"The negation of 'P and Q' is 'not P and not Q'." By De Morgan, $\neg(P \wedge Q) \equiv \neg P \vee \neg Q$ . The negation of "Amara speaks Hausa and Yoruba" is "Amara does not speak Hausa or does not speak Yoruba" — she might speak one of them.

Misconception

"The negation of 'if P then Q' is 'if P then not Q'." The negation is $P \wedge \neg Q$ . "If it rains, the match is cancelled" is refuted by a rainy day on which the match was played — not by another "if" statement.

ViewpointsH

Many ways of seeing

Set theory— truth sets and Venn diagrams

Fix a universe $U$ and properties $P(x)$ , $Q(x)$ with truth sets $A = \{x \in U : P(x)\}$ and $B = \{x \in U : Q(x)\}$ . Then $P \wedge Q$ , $P \vee Q$ and $\neg P$ have truth sets $A \cap B$ , $A \cup B$ and the complement $A^{c}$ . De Morgan's laws become $(A \cap B)^{c} = A^{c} \cup B^{c}$ and $(A \cup B)^{c} = A^{c} \cap B^{c}$ . And "for every $x$ , $P(x) \to Q(x)$ " says exactly that $A \subseteq B$ : the conditional is the logical form of the subset relation, which is why it is false only on $A \setminus B$ . See sets.

Algebra— logic as arithmetic modulo 2

Write $1$ for true and $0$ for false, and compute modulo $2$ (so $1 + 1 = 0$ ). Then $P \wedge Q = PQ$ , $\neg P = 1 + P$ , $P \oplus Q = P + Q$ , $P \vee Q = P + Q + PQ$ and $P \to Q = 1 + P + PQ$ . Every truth table is the table of a polynomial in which no variable appears squared (because $P^2 = P$ for $P \in \{0, 1\}$ ) — its algebraic normal form, studied by Ivan Zhegalkin in 1927 — and a formula is a tautology exactly when its polynomial is the constant $1$ . George Boole's original insight was that logic could be done by algebra; today $\{0, 1\}$ with these operations is the field $\mathbb{F}_2$ , the arithmetic of computers.

Geometry— rows are the corners of a cube

The $2^n$ rows of a truth table are the corners of an $n$ -dimensional cube $\{0, 1\}^n$ : for $n = 3$ , an ordinary cube with corners such as $(1, 0, 1)$ . A formula is just a choice of which corners are "true". A literal such as $\neg P_2$ picks out a face (half the corners), a conjunction of literals picks out a smaller sub-cube, and a formula in disjunctive normal form covers the true corners by sub-cubes. Simplifying a formula means covering the same corners with fewer, larger sub-cubes — which is exactly what the Karnaugh maps used by circuit designers (Maurice Karnaugh, 1953) do, by unfolding the cube flat. Two rows differing in one variable are neighbouring corners joined by an edge.

Computation— switches, circuits and NAND

In 1937 Claude Shannon showed in his master's thesis that circuits of electrical switches compute exactly these truth functions: switches in series behave like $\wedge$ , in parallel like $\vee$ . Every chip in a phone is a vast propositional formula. The computer experiment above checks that the single connective NAND, $\neg(P \wedge Q)$ , can build every truth table — which is why chips can be made from millions of copies of one kind of gate. Henry Sheffer published this property of NAND in 1913; Charles Sanders Peirce had noticed the same for NOR decades earlier in unpublished work.

Logic— truth versus proof

There are two ways to establish a law such as $P \to Q \equiv \neg Q \to \neg P$ : compute its truth table, or derive it with rules of inference such as modus ponens. For propositional logic the two agree — every tautology can be derived, and only tautologies can (a completeness theorem, proved by Emil Post in 1921). For logics with quantifiers the story is subtler and deeper; see first-order logic. And as the Lean section shows, if one does not assume excluded middle, some classical tautologies stop being derivable — the starting point of constructive logic and of type theory.

History & global context

History and global context

Ancient Greece. Aristotle (4th century BCE) analysed arguments built from terms ("all A are B"). The Stoic logicians, above all Chrysippus of Soli (3rd century BCE), developed a logic of whole propositions joined by "if", "and" and "or", including the forms we call modus ponens and modus tollens. Philo of Megara proposed reading "if … then" as false only when the first part is true and the second false — our conditional. The debate with his teacher Diodorus Cronus over which conditionals are true was so famous that, as Sextus Empiricus reports, the poet Callimachus joked that even the crows on the rooftops cawed about it.
India. The Nyāya school and later Buddhist logicians such as Dignāga (5th–6th century) and Dharmakīrti (7th century) built detailed theories of valid inference (anumāna), in a framework quite different from the Greek one.
The Islamic world. Ibn Sīnā (Avicenna, c. 980–1037) developed a theory of conditional and disjunctive propositions and the arguments built from them, which was studied and extended by later logicians writing in Arabic and Persian.
Algebra of logic. In 1847 George Boole published The Mathematical Analysis of Logic and Augustus De Morgan his Formal Logic; the laws now named after De Morgan were known in some form to medieval logicians such as William of Ockham. Gottlob Frege's Begriffsschrift (1879) gave the first fully formal system of logic with quantifiers.
Truth tables in their modern form appear in the work of Ludwig Wittgenstein and Emil Post (both 1921), with earlier anticipations by Charles Sanders Peirce. Post also proved the completeness of propositional logic.
Computation. Claude Shannon (1937) connected logic to switching circuits; Stephen Cook (1971) and Leonid Levin (1973) showed that satisfiability is NP-complete.

Four cards

A promise and when it is broken

Connectives and truth tables

Worked examples

Explore: truth tables that build themselves

The laws, and why they hold

Truth tables and logic in Lean

Truth tables by machine

Exercises

Common misconceptions

Many ways of seeing

History and global context

Further reading