Natural Deduction

Proof rules, proof trees, and classic derivations

Natural Deduction

Natural deduction builds proofs as trees from a few rules, one pair for each connective. Browse the rules, then watch real proofs grow step by step.

Proof Rule Reference

Click a rule card to see what it needs and what it gives you. Each connective has an introduction rule (how to prove it) and an elimination rule (how to use it).

→IConditional Proof[A] ... BA → BAssume A, derive B, discharge assumpti...→EModus PonensA → BABFrom implication and its antecedent, g...∧IConjunction IntroABA ∧ BCombine two truths into one conjunction.∧EConjunction ElimA ∧ BA (or B)Extract either component from a conjun...∨IDisjunction IntroAA ∨ BWeaken a truth to a disjunction.∨ECase AnalysisA ∨ B[A]...C[B]...CCProve C from each disjunct separately.¬INegation Intro[A] ... ⊥¬AAssume A, derive contradiction, conclu...¬ENegation ElimA¬A⊥A statement and its negation give a co...RAAReductio (Double Negation Elim)[¬A] ... ⊥AAssume ¬A, derive contradiction, concl...⊥EEx Falso⊥AFrom falsehood, anything follows.

Click any card to see a concrete example. Premises are above the line; conclusion is below.

Go deeper:Introduction and elimination

Natural deduction is a proof system that mirrors how mathematicians actually reason. Each logical connective has introduction and elimination rules. To prove A → B, assume A and derive B (introduction). Given A → B and A, conclude B (elimination / modus ponens). Proofs build tree-like structures from assumptions to conclusions.

Natural deduction has a small set of rules, each tied to a connective. Introduction rules tell you how to prove a formula; elimination rules tell you how to use one. Together, they form a complete system for propositional logic.

Key insight: The introduction/elimination pattern is deeply symmetric. In type theory, this symmetry corresponds to constructors and deconstructors -- the Curry-Howard correspondence between proofs and programs.

Proof Tree Builder

Pick a proof and step through it. The conclusion sits at the bottom, the tree grows upward, and assumptions are marked once a rule discharges them.

Proof tree — conclusion at bottom, assumptions at top (depth 1)p → p→I (1)
Step 1 / 2
Go deeper:Reading a proof tree

A proof tree grows upward: the conclusion sits at the root (bottom), and each rule application adds premises as children. Assumptions appear as leaves. When a rule discharges an assumption (like →I), it is marked as used. Step through pre-built proofs to see the tree unfold.

Key insight: A proof tree with no undischarged assumptions is a proof of a theorem -- a formula true in all interpretations. Open assumptions represent hypotheses that the conclusion depends on.

Classic Proofs Gallery

Choose a classic proof and step through it line by line. Notice which ones need reductio ad absurdum (RAA) to finish.

Identity: p → pThe simplest conditional proof: assume the antecedent and you already have it.#FormulaJustification1.pAssume (1)
Line 1 / 2
Go deeper:Classical and intuitionistic logic

Some proofs are milestones of logic. The identity proof (p → p) is the simplest non-trivial derivation. Double negation elimination (¬¬p → p) requires the classical rule of reductio ad absurdum. The law of excluded middle (p ∨ ¬p) is surprisingly tricky. Walk through each one.

Key insight: Without the rule of reductio ad absurdum (proof by contradiction), you get intuitionistic logic, where p ∨ ¬p and ¬¬p → p are not provable. The choice of rules determines which logic you are working in.

Key Takeaways

  • Natural deduction has introduction and elimination rules for each connective.
  • Proof trees grow upward from the conclusion, with assumptions as leaves.
  • Discharging assumptions converts conditional proofs into theorems.
  • Classical vs intuitionistic logic differs in whether contradiction-based rules are allowed.

Spot a mistake or have an idea?

Search