Learn natural deduction

A proof starts from the premises and reaches the conclusion in small steps, each justified by a rule. In Fitch notation, every line states the formula, the rule that allows it and the lines that rule relies on. If every line is correct, the conclusion follows from the premises.

What you want to prove is written as a sequent, for example a ∧ b, a → c ⊢ c ∧ b. The premises sit to the left of ⊢, separated by commas, and the conclusion to the right. With nothing on the left, as in ⊢ a → a, the formula has to come from the rules alone, and it is called a theorem.

To save parentheses, ¬ binds tightest, ∧ and ∨ bind tighter than →, a chain of ∧ groups to the left and a chain of → groups to the right. So a → b ∧ c is a → (b ∧ c), a ∧ b ∧ c is (a ∧ b) ∧ c and a → b → c is a → (b → c). The site always shows the short form.

Step through the proof below, line by line, and notice what each justification cites.

None of these lines asks you to know what a, b or c mean. A rule applies if the cited formulas have the shape it requires, whatever the subject. That is why a proof can be checked by hand or by a program, without debating the meaning of anything.

Each connective brings two kinds of rule. The introduction rule, marked I, says how to reach a formula with that connective. The elimination rule, marked E, says what you can take from a formula that already has it. In the next sections you see, for each rule, its schema, where φ and ψ stand for any formulas, an example and the most frequent slip.

Conjunction is the best place to start: φ ∧ ψ asserts both formulas, so there is one rule to join them and another to split them.

The elimination rule looks only at the main connective of the cited line. In a ∧ b ∧ c, which is (a ∧ b) ∧ c, the two sides are a ∧ b and c. Each ∧E removes one layer, and the example above spends one line per layer.

An implication φ → ψ is a promise: whenever you have φ, you have ψ. Using it is a plain exchange. You bring φ and you get ψ, with nothing else to do.

An implication asserts neither φ nor ψ. It only rules out the case where φ is true and ψ is false. So having φ → ψ on a line gives you neither formula, and you must obtain φ some other way before applying the rule.

It remains to see how to reach an implication. That takes a new tool, the subproof, which is the topic of the next section.

To prove φ → ψ, you don't need to know whether φ is true. You assume φ, just to see where it leads, and show that ψ follows. The assumption opens a subproof: a proof inside the proof, with its own bar and with the hypothesis on its first line.

A subproof is cited as a range, from the hypothesis to the last line, for example 3–6. If it has a single line, the range starts and ends there, like 1–1 in ⊢ a → a, where the hypothesis a is already the last line.

Everything you write inside a subproof may depend on the hypothesis, so it only holds while the hypothesis is in force. When the subproof closes, the hypothesis stops counting, and the lines inside can no longer be cited one by one. What remains is the whole range, which is what the →I rule uses.

The other direction is no problem: from inside a subproof you can directly cite the outer lines above it, without repeating them. The proof must end on a line outside every subproof.

Subproofs can also sit inside one another. The most recent one closes first. Follow this proof, where each →I closes one hypothesis, the inner one before the outer one.

One case is left. The subproof has to end on the formula you want, and that formula may already be written outside. Citing it is not enough, because it has to appear as the last line. That is what R is for: it repeats a formula on a new line.

To reach φ ∨ ψ, one of the formulas is enough. Using a disjunction takes more work: you don't know which one is true, so you handle both cases.

The formula you add with ∨I can be anything, even one that appears nowhere else. The price is losing information: from a you go to knowing only that a or b is true. That is why ∨I is usually the last step, once you know which side you can prove.

In ∨E, each case is a separate subproof, and what you write in one cannot be cited in the other. The conclusion need not mention φ or ψ at all. It only has to be the same formula on the last line of both cases, and that is the one that moves outside.

To deny φ is to show that φ leads to a contradiction, written F. This is where ¬I, ¬E, FI and FE come in.

F is a formula like any other, except that it is never true. Other texts write it as ⊥, and you can type it that way here too, although the site always displays F. The usual way to reach it is the FI rule.

With F you can now deny things. The ¬I rule follows the idea from the opening: you suppose φ, reach F and conclude that φ cannot be true.

Elimination does very little: it removes two negations in a row, and nothing else. No rule gives you φ from ¬φ, because those two formulas say the opposite of each other.

That leaves FE. From a contradiction you can write any formula. It looks odd, but a line with F only appears in an impossible situation, where nothing is left to tell apart. It is mostly useful in ∨E: a case that contradicts the rest ends in F, and FE makes it give the formula the other case reaches.

Some proofs repeat the same pattern every time. Derived rules give it a name, and each of them can be replaced by a proof that uses only base rules.

A derived rule doesn't let you prove anything new. It shortens what you can already prove. Each figure has the schema, the right moment to use the rule and a proof with base rules only. Those proofs are written with p, q and r, but they hold for any formulas in place of φ, ψ and θ: just swap the letters.

In a proof, a derived rule is used like any other: you write its abbreviation and cite the lines. With MT, this proof does in two lines what would take two subproofs with base rules only.

The shape of the conclusion and of the premises often tells you the next step. These are the questions to ask when you don't know how to go on.

Start from the conclusion. Its shape tells you how the proof is likely to end, and that gives you a smaller goal:

• If it is φ ∧ ψ, prove each side and join them with ∧I.
• If it is φ → ψ, suppose φ and look for ψ. Close with →I at the end.
• If it is ¬φ, suppose φ and look for F. Close with ¬I at the end.
• If it is φ ∨ ψ, see whether you can prove one side and finish with ∨I. Sometimes neither side comes out alone, and then the answer lies in the premises.

Ask the same question for each new goal. Play the proof below, or step through it by hand, and read the reason for each line.

After each strategy there is a lab, with a sequent to prove right here. It opens in guided mode: you tap the lines you want to cite and choose the rule. If you prefer typing, switch mode at the top of the editor.

When the conclusion stops helping, look at what you have. Every accessible line offers something:

• From φ ∧ ψ, take both sides with ∧E. It costs nothing and gives you more lines to cite.
• From φ → ψ, try to get φ, because then →E gives you ψ.
• From φ ∨ ψ, open both cases with ∨E and aim for the same goal in each. Do this early: inside each case you have one more line to use.
• With ¬φ, look for φ. If you get it, FI gives you F.

If none of this is enough, reductio ad absurdum remains. Suppose the negation of the goal and look for F. You gain a line to use, and the contradiction often comes from a negated premise. It comes last because the proof ends up longer and less direct.

If you are still stuck, the proof may not exist. The next section explains how to show that.

The underlying question remains: does what you can prove match what is true under every valuation? Soundness and completeness say that it does.

So far, everything has been syntax: ⊢ means that there is a proof. The other notion comes from truth tables. A valuation gives each variable the value true or false, and we write ⊨ when every valuation that makes the premises true also makes the conclusion true.

Soundness says that if there is a proof, the sequent is valid: ⊨ follows from ⊢. The reason lies in the rules, because each one preserves truth. If what it cites is true, what it writes is true as well. Inside a subproof the same holds, for the valuations that make the open hypotheses true. Since a proof is a chain of such steps, the truth of the premises reaches the conclusion.

This gives you a way to show that there is no proof, without trying them all. One valuation with true premises and a false conclusion is enough, and it is called a counterexample.

Completeness is the opposite direction: if the sequent is valid, there is a proof. ⊢ follows from ⊨. This is the hard part, because it says the rules leave nothing out. The demonstration is beyond this lesson, but the idea is this: when a conclusion cannot be proved, you can build a valuation that serves as a counterexample.

Neither result is automatic, because both depend on the chosen rules. If you remove ¬E from the base rules, for example, a ∨ ¬a stays true under every valuation and no longer has a proof.

Together, they say that ⊢ and ⊨ coincide. Every sequent has either a proof or a counterexample, never both. Completeness only says that the proof exists, not that it is short or easy to find, and that is what strategies are for.