You have been writing proofs for years — "assume n is even, then n = 2k, so…". A formal proof system takes that informal habit and makes it into a game with strict rules: a fixed, tiny list of legal moves, and a proof is nothing but a finite record of those moves. No hand-waving, no "clearly", no appeals to intuition — every single line must be justified by a rule you could check with a stamp. It is so mechanical that a computer can verify it, which is exactly what proof assistants like Coq, Lean and Isabelle do: they check that a human's chain of moves really is legal, all the way down.

This page teaches one such system — natural deduction — and, above it, the one idea that gives all formal systems their point: the gap between truth and derivation. Everything here builds on ordinary proof by deduction; we are just making the deduction formal.

Two turnstiles: \models versus \vdash

There are two completely different questions you can ask about "does P follow from \Gamma?", and formal logic keeps them apart with two symbols that look alike but mean very different things.

• \Gamma \models P — semantic entailment. It says: in every valuation (every "possible world", every truth-table row) that makes all of \Gamma true, P is true as well. This is about meaning and truth.
• \Gamma \vdash P — syntactic derivability. It says: there exists a formal proof of P from the premises \Gamma, built entirely by pushing symbols around with the rules of your chosen system. This is about shape and moves, not meaning at all.

The \models symbol is read "models" or "entails"; the \vdash symbol (a "turnstile") is read "proves" or "yields". A machine can check \vdash by inspecting a proof line by line; checking \models in general means reasoning about all models. That these two end up agreeing is the deepest fact in the subject.

What a formal proof is

A formal proof of P from premises \Gamma is a finite sequence (or tree) of formulas ending in P, in which every formula is either

• a premise from \Gamma, or a temporary assumption we open (and must later close), or
• an axiom — a formula the system hands you for free, no justification needed, or
• the result of applying a rule of inference to earlier lines.

The difference between an axiom and a rule matters. An axiom is a specific formula declared true at the start (for example P \rightarrow (Q \rightarrow P) in some systems). A rule of inference is a licence to move: given lines of one shape, you may write down a line of another shape. "From P \rightarrow Q and P, write Q" is a rule, not a formula.

Different systems strike the axiom-versus-rule balance differently:

• A Hilbert system is nearly all axioms and almost no rules — often just a few axiom schemes plus the single rule modus ponens. Proofs are long, flat lists; the system is easy to reason about but painful to compute in.
• Natural deduction (Gentzen, 1934) flips it: almost no axioms, but a rich kit of introduction and elimination rules — one pair per connective — plus the ability to make and discharge assumptions. Proofs read the way people actually argue.
• The sequent calculus works instead with whole sequents \Gamma \vdash \Delta and left/right rules; it is the tidiest for proving things about proofs (cut-elimination, decidability).

We spend the rest of this page in natural deduction.

The introduction and elimination rules

Natural deduction gives each connective an introduction rule (how to build a formula with that connective) and an elimination rule (how to use one). Read \dfrac{\text{premises}}{\text{conclusion}} as "from the premises above the bar, infer the conclusion below it".

Conjunction.

Implication. Elimination is modus ponens; introduction is a conditional proof — you assume P, derive Q, then discharge the assumption to conclude P \rightarrow Q. The square brackets [P] mark the assumption as closed.

Disjunction. Introduction is easy; elimination is proof by cases — to use P \vee Q, show the goal R follows from P alone and from Q alone.

Negation and contradiction. Write \bot for "contradiction" (the absurdity). To introduce a negation, assume P, reach \bot, and conclude \neg P. To eliminate, a formula and its negation together give \bot.

The last, reductio ad absurdum (RAA, or "proof by contradiction"), is the classical extra: assume the negation of what you want, derive absurdity, and conclude the thing itself. (Intuitionists accept \negI but not RAA — that one rule is the whole quarrel between classical and constructive logic.)

Worked example: a full derivation

Let us prove \vdash (P \wedge Q) \rightarrow (Q \wedge P) — commuting a conjunction — with no premises at all (so it is a theorem). The strategy is set by the goal: to prove an implication, use \rightarrowI, which tells us to assume the left side and chase the right side.

1. Assume P \wedge Q. (assumption 1)
2. Q, by \wedgeE on line 1.
3. P, by \wedgeE on line 1.
4. Q \wedge P, by \wedgeI on lines 2, 3.
5. (P \wedge Q) \rightarrow (Q \wedge P), by \rightarrowI, discharging assumption 1.

Because line 5 discharges the only assumption, the finished proof depends on nothing: we have shown \vdash (P \wedge Q) \rightarrow (Q \wedge P). The diagram below is the same proof drawn as a tree — premises above each bar, conclusions below — so you can watch it grow move by move.

Another classic: modus tollens

Modus tollens — from P \rightarrow Q and \neg Q, conclude \neg P — is not a primitive rule; it is derived. Here is P \rightarrow Q,\ \neg Q \vdash \neg P:

1. P \rightarrow Q (premise)
2. \neg Q (premise)
3. Assume P. (assumption 1)
4. Q, by \rightarrowE on 1, 3.
5. \bot, by \negE on 4, 2.
6. \neg P, by \negI, discharging assumption 1.

Notice how the whole argument turns on opening assumption 1 at line 3 and closing it at line 6. Everything between lives inside that assumption's scope; once discharged, \neg P rests only on the two genuine premises.