← Back to System Internals

A Natural Deduction Proof System

Gries’ second style of formal reasoning — deriving new facts line by line from premises using named inference rules, the way a working mathematician actually argues, rather than rewriting one formula into another with equivalence laws.

By this point you can manipulate propositions with the algebra of equivalence — De Morgan, distribution, absorption — rewriting a formula step by step until it collapses to T. That is elegant for boolean simplification, but it is not how anyone proves “if the input is sorted then binary search returns the right index.” For implications and case analysis you want to reason forward from assumptions: suppose the antecedent, grind out consequences, arrive at the conclusion. That is natural deduction, and it is the workhorse for the implication proof obligations that program correctness throws at you.

Two styles of proof

Gries develops two complete, sound systems for propositional logic. They reach exactly the same set of theorems; they differ entirely in how a proof is written down.

# Prove:  P ∧ (P ⇒ Q)  ⇒  Q
# Rewrite one formula until it is T.
   P ∧ (P ⇒ Q)  ⇒  Q
# implication as disjunction
≡ ¬(P ∧ (¬P ∨ Q)) ∨ Q
# distribute, De Morgan, simplify
≡ ¬(P ∧ Q) ∨ Q
≡ ¬P ∨ ¬Q ∨ Q
≡ ¬P ∨ T
≡ T          # a theorem

# Prove:  P, P ⇒ Q  ⊢  Q
# Derive new LINES from premises.
1  P              premise
2  P ⇒ Q          premise
3  Q              ⇒-E on 1, 2
# Q is derived → done. This is how a
# mathematician writes it: modus ponens.

The left column treats a proof as a chain of equivalences massaging a single expression toward T. The right column treats a proof as a sequence of assertions, each one either given or squeezed out of earlier ones by a rule of inference. The second style scales far better to hypothetical reasoning (“assume this, then…”) and to breaking a goal into cases — the two moves that dominate real proofs.

The format of a proof

A natural deduction proof is a numbered sequence of lines. Each line holds one proposition together with a justification: either it is a premise (something given) or an assumption (something temporarily supposed), or it is derived from one or more earlier lines by a named inference rule. The proposition on the last line is the goal — when it appears, the proof is complete.

To prove that premises H1, …, Hn yield conclusion C — written H1, …, Hn ⊢ C — you list the premises, then extend the list one justified line at a time until C shows up. Here is a small worked proof that P ∧ Q and Q ⇒ R together give R ∧ P:

# Goal:  P ∧ Q,  Q ⇒ R   ⊢   R ∧ P

  line   proposition        justification
  ────   ───────────        ───────────────────────
   1     P ∧ Q             premise
   2     Q ⇒ R             premise
   3     P                 ∧-E on 1        # left conjunct
   4     Q                 ∧-E on 1        # right conjunct
   5     R                 ⇒-E on 2, 4     # modus ponens
   6     R ∧ P             ∧-I on 5, 3     # goal reached

Read it top to bottom: nothing on any line is unjustified. Lines 1–2 are the givens; 3–4 take the conjunction apart; 5 fires modus ponens; 6 reassembles the goal. Every step cites the earlier line numbers it depends on and the rule that licenses it. This bookkeeping is exactly what makes the proof checkable — a reader (or a machine) can verify each line in isolation.

Inference rules

The engine of the system is a fixed, small set of inference rules. They come in matched pairs, one per connective: an introduction rule that tells you how to build a formula with that connective, and an elimination rule that tells you how to use one you already have. Above each line is what you must already have; below is what you may then write.

Two of these carry more weight than the rest. Proof by cases (∨-E) is how you reason about a disjunctive fact you cannot pin down — you show the same conclusion in every case. Assumption discharge (⇒-I) is how you prove an implication at all: you cannot prove P ⇒ Q by knowing P is true, because it may not be; instead you temporarily suppose it, work forward, and record that the resulting Q depended on that supposition.

Assumptions and their scope

An assumption is not a free fact — it is a supposition that lives inside a subproof, drawn as an indented box. Everything you derive inside the box may lean on the assumption; nothing outside the box may. When you close the box with ⇒-I, you discharge the assumption: the box collapses to a single implication assumption ⇒ last-line, which is now usable at the outer level. This scoping is what keeps ND honest — a temporary supposition can never leak out and be mistaken for a proven fact.

The classic first example is P ⇒ (Q ⇒ P) — provable from no premises at all, using nested boxes:

# Goal:   ⊢   P ⇒ (Q ⇒ P)

  1  ┌─ P                assume  (outer box, scope of P)
  2  │  ┌─ Q             assume  (inner box, scope of Q)
  3  │  │   P            reiterate line 1 — P is in scope here
  4  │  └─ Q ⇒ P        ⇒-I: discharge Q (from 2–3)
  5  └─ P ⇒ (Q ⇒ P)    ⇒-I: discharge P (from 1–4)
# Both assumptions discharged → the conclusion
# depends on nothing. It is a tautology.

Note how P from line 1 is legitimately reused at line 3: line 3 sits inside the outer box, so P is still in scope. Had line 1’s box already closed, citing it would be an error.

A more useful example is the transitivity of implication, (P ⇒ Q) ∧ (Q ⇒ R)  ⊢  (P ⇒ R) — the shape you meet constantly when chaining program steps:

# Goal:  (P ⇒ Q) ∧ (Q ⇒ R)   ⊢   P ⇒ R

  1     (P ⇒ Q) ∧ (Q ⇒ R)   premise
  2     P ⇒ Q                 ∧-E on 1
  3     Q ⇒ R                 ∧-E on 1
  4  ┌─ P                     assume  (scope of P opens)
  5  │   Q                    ⇒-E on 2, 4   (modus ponens)
  6  │   R                    ⇒-E on 3, 5   (modus ponens)
  7  └─ P ⇒ R                 ⇒-I: discharge P (from 4–6)
# Line 7 no longer depends on the assumption;
# it depends only on premise 1.  ∎

Inside the box we happily use P as if true (lines 5–6). The instant we close the box at line 7, that usage is sealed inside an implication and the assumption is gone. This assume-work-discharge rhythm is the single most important pattern in the whole system.

The Deduction Theorem

Why is the assume-and-discharge move legitimate? Because of a metatheorem that connects derivation from an extra premise to a derived implication:

In words: proving Q with P added to your premises is exactly as good as proving the implication P ⇒ Q without it. The two are interderivable. That equivalence is precisely what ⇒-I encodes as a mechanical rule — opening a box adds P to your working premises, and closing it trades the box for P ⇒ Q at the outer level.

The payoff is enormous: it means you never have to reason directly about an implication as an opaque object. You reduce proving P ⇒ Q to the far easier task of assuming P and hunting for Q. The theorem guarantees the two are the same, so the shortcut is sound. Every subproof box in the previous section is the Deduction Theorem applied once.

Soundness & when to use which style

Both proof systems are sound: every rule preserves truth, so anything you derive is genuinely a logical consequence of the premises (and, for ND, the system is also complete — every valid consequence has a proof). Soundness is what lets you trust a mechanical, line-by-line check as a real guarantee of correctness. The choice between the styles is therefore about ergonomics, not validity.

For program proofs this matters concretely. Almost every verification condition you generate has the form of an implication — most often P ∧ B ⇒ wp(S, P), the obligation that a loop body preserves its invariant, or P ∧ ¬B ⇒ R, that exit re-establishes the postcondition. ND handles these cleanly: assume the antecedent (the invariant and the guard), then derive the consequent step by step. The equivalence style, by contrast, would force you to flatten the whole implication into a single formula and grind it to T — possible, but painful the moment the predicates involve real arithmetic or arrays.

Summary