Natural Deduction

Prove conclusions from premises with introduction and elimination rules.

The idea

Natural deduction is a proof system: a method for establishing that a conclusion follows from premises by applying inference rules to the formulas themselves, without evaluating truth values.

A derivation is a finite list of formulas in which every line is a premise, a temporary assumption, or the result of applying an inference rule to earlier lines. Each connective carries two rules: an elimination rule that takes a formula built with it apart, and an introduction rule that builds one. For conjunction, elimination passes from $P \wedge Q$ to $P$, and introduction passes from $P$ together with $Q$ to $P \wedge Q$.

That some derivation of $\varphi$ from the premises $\Gamma$ exists is written $\Gamma \vdash \varphi,$ read as $\Gamma$ proves $\varphi$. The claim is purely syntactic: a rule applies because the earlier lines have the required shape, not because anyone has checked that they are true. This is what makes a derivation mechanically checkable — a machine can verify every step by matching shapes. Whether the conclusion is true is a separate, semantic question, and a derivation never consults it.

Ways to work on it

• Walkthrough. Chain named inference rules to derive a conclusion from premises.
• Practice. Identify the conclusion a named rule licenses.
• Hardest. Prove an implication from the given premises.

Not sure where to start? Take the ten-question placement test.