Natural Deduction for Propositional Logic

Definition and intuition

Natural deduction is a proof system in which each logical connective comes with two rules: an introduction rule (how to build a formula with that connective) and an elimination rule (how to use one). A proof is a tree: premises and discharged assumptions sit at the leaves, each horizontal bar applies one rule, and the conclusion is the formula at the root. We write $\Gamma \vdash \varphi$ when $\varphi$ is derivable from the set of assumptions $\Gamma$.

The defining trick is the assumption: you may write any formula in brackets, e.g. $[A]$, use it freely, and later discharge (close) it with an $\to I$ step. A formula proved with no open assumptions is a theorem ($\vdash \varphi$).

The core rules

The $\to I$ rule is the key one: to prove $A \to B$, assume $A$, derive $B$, then discharge that assumption $[A]$ and conclude $A \to B$. The bracket is closed exactly at the $\to I$ that introduces the implication.

Soundness and completeness

These two metatheorems tie syntax (derivations, $\vdash$) to semantics (truth tables, $\models$):

• Soundness: if $\Gamma \vdash \varphi$ then $\Gamma \models \varphi$. Every rule preserves truth, so anything you derive is genuinely a logical consequence — the system never proves a falsehood.
• Completeness: if $\Gamma \models \varphi$ then $\Gamma \vdash \varphi$. Every tautology (and every valid entailment) has a derivation. Together: $\Gamma \vdash \varphi \iff \Gamma \models \varphi$.

How to check a derivation

Konkur questions often show a finished proof tree and ask whether (or how many times) the rules were misused. The checklist:

1. Match each bar to its rule schema. Read the rule label and confirm the premises above the bar and the conclusion below it fit that exact pattern (e.g. $\to E$ needs both $A \to B$ and $A$, and yields $B$).
2. Track assumptions. Every bracketed $[A]$ is an open assumption until some $\to I$ below it discharges it. At the root, no bracket may remain open for a theorem.
3. Read bottom-up then top-down. Bottom-up tells you what is being introduced; top-down confirms each required premise is actually present in the tree.

Mini-example: $\vdash (A \to B) \to (A \to B)$

Assume $[A \to B]$ and, separately, $[A]$. Apply $\to E$ to get $B$, then $\to I$ discharging $[A]$ to get $A \to B$, then $\to I$ discharging $[A \to B]$:

$\dfrac{\dfrac{\dfrac{[A \to B] \quad [A]}{B}\ \to E}{A \to B}\ \to I}{(A \to B) \to (A \to B)}\ \to I$

Both brackets are discharged, no assumption stays open, and the conclusion is a tautology — a fully correct derivation.

Exam trick: Don't be intimidated by a tall proof tree. Read it bottom-up to see what each bar introduces, then top-down to confirm every premise the rule needs is actually present. The tell-tale sign of a correct conditional proof is that each bracketed assumption $[A]$ lines up with exactly one $\to I$ below it that discharges it — if every bracket closes and every bar matches its schema, the count of incorrect uses is $0$.