Ctrl+K

Lecture 3 — Propositional logic proofs

Lecture 3 — Propositional logic proofs#

Abstract

We learn to prove — and to see a proof as a program. Natural deduction for propositional logic, the BHK interpretation, and the Curry–Howard reading of the connectives: implication is a function, conjunction a product, disjunction a sum, negation a function into the empty type. We do it hands-on through Emily Riehl’s Lean game A Reintroduction to Proofs, mapping each level to an inference rule, and we mark precisely where intuitionistic reasoning ends and classical logic begins.

Learning objectives#

  • State Gentzen’s introduction and elimination rules for \(\To, \land, \lor, \bot\) (and derived \(\neg, \top\)), and read a rule as premises-over-conclusion with hypothesis discharge.

  • Explain the Brouwer–Heyting–Kolmogorov (BHK) meaning of each connective and use it to judge whether a formula is intuitionistically valid.

  • Articulate the Curry–Howard dictionary — \(\To\) a function type, \(\land\) a product, \(\lor\) a sum, \(\bot\) the empty type, \(\neg A = A\To\bot\) — and read a proof term as the program that witnesses a proposition.

  • Map each Lean tactic (intro, exact, apply, constructor, rcases/obtain, left/right, exfalso, by_contra) to the exact rule or term-former it performs.

  • Produce sorry-free proofs of representative theorems: \(\land\)/\(\lor\)-symmetry, currying, \(A\To\neg\neg A\), \(\neg\neg\neg A\To\neg A\), and a De Morgan law.

  • Identify \(A\lor\neg A\), \(\neg\neg A\To A\) and Peirce’s law as the classical boundary, and justify exactly when by_contra is genuinely required.

Why this matters#

A first logic course usually decides propositional formulas with truth tables: a tautology is a formula true under every valuation, and that is that. A proof assistant cannot work this way. Its kernel does not evaluate a table; it checks a derivation — a syntactic object built from a fixed stock of inference rules. So before Lean can help us with real mathematics we must answer a deceptively simple question, the one that opens this lecture: what, precisely, is a proof?

The answer that makes machine-checked mathematics possible is that a proof is a construction, and a construction is a typed program. This is the Curry–Howard correspondence, glimpsed already in Lecture 2 as the slogan proofs = programs. This lecture turns the slogan into a working dictionary: every connective becomes a type former, every inference rule becomes a term former, and every Lean tactic becomes a recipe that fills a hole in a proof term. The same moves you learn here on toy propositions are, unchanged, the moves that build the hundred kernel-checked theorems of the Lecture 6 research formalization.

Natural deduction for propositional logic#

Gentzen’s calculus (1934/35) gives each connective introduction rules (how to prove it) and elimination rules (how to use it). A derivation is a finite tree whose leaves are assumptions and whose internal nodes are rule instances; the formula at the root is the conclusion. We write a rule as premises over conclusion.

Implication is the subtle one, because its introduction discharges a hypothesis. The bracket \([A]\) marks an assumption that is “used up” — closed off — by the rule below it:

\[\begin{split} \frac{\begin{array}{c}[A]\\ \vdots\\ B\end{array}}{A\To B}\;{\To}I \qquad\qquad \frac{A\To B \qquad A}{B}\;{\To}E \end{split}\]

The elimination rule \({\To}E\) is modus ponens. Conjunction and disjunction follow the same premises-over-conclusion pattern:

\[ \frac{A \qquad B}{A\land B}\;{\land}I \qquad \frac{A\land B}{A}\;{\land}E_1 \qquad \frac{A\land B}{B}\;{\land}E_2 \]
\[\begin{split} \frac{A}{A\lor B}\;{\lor}I_1 \qquad \frac{B}{A\lor B}\;{\lor}I_2 \qquad \frac{A\lor B \qquad \begin{array}{c}[A]\\ \vdots\\ C\end{array} \qquad \begin{array}{c}[B]\\ \vdots\\ C\end{array}}{C}\;{\lor}E \end{split}\]

Disjunction elimination is case analysis: to use \(A\lor B\) toward a goal \(C\) you must handle both possibilities, and each case may discharge its own assumption. Falsity has an elimination but, tellingly, no introduction — that absence is the whole point:

\[ \frac{\bot}{C}\;{\bot}E \quad(\text{ex falso quodlibet}). \]

Negation is derived: \(\neg A := A\To\bot\), so the rules for \(\neg\) are exactly \({\To}I\) and \({\To}E\) specialized to conclusion \(\bot\). Likewise \(\top := \bot\To\bot\) (or a primitive with a single trivial proof).

Harmony and normalization

Introduction and elimination are in harmony: an introduction immediately followed by the matching elimination is a detour that can be removed. For conjunction, \({\land}E_1\) applied to \({\land}I\) of \(A\) and \(B\) simply returns the \(A\) you started with. Prawitz proved that removing all such detours normalizes a derivation, and — the punchline of the lecture — under Curry–Howard detour removal is exactly \(\beta\)-reduction. Simplifying a proof is running a program.

BHK: what a proof is#

The Brouwer–Heyting–Kolmogorov interpretation reads each connective as a recipe for constructions, not as a truth value. This is the conceptual pivot: “proof” becomes a first-class object, which is exactly why it can later be a Lean term.

  • A proof of \(A\land B\) is a pair \(\langle a,b\rangle\): a proof \(a\) of \(A\) together with a proof \(b\) of \(B\).

  • A proof of \(A\lor B\) is a tagged proof \((i,p)\): a bit \(i\in\{0,1\}\) choosing a disjunct, plus a proof \(p\) of that disjunct.

  • A proof of \(A\To B\) is a function turning any proof of \(A\) into a proof of \(B\).

  • There is no proof of \(\bot\).

  • A proof of \(\neg A = A\To\bot\) is a function turning any putative proof of \(A\) into a proof of \(\bot\).

Two clauses do the real work. The disjunction clause forces you to know which side holds: to assert \(A\lor B\) constructively you must exhibit the tag. That is why there is, in general, no construction witnessing \(A\lor\neg A\) — you would need to actually decide \(A\). And the negation clause explains a common stumble: \(\neg A\) is not “the truth value false”; it is a map \(A\to\bot\), something you apply, never something you evaluate.

Curry–Howard for the connectives#

BHK’s “constructions” are literally typed terms. This extends the dictionary of Lecture 2 (and of the course’s 08_curry_howard notebook) from \(\To\) and \(\land\) to \(\lor\), \(\bot\) and \(\neg\):

Logic

Type theory

Introduce

Eliminate

\(A \To B\)

function \(A \to B\)

\(\lam\)-abstraction fun a => …

application \(f\,a\)

\(A \land B\)

product \(A \times B\)

pairing \(\langle a,b\rangle\)

projections \(\pi_1,\pi_2\)

\(A \lor B\)

sum \(A + B\)

injections \(\mathsf{inl},\mathsf{inr}\)

case analysis

\(\bot\)

empty type \(\varnothing\)

— (no intro)

\(\mathsf{absurd}\) / False.elim

\(\neg A\)

\(A \to \varnothing\)

assume \(A\), derive \(\bot\)

apply to a proof of \(A\)

\(\top\)

unit type \(\mathbf 1\)

the sole point trivial

—

Provability becomes inhabitation: \(A\) is provable iff the type \(A\) has a closed term. In Lean, And is a structure (product), Or is an inductive type with two constructors Or.inl/Or.inr (sum), False is the inductive type with no constructors, and True has one.

Theorem (Howard 1969/1980; Prawitz)

Closed normal terms of the simply-typed \(\lam\)-calculus with products, sums and the empty type — normal for \(\beta\) together with the permutative (commuting) conversions required for \(\lor\)-elimination and \(\bot\)-elimination — are in bijection with Prawitz-normal natural-deduction derivations of intuitionistic propositional logic, and this bijection carries detour reduction (\(\beta\) together with permutative conversions) to proof normalization.

In particular the calculus is strongly normalizing, so there is no closed term of type \(\bot\) — the proof system is consistent.

Worked example 1 — conjunction is commutative#

Here is the full derivation of \(A\land B\To B\land A\). We open the hypothesis \(A\land B\), project twice, repackage, then discharge:

\[ \frac{\dfrac{\dfrac{[A\land B]}{B}\;{\land}E_2 \qquad \dfrac{[A\land B]}{A}\;{\land}E_1}{B\land A}\;{\land}I}{(A\land B)\To(B\land A)}\;{\To}I \]

Read off the proof term by naming the discharged hypothesis \(h\) and the projections \(h.1,h.2\): the program is \(\lam h.\,\langle h.2,\,h.1\rangle\). In Lean, term mode and tactic mode build the same kernel object:

-- term mode: the proof IS the program
theorem and_comm' {P Q : Prop} : P ∧ Q → Q ∧ P :=
  fun h => ⟨h.2, h.1⟩

-- tactic mode: a recipe that fills the same hole
theorem and_comm'' {P Q : Prop} : P ∧ Q → Q ∧ P := by
  intro h            -- goal Q ∧ P, with h : P ∧ Q      (→I / λ)
  obtain ⟨p, q⟩ := h  -- destructure the pair            (∧E)
  exact ⟨q, p⟩        -- build the swapped pair           (∧I)

The disjunction analogue is the same shape with case analysis instead of projection: from h : P ∨ Q, rcases h with p | q splits into two goals, closed by Or.inr p and Or.inl q respectively.

Worked example 2 — currying is the exponential adjunction#

The two ways of taking two hypotheses are interderivable:

\[ (A\land B\To C)\;\;\cong\;\;(A\To B\To C). \]

Left to right (curry) and right to left (uncurry) are one-line programs — and they are exactly the product/exponential adjunction \(\mathrm{Hom}(A\times B, C)\cong\mathrm{Hom}(A, C^{B})\) read as terms:

theorem curry   {P Q R : Prop} : (P ∧ Q → R) → (P → Q → R) :=
  fun f p q => f ⟨p, q⟩
theorem uncurry {P Q R : Prop} : (P → Q → R) → (P ∧ Q → R) :=
  fun g h => g h.1 h.2

Note that \(\To\) is right-associative and curried: \(P\To Q\To R\) means \(P\To(Q\To R)\) and eats its arguments one at a time — the K/S combinator shape from Lecture 2.

Worked example 3 — negation, constructively#

Three theorems about \(\neg\) that people wrongly assume need classical logic. All are pure constructions. Recall \(\neg\neg A = (A\To\bot)\To\bot\).

\[ A\To\neg\neg A,\qquad \neg(A\land\neg A),\qquad \neg\neg\neg A\To\neg A. \]
theorem dni  {P : Prop} : P → ¬¬P            := fun p k => k p
theorem noncontra {P : Prop} : ¬(P ∧ ¬P)     := fun h => h.2 h.1
theorem tne  {P : Prop} : ¬¬¬P → ¬P          := fun h p => h (fun k => k p)

Trace dni: given p : P we must produce a term of ¬¬P = (P → False) → False, i.e. a function k : P → False ↦ (k p : False) — literally apply the continuation to the proof. The converse \(\neg\neg A\To A\) is the one that is not available here; it is double-negation elimination, and it is the classical boundary in disguise (see below).

Run it — Algorithm W rediscovers double negation

Strip the types away and dni is the untyped term \(\lam p\,k.\,k\,p\); ask the lab for its principal type:

  • ch term \p k. k p — runs Algorithm W and reports \(\alpha\To(\alpha\To\beta)\To\beta\); read the result atom \(\beta\) as \(\bot\) and this is \(A\To\neg\neg A\).

  • ch term \h p. h (\k. k p) — the same game for tne.

The Curry-style moral: the program comes first, and the theorem it proves is its most general type.

Worked example 4 — a De Morgan law, and its classical cousin#

One direction-pair is fully constructive; one implication is genuinely classical.

\[ \neg(A\lor B)\;\Longleftrightarrow\;(\neg A\land\neg B)\qquad(\text{intuitionistic, both directions}) \]
\[ \neg(A\land B)\;\To\;(\neg A\lor\neg B)\qquad(\text{classical only}). \]

The constructive equivalence, as a single proof term, uses only \(\lor\)-elimination and function application:

theorem deMorgan_or {P Q : Prop} : ¬(P ∨ Q) ↔ (¬P ∧ ¬Q) :=
  ⟨fun h => ⟨fun p => h (Or.inl p), fun q => h (Or.inr q)⟩,
   fun ⟨np, nq⟩ h => h.elim np nq⟩

The forward map takes h : ¬(P ∨ Q) and builds each conjunct by feeding it an injection; the backward map takes ⟨np, nq⟩ and an alleged h : P ∨ Q and case-splits. The other De Morgan direction, \(\neg(A\land B)\To(\neg A\lor\neg B)\), cannot be a term: to output the sum you would have to pick a tag, i.e. decide which conjunct fails, and BHK forbids that without more information. It needs excluded middle.

Lean tactics as proof-term construction#

The bilingual claim of the lecture: every tactic is a recipe that builds a piece of the proof term. A tactic transforms the goal state (a context of hypotheses \(\Gamma\) and a target \(\vdash A\)) and appends to the underlying term. Here is the dictionary that the whole live session runs on.

Tactic

Natural-deduction rule

Term action

Effect on goal

intro h

\({\To}I\) (discharge)

\(\lam h.\,?\)

\(A\To B\;\leadsto\;B\) with h : A

exact e

assumption / close

plug in \(e\)

closes the goal

apply f

\({\To}E\) backward

build \(f\,?\)

\(Q\leadsto P\) when f : P → Q

constructor / ⟨a,b⟩

\({\land}I\)

pair

\(A\land B\leadsto A,\;B\)

rcases/obtain h with …

\({\land}E\), \({\lor}E\), \({\bot}E\)

project / match

destructure (0, 1 or 2 subgoals)

left / right

\({\lor}I_1\) / \({\lor}I_2\)

\(\mathsf{inl}\) / \(\mathsf{inr}\)

\(A\lor B\leadsto A\) (or \(B\))

exfalso

\({\bot}E\)

False.elim ?

replaces any goal by \(\bot\)

by_contra h

classical (¬¬-elim)

Classical.byContradiction

goal \(A\leadsto\bot\) with h : ¬A

The single crucial warning: by_contra is not a natural-deduction rule. It is the classical axiom \(\neg\neg A\To A\) wearing a tactic’s clothes. Everything above it in the table is constructive; only the last row leaves the intuitionistic fragment. And do not confuse it with exfalso: exfalso is \({\bot}E\) (“from \(\bot\), anything”), always valid; by_contra is “assume \(\neg\)goal, derive \(\bot\)”, which is where classical logic enters.

Run it — drive the tactics yourself

The Lambda Lab has an interactive proof builder that speaks exactly the implication rows of this table:

  • prove (P -> Q) -> P -> Q — close the goal with intro, apply and exact (hint nudges you when stuck, undo backtracks).

On qed the lab extracts the λ-term you just built and infers its principal type — the “term action” column of the table made visible: every tactic appended exactly one node to the program.

Run it — see a tactic fill a hole

Copy the four worked theorems above into the game’s editor or any Lean playground and watch the goal state change line by line. Or feel the “proof = program” identity in the untyped world of the Lambda Lab:

And modus ponens is application, which you can watch by reducing the S-combinator proof term \(\lam f\,g\,x.\,f\,x\,(g\,x)\) on concrete “proofs”. The same statement is proved in all four provers in the artifacts directory (Lean, Agda, Rocq, Mizar).

The game, world by world#

Riehl’s A Reintroduction to Proofs is a Lean 4 game (17 worlds, MIT-licensed, built for a Fall-2025 first-year seminar at Johns Hopkins, pinned to Lean v4.23.0) that runs entirely in the browser on the Lean Game Server. Its design is a gift to this lecture: it front-loads the constructive core and quarantines classical logic in a single world reached only at the end. It even studies the Empty type before negation, so that \(\neg P\) arrives as an already-understood \(P\To\bot\) rather than a mysterious primitive.

For a propositional-logic session, play this dependency chain (deferring the quantifier, arithmetic and equality worlds to later lectures):

  • TypeWorld — p : P means “\(p\) is a proof of \(P\)”; meet exact, assumption.

  • FunctionWorld / ImplicationWorld — \(\To\) as a function; the identity proof fun p => p, composition, and intro/apply/exact.

  • ProductWorld / ConjunctionWorld — constructor, ⟨_,_⟩, projections; \(\land\)-symmetry and associativity.

  • CoproductWorld / DisjunctionWorld — left/right, obtain/rcases; \(\lor\)-symmetry.

  • EmptyWorld — Empty → A by intro p; cases p (elimination with zero constructors).

  • NegationWorld — \(\neg P := P\To\bot\), ex falso, and the three constructive negation theorems of Worked Example 3.

  • ClassicalWorld — and only here: by_contra, Classical.em.

Run it — play the constructive core

The game is one click, nothing to install:

  • A Reintroduction to Proofs — clear TypeWorld → FunctionWorld → ImplicationWorld, then Conjunction/DisjunctionWorld, then Empty/NegationWorld — without touching ClassicalWorld.

After each world, return to the tactic table above and name the row you just used. It runs in the browser on the same engine as the Natural Number Game.

The classical boundary#

Everything so far lived in the intuitionistic fragment. The following are equivalent over intuitionistic propositional logic — adding any one recovers full classical logic:

\[ \text{excluded middle } A\lor\neg A,\qquad \text{double-negation elim } \neg\neg A\To A,\qquad \text{Peirce's law } ((A\To B)\To A)\To A. \]

None of the three is constructively provable, precisely because each would let you manufacture a disjunction tag (or a witness) out of thin air. Lean keeps them out of its computational core and offers them as the axiom Classical.em : ∀ P, P ∨ ¬P, which by_contra invokes.

Worked example 5 — Peirce’s law needs by_contra#

\[ ((A\To B)\To A)\To A. \]

Classically it is a two-move proof; constructively it has no proof term at all.

theorem peirce {P Q : Prop} : ((P → Q) → P) → P := by
  intro h
  by_contra hnp                     -- hnp : ¬P, goal : False
  exact hnp (h (fun p => absurd p hnp))

Trace it: hnp : ¬P; from it we can prove anything, so fun p => absurd p hnp : P → Q; feeding that to h yields P; feeding that to hnp yields False. Every step but by_contra is constructive — the classical content is isolated in exactly one move.

Contrast this with the honest fact that no tactic-free, fun-only term of that type exists:

Theorem (no intuitionistic witness)

There is no closed simply-typed \(\lam\)-term of type \(((A\To B)\To A)\To A\) for atomic \(A\neq B\).

Sketch: by strong normalization it suffices to inspect \(\beta\)-normal, \(\eta\)-long inhabitants. Such a term must begin \(\lam h.\,t\) with \(h:(A\To B)\To A\) and \(t:A\); the only way to reach an \(A\) is \(h\,u\) with \(u:A\To B\), i.e. \(u=\lam a.\,s\) with \(a:A,\ s:B\); but \(B\) is a fresh atom with no closed inhabitant and nothing in context produces one — the search loops with no base case. Hence Peirce’s law is not intuitionistically derivable.

This is what the Curry–Howard lab reports: ch type '((P -> Q) -> P) -> P' answers not inhabited in intuitionistic STLC. Feel the sketch’s dead end yourself with ch build '((P -> Q) -> P) -> P': after intro h, apply h, intro p you face the goal Q with only proofs of P in scope — the search loops with no base case, exactly as the theorem predicts. The classical proof and the (nonexistent) constructive one are different objects, and the gap is measured exactly:

Theorem (Glivenko, 1929)

For a propositional formula \(A\): \(\;\proves_c A\;\) iff \(\;\proves_i \neg\neg A\). Classical propositional provability embeds into intuitionistic provability under double negation. Everything classical is, quite literally, a double negation away — which is why double-negation translations work and why by_contra succeeds exactly when a \(\neg\neg\)-shifted goal is constructive.

The pedagogical cost to state plainly: a classical existence proof by by_contra shows that a counterexample cannot exist without ever handing you the object. When you later want the witness — a root, a bound, a construction — you must stay inside the constructive fragment.

Common pitfalls#

  • Reading \(\neg P\) as a truth value. \(\neg P\) is the function type \(P\To\bot\): something you apply to a proof of \(P\) to get \(\bot\), not something you “evaluate to false”.

  • Thinking \(\lor\)-elimination tells you which disjunct holds. From h : P ∨ Q you must handle both cases (rcases h with p | q); constructively you never learn the tag.

  • Assuming \(A\lor\neg A\), \(\neg\neg A\To A\) and Peirce’s law are “obviously provable”. They are exactly the axioms the game quarantines in ClassicalWorld; the constructive core deliberately lacks them.

  • Reaching for by_contra reflexively. It is a classical move. Many goals — \(A\To\neg\neg A\), \(\neg(A\land\neg A)\), both directions of \(\neg(A\lor B)\Leftrightarrow\neg A\land\neg B\) — have direct constructive proofs, and by_contra merely hides that content.

  • Confusing exfalso with by_contra. exfalso is \({\bot}E\) (always valid); by_contra assumes the negation of the goal (classical). Different rules that both mention False.

  • Direction confusion among tactics. constructor/⟨_,_⟩ builds a conjunction (\({\land}I\)) while rcases/obtain uses one (\({\land}E\)); intro moves a hypothesis in (forward) while apply reasons backward through modus ponens.

  • Treating term mode and tactic mode as different logics. exact ⟨p, q⟩ and constructor invoke the same rule \({\land}I\) and build the same kernel term.

  • Misparsing \(P\To Q\To R\). Implication is right-associative and curried: it means \(P\To(Q\To R)\).

  • Equating a truth-table check with a proof. A formula can be classically valid yet have no intuitionistic derivation and no \(\lam\)-term witness; Glivenko’s theorem measures precisely that gap.

Exercises#

  1. (Pen & paper.) Draw the full natural-deduction derivation of \(\lor\)-symmetry \(A\lor B\To B\lor A\), marking every discharged assumption. Then read off its proof term.

  2. (Lab / Lean.) Prove \(\land\)-symmetry \(P\land Q\To Q\land P\) and \(\lor\)-symmetry \(P\lor Q\To Q\lor P\) in the game (ConjunctionWorld and DisjunctionWorld) using intro, obtain/rcases, left/right, exact. Rewrite each as a single term-mode fun … => ….

  3. (Lean.) Give constructive proof terms for \(P\To\neg\neg P\) and \(\neg\neg\neg P\To\neg P\), then try and fail to prove \(\neg\neg P\To P\) without by_contra. Explain the failure via BHK.

  4. (Lean.) Prove both directions of \(\neg(P\lor Q)\Leftrightarrow(\neg P\land\neg Q)\) constructively, and the one-way \((\neg P\lor\neg Q)\To\neg(P\land Q)\). Which De Morgan implication is missing, and why?

  5. (Lab.) In the Lambda Lab, evaluate reduce FST (PAIR a b) and reduce SND (PAIR a b), and explain, in one sentence each, which inference rule each reduction realizes under Curry–Howard.

  6. (Lean, hard.) Prove Peirce’s law \(((P\To Q)\To P)\To P\) using by_contra. Then argue, in prose, why no tactic-free fun-only term of this type exists (use the normal-form sketch above).

  7. (Pen & paper, hard.) Using Glivenko’s theorem, show that \(\neg\neg(A\lor\neg A)\) is intuitionistically provable even though \(A\lor\neg A\) is not. Exhibit a proof term for \(\neg\neg(A\lor\neg A)\).

  8. (Lean, hard.) In ClassicalWorld, prove the four-way case exhaustion \((P\land Q)\lor(P\land\neg Q)\lor(\neg P\land Q)\lor(\neg P\land\neg Q)\) from Classical.em P and Classical.em Q. Identify the single place where classical logic is unavoidable.

References#

Contents