Proofs

A truth table checks an argument by trying every case. A proof does something different: it shows how the conclusion follows from the premises, through a chain of small steps that anyone can check. This guide covers the proof system the app uses: natural deduction, drawn in the style of Frederic Fitch, with the rules of forall x: Calgary. If arguments and validity are new to you, read the basics guide first.

What a proof is

A proof is a numbered list of formulas. It starts with the premises and ends with the conclusion. Every line in between follows from earlier lines by a rule: a small step that clearly keeps truth, such as “from P → Q and P, infer Q”.

Why prove, when a truth table can settle the question? A table doubles with every sentence letter, while a proof often needs only a few lines. A proof also shows why the conclusion follows, step by step, much as people reason. And in richer logics, such as the first-order logic that forall x turns to later, truth tables can no longer settle validity, but proofs still work.

Lines, premises and citations

Each line has a number, a formula and a justification that says where the formula comes from. The premises come first, each marked PR, with a horizontal bar under the last one. Every later line names a rule and cites the earlier lines the rule uses, by their numbers. So “→E 1, 3” means “by the rule →E, from lines 1 and 3”.

The proof is finished when the conclusion, which the app calls the goal, stands on a line of the main proof and every line is correct.

Assumptions and subproofs

Sometimes you reason from a supposition: “suppose it rained; then …”. Such a supposition is an assumption, marked AS. It opens a subproof: the assumption and the lines after it, indented with a vertical bar of their own and a horizontal bar under the assumption. A subproof can contain further subproofs, each adding a bar.

The lines of a subproof hold only under its assumption. So when the subproof ends, it is closed, and its lines can no longer be cited one by one. Instead, some rules cite the whole subproof, as a range from its assumption to its last line, such as 3–5. Closing a subproof this way is called discharging its assumption. Every subproof must be closed before the proof ends.

Introduction and elimination rules

Most rules come in pairs, one pair for each connective. An introduction rule says how to prove a formula with that main connective. An elimination rule says how to use a formula with that main connective once you have it. Here A and B stand for any formulas:

• ∧I, Conjunction introduction: from A and B, infer A ∧ B. ∧E, Conjunction elimination: from A ∧ B, infer A, or B.
• →E, Conditional elimination (also known as modus ponens): from A → B and A, infer B. →I, Conditional introduction: if a subproof that assumes A reaches B, close it and infer A → B.

A few rules are not tied to one connective, such as R (Reiteration), which repeats an earlier line. The full list is in Going deeper. Since the main connective decides which rules fit, the syntax trees guide helps here too.

Worked example: a chain of conditionals

“If it rains, the street is wet. If the street is wet, it is slippery. So if it rains, it is slippery.” This is P → Q, Q → R ∴ P → R. The truth tables guide shows that it is valid. Here is how to prove it.

1. Enter the argument. Type P -> Q, Q -> R :. P -> R under Argument to prove, or use the button above. The app turns the spellings into symbols, writes the premises as lines 1 and 2, and shows the goal, P → R, under Goal.
2. Plan from the goal. The goal is a conditional, and →I proves conditionals: assume the antecedent, P, reach the consequent, R, then close the subproof.
3. Assume P. On line 3, type P and press Tab. The line becomes an assumption, indented in a new subproof.
4. Use the first premise. Press Enter for line 4, which stays in the subproof. Type Q, and in the justification field type →E 1, 3 (or ->E 1,3): from P → Q on line 1 and P on line 3, Conditional elimination gives Q.
5. Use the second premise. Line 5 is R, by →E 2, 4.
6. Close the subproof. Press Enter, then Shift+Tab to move line 6 out of the subproof. Type P → R and justify it by →I 3–5, citing the whole subproof. Type the range as 3-5; the app shows it as 3–5.
7. Check. Every line now ends in ✓, and under Goal the app says Proof complete.

Line 6 does not say that P is true, only that if P is true, so is R. That is why the subproof must close: Q and R on lines 4 and 5 hold only under the assumption P, so after line 6 they no longer count.

Worked example: proof by cases

“The key is in the drawer or in my coat. It is not in the drawer. So it is in my coat.” This is P ∨ Q, ¬P ∴ Q. To use a disjunction, ∨E (Disjunction elimination) argues by cases: if the goal follows from the left side, and also from the right side, it follows from the disjunction. It cites the disjunction and two subproofs, one for each side.

1. First case: assume P. Line 3 is P, an assumption.
2. Find a contradiction. Line 2 says ¬P and line 3 says P. ¬E (Negation elimination) turns a formula and its negation into ⊥: line 4 is ⊥, by ¬E 2, 3.
3. Anything follows from ⊥. X (Explosion) gives any formula from ⊥, so line 5 is Q, by X 4. The first case reaches the goal.
4. Second case: assume Q. Press Enter, then Shift+Tab and Tab. The first subproof closes, and a new one opens with Q as its assumption on line 6.
5. Repeat it. This subproof must end with Q, and it starts with it. R (Reiteration) repeats an earlier line: line 7 is Q, by R 6.
6. Combine the cases. Press Enter, then Shift+Tab to return to the main proof. Line 8 is Q, by ∨E 1, 3–5, 6–7.

Line 8 cites the subproof 3–5 although another subproof came after it. A closed subproof can still be cited as a whole from later lines.

A shortcut: derived rules

This pattern is common enough to have its own rule. DS (Disjunctive syllogism) goes from A ∨ B and ¬A to B in one step:

DS is a derived rule: whatever it does, the basic rules can do too, as the 8-line proof shows. The app offers the five derived rules of forall x (DS, MT, DNE, LEM and DeM) while Allow derived rules is on, as it is for a new proof. Switch it off to practise with the basic rules only; a line that uses DS then gets ✗ and the explanation “DS is a derived rule, and derived rules are switched off for this proof.”

Complete proof follows the switch. With derived rules on, it gives the 3-line proof. With them off, it gives a proof by cases of 7 lines instead of 8: its last line is ∨E 1, 3–5, 6–6, which cites the one-line subproof on line 6 directly, instead of repeating Q with R.

Choosing rules and getting help

• The rule list. Each justification field ends in a Choose a rule button (⌄). It lists the basic rules, then the derived rules if they are allowed. Each entry shows the rule’s symbol, its full name, its shape (the first, if it has several) and what it cites: →E is Conditional elimination, and “cites 2 lines”. Pick one, and the app writes it into the field, keeps any citations already typed, and leaves the cursor ready for them. From the keyboard, Ctrl+Space opens the list, ↑ and ↓ move through it, Enter picks a rule, and Esc closes it.
• Suggestions while typing. Start typing a rule, such as → or ->, and the matching rules appear under the field. The switch Suggest rules while typing, next to Allow derived rules, turns this off; the button and Ctrl+Space still work.
• Line marks. Each line ends in ✓ (correct), ✗ (has an error) or … (unfinished). Click ✗ to read what is wrong. If a rule does not fit the lines it cites, the explanation also shows the rule’s shape.
• Hints. Hint says what to aim for next, and Show next line writes that line for you. At the start of the first example, Hint says “Your goal P → R is a conditional. Assume its antecedent and work towards its consequent, then close the subproof by →I.”, and Show next line adds P as an assumption on line 3.
• Solve and Practice. In Solve, the default, Complete proof fills in a whole proof and says “Here is a complete proof. Undo brings your own lines back.” In Practice there is no Complete proof, but Hint and Show next line still help. Exercises open in Practice.

Common mistakes

Citing a line inside a closed subproof. After line 6 of the first example, the subproof 3–5 is closed. A line 7 that gets R by →E 2, 4 looks harmless, but Q on line 4 held only under the assumption P. The app marks it ✗: “4 is inside a subproof that has already closed, so line 7 can't use it.” The subproof can still be cited as a whole, as 3–5, by a rule that cites a subproof.

• Forgetting to close a subproof. If you forget Shift+Tab, line 6 stays inside the subproof it cites, and the app says “Line 6 is still inside the subproof 3–5. A subproof can be cited only after it closes.” The goal is not in the main proof either.
• Citing too few or too many lines. Each rule cites a fixed number of lines and subproofs. →E 1 on line 4 gets “→E cites 2 lines, but this line gives 1 citation.”
• Two lines instead of a range. →I 3, 5 cites two separate lines; →I 3–5 cites the subproof from line 3 to line 5. The first gets “→I cites 1 subproof, but this line gives 2 citations.”
• Using a rule backwards. From P → Q and Q, no rule gives P, and no proof can: that is affirming the consequent, an invalid pattern.

The rules of forall x

These are the app’s rules, as forall x: Calgary gives them. In a shape, “A, B ⊢ C” means: from lines of the form A and B, infer C. “[A … B]” stands for a subproof whose assumption is A and whose last line is B. The cited lines may come in any order.

Why derived rules are safe

Each derived rule is a shortcut. Its conclusion can be proved from what it cites with the basic rules alone, by a fixed pattern of lines; for DS, the pattern is the proof by cases above. So any proof that uses a derived rule can be rewritten without it, by putting the pattern in its place. Derived rules make proofs shorter, but never let you prove anything new. A rule with that property is called admissible, and every derived rule is admissible for this reason.

Scope, precisely

The app checks citations as forall x does:

• A line can cite an earlier line only while that line is still available: it is in the main proof, or in a subproof that is still open at the citing line. Lines inside a closed subproof are out of reach.
• A subproof is cited only as a whole, as i–j, from its assumption on line i to its last line j. It must have closed before the citing line, and its last line must sit on its own level, not inside a subproof nested in it.
• A closed subproof stays citable from every later line, unless it lies inside another subproof that has closed in the meantime.
• Premises come first. Premises and assumptions take no justification. Every subproof must be closed by the end, and the goal must stand in the main proof.

Soundness and completeness

Write Γ ⊢ A when there is a proof of A whose premises are among the formulas Γ (the Greek capital gamma). It is the same symbol as in the rule shapes above: a shape says that one step leads from what the rule cites to its conclusion, and Γ ⊢ A says that a whole proof leads from Γ to A. Write Γ ⊨ A when the argument is valid: every valuation that makes all of Γ true makes A true. Two theorems connect them, for any finite list of premises Γ:

• Soundness: if Γ ⊢ A, then Γ ⊨ A. Each rule keeps truth: whenever the premises and the assumptions still open are true, so is the new line. So a proof can never lead from true premises to a false conclusion.
• Completeness: if Γ ⊨ A, then Γ ⊢ A. Every valid argument has a proof. This is harder to show: the usual proof starts from the fact that A cannot be proved from Γ and builds a valuation that makes Γ true and A false.

So for propositional logic, proofs and truth tables pick out exactly the same arguments. The app relies on this. Before it searches for a proof, Complete proof checks the argument by truth table (if it has at most 20 sentence letters), and for an invalid argument it says “This argument is invalid, so it has no proof.” and shows a valuation with the premises true and the goal false: for P → Q, Q ∴ P, P false and Q true. For a valid argument, the search is built to find a proof every time, given enough steps, but the app stops it after 50,000 steps.

⊢ and ⊨

The two symbols look alike but come from different worlds. The single turnstile ⊢ is about proofs: rules applied to symbols, with no mention of truth. The double turnstile ⊨ is about truth: valuations, with no mention of rules. Soundness and completeness say that, for propositional logic, the two agree.

A theorem is a formula that can be proved from no premises at all: ⊢ A. By soundness and completeness, the theorems are exactly the tautologies. To prove one in the app, start the argument with ∴, as in :. P v ~P.

Indirect proof and ¬I

Two rules are made for subproofs that end in ⊥. ¬I (Negation introduction) assumes A and concludes ¬A. IP (Indirect proof) assumes ¬A and concludes A. They look alike, but ¬I only adds a negation, while IP takes one away.

IP is what makes the logic classical. Without it, and without the derived rules, the other basic rules cannot prove P ∨ ¬P or ¬¬P → P; they give what is called intuitionistic logic. This proof of P ∨ ¬P uses both rules. It assumes the negation of the goal (line 1). Inside, assuming P leads to P ∨ ¬P, which clashes with line 1, so ¬I gives ¬P. But ¬P leads to P ∨ ¬P as well, another clash. So the assumption on line 1 is impossible, and IP concludes P ∨ ¬P.

Further reading

forall x: Calgary, the free textbook whose rules the app uses, covers all of this in its part on natural deduction for TFL, its name for propositional logic: the basic rules, how to construct proofs, the additional rules and how to derive them, ⊢ and theorems, and soundness and completeness. The proof of soundness itself is in its Metatheory part. Natural deduction goes back to Gerhard Gentzen and Stanisław Jaśkowski, who published it independently in 1934; the bars come from Frederic Fitch’s Symbolic Logic (1952). The tableaux guide compares proofs with tableaux, which are also sound and complete.