3.2  Four Kinds of Task

The method of Section 3.1 answers one kind of question: here are premises, here is a conclusion, find a derivation. Mathematics asks others as well:

  • prove a statement from nothing;
  • show that two statements say the same thing;
  • show that some conditions cannot all be met at once;
  • decide whether a conclusion follows at all, when nobody says whether it does.

Each of these changes where a search starts and what counts as its end. This section takes the four tasks in turn. Underneath, it finds, they are one question.

3.2.1. Four tasks, one method

Let the task choose the search. The four tasks use the same rules and the same method. What differs is the first move and the finish line.

Task The claim Where the search starts What ends it
theorem ⊢φ step 2 on the goal; every resource is an assumption the goal asks for the goal, reached outside every box
equivalence φ⊣⊢ψ (Definition 2.4.2) two searches, one from each side two derivations
inconsistency Γ⊢⊥ step 4: the goal is ⊥; look for a clash partner already on a line ⊥, outside every box
derive or break Γ⊢φ? (verdict withheld) try to break it first a derivation, or statements that make the counterexample set true

Only the last task leaves open which way it ends. The other three state their claim: a failed search leaves the question open, as Section 3.1’s failed search did, and a break ends the task against the claim.

Quick check. Which task is each? (i) ⊢P∨¬P. (ii) P∧Q⊣⊢Q∧P. (iii) Show that P, ¬P∨Q and ¬Q cannot all be accepted together. (iv) Does P→Q, Q⊢P hold?

Solution.

  • (i) A theorem. (ii) An equivalence. (iii) An inconsistency: the claim P, ¬P∨Q, ¬Q⊢⊥. (iv) Derive or break; it breaks, since it is affirming the consequent (Section 1.3).

3.2.2. Theorems

A theorem of logic is a statement derivable from no premises, ⊢φ (Definition 1.2.3 with the list empty).

Solution. There are no premises, so step 1 writes only the goal. Step 2 opens a box on P→(Q∧¬Q) with the goal ¬P, and then, inside it, a box on P with the goal ⊥:

1P→(Q∧¬Q)asm, for →I
⋮
7¬P
8(P→(Q∧¬Q))→¬P→I 1–7
1P→(Q∧¬Q)asm, for →I
2Pasm, for ¬I
⋮
6⊥
7¬P¬I 2–6
8(P→(Q∧¬Q))→¬P→I 1–7

Now there are two resources, both assumptions the goal asked for. Step 3 fires the first on the second, giving Q∧¬Q, and splits it by ∧E. Step 4 finds the clash.

1P→(Q∧¬Q)asm, for →I
2Pasm, for ¬I
3Q∧¬Q→E 1, 2
4Q∧E 3
5¬Q∧E 3
6⊥¬E 4, 5
7¬P¬I 2–6
8(P→(Q∧¬Q))→¬P→I 1–7

A theorem has no premises, so the goal does all the early work. Once proved, it is a derived rule with nothing above the line (Definition 2.3.1): any derivation, from any premises, may write an instance of it as a line, as derivations already write LEM.

3.2.3. Equivalences

Solution. (⇒) The goal is an implication, so a box on P∧¬Q. ∧E splits it, the premise fires on P, and DS removes the refuted side.

1P→(Q∨R)
2P∧¬Qasm, for →I
⋮
6R
7(P∧¬Q)→R→I 2–6
1P→(Q∨R)
2P∧¬Qasm, for →I
3P∧E 2
4¬Q∧E 2
5Q∨R→E 1, 3
⋮
6R
7(P∧¬Q)→R→I 2–6
1P→(Q∨R)
2P∧¬Qasm, for →I
3P∧E 2
4¬Q∧E 2
5Q∨R→E 1, 3
6RDS 5, 4
7(P∧¬Q)→R→I 2–6

(⇐) The goal is an implication: a box on P, with the goal Q∨R. That goal is a disjunction, so it is postponed (step 2). The premise waits for P∧¬Q: P is in hand, ¬Q is not, and nothing clashes. That is step 5, and the well-chosen statement is Q, whose negation the premise waits for: LEM on Q.

1(P∧¬Q)→R
2Pasm, for →I
⋮
10Q∨R
11P→(Q∨R)→I 2–10
1(P∧¬Q)→R
2Pasm, for →I
3Q∨¬QLEM
4Qasm, for ∨E
⋮
5Q∨R
6¬Qasm, for ∨E
⋮
9Q∨R
10Q∨R∨E 3, 4–5, 6–9
11P→(Q∨R)→I 2–10

In the case Q, ∨I gives the left side. In the case ¬Q, ∧I builds P∧¬Q, the premise gives R, and ∨I gives the right side.

1(P∧¬Q)→R
2Pasm, for →I
3Q∨¬QLEM
4Qasm, for ∨E
5Q∨R∨I 4
6¬Qasm, for ∨E
7P∧¬Q∧I 2, 6
8R→E 1, 7
9Q∨R∨I 8
10Q∨R∨E 3, 4–5, 6–9
11P→(Q∨R)→I 2–10

An equivalence is two searches, and they need not be alike. The direction (⇒) used a derived rule and no classical step. The direction (⇐) reached step 5, because its goal was a disjunction with no side in hand. When one direction is easy, do it first: it checks that the statements are worth comparing, and its lines often suggest the other direction’s split.

3.2.4. Inconsistent lists

Sometimes the task is not to reach a conclusion but to show that some statements cannot be accepted together: a puzzle’s conditions that no number meets, the hypotheses of a lemma that contradict each other, or the assumption of a proof by contradiction together with what is given. Section 2.5 (Exercise (B5: Derive or break, used later)) already read an RAA derivation as a derivation of ⊥ from the counterexample set. A derivation of ⊥ does this job, and the list it starts from gets a name.

Definition 3.2.1 (Inconsistent and Consistent Lists)

Let Γ be a list of statements φ1,…,φn, where n≥0. The list Γ is inconsistent if Γ⊢⊥: some derivation whose premises all belong to Γ has ⊥ as its last line. It is consistent if it is not inconsistent, that is, if no derivation with premises in Γ ends with ⊥.

In words: a list is inconsistent when a derivation from it reaches ⊥ outside every box. The definition speaks only of derivations, and says nothing about whether the statements are true. The list P,¬P is inconsistent, by one ¬E line, and so is any list with ⊥ as a member. To show a list inconsistent, exhibit a derivation. To show one consistent, one would have to rule out every derivation, and nothing in this chapter can do that.

Proposition 3.2.1 (An Inconsistent List Proves Everything)

For a list of statements Γ, the following are equivalent:

  • (i) Γ is inconsistent;
  • (ii) Γ⊢ψ for every statement ψ;
  • (iii) Γ⊢χ and Γ⊢¬χ for some statement χ.

In words: an inconsistent list proves every statement, and a list that proves some statement and its negation is inconsistent. This is Proposition 2.1.1 grown from two premises to any inconsistent list. Its proof is in the fold of the next subsection.

Quick check. Without writing a derivation, explain why P, ¬P⊢Q∧¬Q.

Solution. The list P,¬P is inconsistent (one ¬E line), so by Proposition 3.2.1, (i) ⇒ (ii), it derives every statement, Q∧¬Q included.

Solution. The goal is ⊥. Look first for a clash partner already on a line (Section 3.1): line 4 is ¬F, so aim at F.

F is the conclusion of line 1, so the new goal is E, a letter. Line 3 gives E from T, but T is not in hand, and E∨T does not say which side holds. So use line 2 by ∨E, with both cases ending in E. The case E is a one-line box; the case T fires line 3.

1E→F
2E∨T
3T→E
4¬F
⋮
9F
10⊥¬E 9, 4
1E→F
2E∨T
3T→E
4¬F
5Easm, for ∨E
6Tasm, for ∨E
⋮
7E
8E∨E 2, 5–5, 6–7
9F→E 1, 8
10⊥¬E 9, 4
1E→F
2E∨T
3T→E
4¬F
5Easm, for ∨E
6Tasm, for ∨E
7E→E 3, 6
8E∨E 2, 5–5, 6–7
9F→E 1, 8
10⊥¬E 9, 4

Read as a proof about n, the derivation shows that no integer meets all four conditions: by (2) and (3), n is even in either case; by (1) it is a multiple of 4; and (4) says it is not. Yet any three of the conditions can be met together: n=6 meets all but (1), n=1 all but (2), n=3 all but (3), and n=12 all but (4). The inconsistency belongs to the four together. The derivation does not say which condition to drop (the fold “Logic permits; it does not choose” in Section 3.1).

Quick check. Which integers between 1 and 10 meet conditions (1), (2) and (4) of Example (Four conditions that no integer meets), and which condition does each break?

Solution. 3 and 9: they are odd, so (1) promises nothing; they are multiples of 3, so (2) holds; and they are not multiples of 4. Each breaks (3).

Here are three more inconsistent lists, each with compound members, and one list that only looks inconsistent.

Example (Three inconsistent lists, and a look-alike)
The list The clash it reaches The derivation of ⊥, in brief
(P∨Q)→R, P∧¬R R, ¬R P by ∧E; P∨Q by ∨I; R by →E; ¬R by ∧E; ⊥ by ¬E (7 lines)
P↔¬P P, ¬P a box on P: ¬P by ↔E, ⊥ by ¬E; ¬P by ¬I; then P by ↔E, and ¬P by ↔E again from that P; ⊥ by ¬E (8 lines)
¬(P→Q), ¬P P→Q, ¬(P→Q) P→Q by VI from ¬P (Proposition 2.1.2); ⊥ by ¬E (4 lines)

Not an instance. P→Q, P→¬Q. The two members look opposed. But with P false (say P: “0=1”) both are true, whatever Q says, so the claim P→Q, P→¬Q⊢⊥ breaks. What the list does derive is ¬P: from P it would give Q and ¬Q. This chapter does not call the list inconsistent, and it does not call it consistent either. Whether a break rules out every derivation of ⊥ is the question the chapter ends on (Section 3.3).

The second row’s derivation is written without a detour: the line ¬P built by ¬I is cited by ↔E, never taken apart at once by ¬E, so it stays, as Section 3.1’s detour paragraph allows (“an introduced line cited elsewhere stays”).

Warning (Not allowed: claims about inconsistency). Each claim below is wrong; the tag names what it misreads.

  • “The list is inconsistent because one of its members is false.” Truth for derivation: inconsistency is a derivation of ⊥ (Definition 3.2.1), not a false member. The one-member list “2>3” has a false member, and no derivation of ⊥ is offered.
  • “P→Q and P→¬Q contradict each other, so the list is inconsistent.” Looks for derivation: nothing has been derived. Both members are true when P is false, and the claim of inconsistency breaks.
  • “Line 7, inside the box of the assumption P, is ⊥; so the premises are inconsistent.” A boxed line: that ⊥ depends on P. It shows the list Γ,P inconsistent, and so Γ⊢¬P. The last line must lie outside every box (Definition 1.4.2).
  • “A search for ⊥ stalled, so the list is consistent.” A stall for a proof: a stalled search proves nothing (Section 3.1). Consistency is the absence of every derivation of ⊥.
  • “The list is inconsistent, so its first member is false.” The list for a member: inconsistency belongs to the list. It says that the members cannot all be accepted together, not which one fails (compare the four conditions above).

3.2.5. The counterexample set, derived

Proving and refuting meet in one list. The counterexample set of a claim Γ⊢φ is the list Γ,¬φ (Definition 1.1.3). Breaking the claim makes that list true. Deriving the claim, it turns out, is showing that list inconsistent.

Proposition 3.2.2 (Derivable Exactly When the Counterexample Set Is Inconsistent)

Let Γ be a list of statements and φ a statement.

  • (a) Γ⊢¬φ if and only if the list Γ,φ is inconsistent.
  • (b) Γ⊢φ if and only if the list Γ,¬φ is inconsistent.

In words: (b) says that a claim is derivable exactly when its counterexample set is inconsistent, and (a) says the same for a negated conclusion. In the proofs, the box of (a) closes by ¬I and that of (b) by RAA: Section 2.5’s distinction between the two rules, stated about whole derivations. Section 1.1’s test of a form, try to break it, now has a partner on the same list: make the counterexample set true, or derive ⊥ from it.

With Γ empty and φ the statement P↔¬P, part (a) says that the second row of Example (Three inconsistent lists, and a look-alike) and Lemma 2.4.2, ⊢¬(P↔¬P), are the same fact.

Second readingThe proofs: append a line, or copy a derivation into a box

Proof. Proof of Proposition 3.2.1. (i) ⇒ (ii): a derivation of ⊥ with premises in Γ, followed by the line ψ by ⊥E, is a derivation of ψ. Its last line lies in no box. (ii) ⇒ (iii): apply (ii) to any χ and to ¬χ. (iii) ⇒ (i): the sequent χ,¬χ⊢⊥ has a one-step derivation (¬E), so by Lemma 2.3.3 (c), Γ⊢⊥.

Proof. Proof of Proposition 3.2.2. (b), (⇒): from Γ⊢φ, Lemma 2.3.3 (a) gives Γ,¬φ⊢φ. The one-line derivation of the premise ¬φ gives Γ,¬φ⊢¬φ. By Lemma 2.3.3 (c) with φ,¬φ⊢⊥, we get Γ,¬φ⊢⊥.

(b), (⇐): let D be a derivation of ⊥ with premises in Γ,¬φ. If the last line of D is a premise in Γ, then ⊥ is a member of Γ, and ⊥E gives φ. (The last line cannot be the premise ¬φ, since ¬φ is not ⊥.) Otherwise, write as premises those premises of D that belong to Γ. Open a box with the assumption ¬φ. Inside it, copy the lines of D that are not premises, in order, with their boxes, renumbering citations; a citation of the premise ¬φ now cites the assumption. Close the box after the copy of the last line of D, and write φ by RAA.

Every copied citation is legal. A cited premise of Γ lies above the box, in no box. The assumption is available throughout the box. The boxes of D sit inside the new box as they sat in D, so every line and every box that was available at a citing line stays available (the scope rule of Definition 1.4.2). The last line of D lies in no box of D, so its copy is a line of the new box itself, as RAA requires. If D never cites ¬φ, nothing changes.

Part (a) is the same, with φ in place of ¬φ and ¬I in place of RAA. If the last line of D is the premise φ itself (possible only when φ is ⊥), nothing is copied: the box is its one assumption line, and ¬I closes it at once. In (⇒), Γ,φ⊢φ and, by weakening, Γ,φ⊢¬φ; chaining with ¬E finishes.

The copying is the move of Section 1.4’s Exercise (C4: The assumptions a line depends on, used later) (b), which turns open assumptions into premises, run backwards.

Quick check. By Proposition 3.2.2, which list must be shown inconsistent to prove ⊢¬(P∧¬P)? Show it.

Solution. By (a), with Γ empty and φ the statement P∧¬P, the list is P∧¬P:

1P∧¬P
2P∧E 1
3¬P∧E 1
4⊥¬E 2, 3

3.2.6. One task in four costumes

Every task of this section is a claim that something is derivable, and by Proposition 3.2.2 every such claim is a claim that a list is inconsistent.

Task As a claim of derivability As a claim of inconsistency It breaks when some choice of statements makes
theorem ⊢φ the list ¬φ φ false
equivalence φ⊢ψ and ψ⊢φ the lists φ,¬ψ and ψ,¬φ one of φ, ψ true and the other false
inconsistency Γ⊢⊥ the list Γ every member of Γ true
derive or break Γ⊢φ the list Γ,¬φ every member of Γ,¬φ true

An equivalence is also a theorem: φ⊣⊢ψ holds exactly when ⊢φ↔ψ. Copy each of the two derivations into a box, as in the fold above, and close both boxes by ↔I. Conversely, add the premise φ to a derivation of φ↔ψ and write ψ by ↔E, and likewise for ψ.

So the four tasks are one: is this list inconsistent? Each costume starts the search in a different place, which is why the task chooses the search. And each row has a second half, the last column: what to do when the list might instead be made true. That is the fourth task.

3.2.7. Derive or break

Section 1.5 listed claims without a verdict (“Derive it or break it”). Here the format becomes a task with its own first move: decide before you search.

Try to break it first. Spend a few minutes trying to make the counterexample set true, starting where the conclusion is false (Section 1.1, “Where to look first”). Either some choice of statements works, and the claim breaks; or every attempt is forced into a clash. Then search for a derivation. The forced attempt usually suggests a plan for it: the statements the attempt had to make true suggest the assumptions of the derivation’s boxes, and the clash it met suggests the derivation’s ⊥.

Solution. (a), trying to break it. The conclusion is false only with P true and ¬Q false, that is, Q true. Then the first premise needs Q→R true, so R true. The second needs ¬R true, so R false. Every choice was forced, and the forcing ends in a clash. So we search.

(a), the derivation. The attempt’s plan: a box on P (the conclusion’s hypothesis), a box on Q (the statement whose negation is wanted), and the clash R, ¬R. Before the box on Q opens, both premises fire on P: lines that need nothing new (Section 3.1).

1P→(Q→R)
2P→¬R
3Pasm, for →I
⋮
9¬Q
10P→¬Q→I 3–9
1P→(Q→R)
2P→¬R
3Pasm, for →I
4Q→R→E 1, 3
5¬R→E 2, 3
6Qasm, for ¬I
⋮
8⊥
9¬Q¬I 6–8
10P→¬Q→I 3–9
1P→(Q→R)
2P→¬R
3Pasm, for →I
4Q→R→E 1, 3
5¬R→E 2, 3
6Qasm, for ¬I
7R→E 4, 6
8⊥¬E 7, 5
9¬Q¬I 6–8
10P→¬Q→I 3–9

(b), trying to break it. The same start: P true, Q true. Now the first premise asks only that Q∨R be true, and Q already makes it so. R is free, and the second premise asks for R false. Nothing clashes: with P and Q true and R false, every member of the counterexample set P→(Q∨R), P→¬R, ¬(P→¬Q) is true. With statements about a real number x, take P: “x>0”, Q: “x>1”, R: “x>3”, at x=2. The claim breaks.

The two claims differ in one connective. Trying to break each found its verdict, and for (a) it also found the derivation. The method of Section 3.1 would have found (a) without the attempt. On (b) the method of Section 3.1 could only search, and a stall is not a verdict; the break is.

The task as a chart. The loop at the bottom is honest: nothing in this chapter promises that it ends.

Diagram. Labels: every try is forced into a clash, a claim Gamma vdash varphi ,\verdict withheld, can the counterexample set\be made true? (start where\the conclusion is false), it breaks:\give the statements, search for a derivation\\(Section 3.1): the forced\clash suggests a plan, has the search\finished ?

Quick check. Change one symbol of the first premise of claim (b) in Example (Two claims, one connective apart) so that the claim can be derived, and derive it.

Solution. For example, replace ∨ by →: that is claim (a), derived above. Or replace ∨ by ∧: from P, the premises give Q∧R and ¬R, which clash.

1P→(Q∧R)
2P→¬R
3Pasm, for →I
4Q∧R→E 1, 3
5R∧E 4
6¬R→E 2, 3
7⊥¬E 5, 6
8¬Q⊥E 7
9P→¬Q→I 3–8

Replacing ∨ by ↔, or Q by R, works too. For ↔: from P, the premises give Q↔R and ¬R; a box on Q gives R by ↔E, which clashes with ¬R, so ¬Q by ¬I. For Q replaced by R: from P, R∨R gives R by ∨E, which clashes with ¬R, so ¬Q by ⊥E.

Remark (Looking ahead). Chapter 4 calls a list whose members can all be made true at once satisfiable, and proves that the satisfiable lists are exactly the consistent ones.

3.2.8. Exercises

A. Check your understanding

Exercise (A1)
  • (a) When is a list of statements inconsistent?
  • (b) By Proposition 3.2.2, which list is inconsistent exactly when P→Q, Q→R⊢P→R?
  • (c) True or false: every list that has ⊥ as a member is inconsistent.
  • (d) True or false: if Γ is inconsistent, so is every list Γ,ψ.
  • (e) Name the task and the first move: “show that P∧Q⊣⊢Q∧P”.

Solution.

  • (a) When ⊥ is derivable from it (Definition 3.2.1).

  • (b) The counterexample set P→Q, Q→R, ¬(P→R).

  • (c) True: the one-line derivation whose only line is the premise ⊥ ends with ⊥.

  • (d) True, by Lemma 2.3.3 (a): the derivation of ⊥ from Γ has its premises in Γ,ψ.

  • (e) An equivalence: two derivations, each starting with ∧E on its premise. Each is Proposition 1.2.1, with the letters exchanged for the second.

Exercise (A2: Drill)

The parts run from naming the task, through one step and a missing piece, to claims to judge and short derivations.

  • (a) Which task is “show ⊢(P∧Q)→P”?
  • (b) “Show that P→¬Q and Q→¬P are provably equivalent.” Which two derivations does this ask for?
  • (c) Write “P, P→Q and ¬Q cannot all be accepted together” as a sequent.
  • (d) A search for ⊥ from P∧¬Q, P→Q begins. Write its first three lines after the premises.
  • (e) Which list must be shown inconsistent to prove P→Q⊢¬Q→¬P by Proposition 3.2.2 (b)?
  • (f) The list Q, ¬P, ¬¬R is the counterexample set of which claims?
  • (g) “P→Q, P→¬Q is inconsistent, since its members contradict each other.” Is this correct?
  • (h) “Inside the box of the assumption P, line 6 is ⊥; so the premises are inconsistent.” Is this correct?
  • (i) “A search for ⊥ from P∨Q, ¬P stalled; so the list is consistent.” Is this correct?
  • (j) “Since P,¬P⊢⊥, the list P,¬P derives both Q and ¬Q.” Is this correct?
  • (k) Derive ⊥ from P→Q, Q→R, P, ¬R.
  • (l) Derive ⊥ from P∨Q, ¬P, ¬Q.

Solution.

  • (a) A theorem.

  • (b) P→¬Q⊢Q→¬P and Q→¬P⊢P→¬Q.

  • (c) P, P→Q, ¬Q⊢⊥.

  • (d) 3 P, ∧E 1; 4 Q, →E 2, 3; 5 ¬Q, ∧E 1. (Then 6 ⊥, ¬E 4, 5.)

  • (e) P→Q, ¬(¬Q→¬P).

  • (f) Of Q,¬P⊢¬R, with ¬¬R the negated conclusion, and of Q,¬¬R⊢P, with ¬P the negated conclusion. Q is not a negation, so it is not the negated conclusion of any claim.

  • (g) No. Both members are true when P is false, and nothing has been derived.

  • (h) No. It shows the premises together with P inconsistent, so the premises derive ¬P.

  • (i) No: a stalled search proves nothing.

  • (j) Yes: Proposition 3.2.1, (i) ⇒ (ii).

  • (k) 5 Q, →E 1, 3; 6 R, →E 2, 5; 7 ⊥, ¬E 6, 4.

  • (l) 4 P, assumption; 5 ⊥, ¬E 4, 2; 6 Q, assumption; 7 ⊥, ¬E 6, 3; 8 ⊥, ∨E 1, 4–5, 6–7.

B. Practice

Exercise (B1: Three theorems)

Derive each theorem, and say which step of Section 3.1’s method opens each box.

  • (a) ⊢¬(P∧¬P)∧¬¬(P∨¬P).
  • (b) ⊢((P→Q)∧(P∨Q))→Q.
  • (c) ⊢((P→Q)→Q)→((Q→P)→P).

Solution.

  • (a)
    1P∧¬Pasm, for ¬I
    2P∧E 1
    3¬P∧E 1
    4⊥¬E 2, 3
    5¬(P∧¬P)¬I 1–4
    6¬(P∨¬P)asm, for ¬I
    7Pasm, for ¬I
    8P∨¬P∨I 7
    9⊥¬E 8, 6
    10¬P¬I 7–9
    11P∨¬P∨I 10
    12⊥¬E 11, 6
    13¬¬(P∨¬P)¬I 6–12
    14¬(P∧¬P)∧¬¬(P∨¬P)∧I 5, 13

    Boxes 1 and 6 come from step 2: each goal is a negation. Box 7 comes from step 2 inside step 4: step 4 chooses to manufacture P∨¬P from its side ¬P, so that it clashes with line 6, and the goal ¬P, a negation, opens the box. The second conjunct needed no classical rule, although P∨¬P itself does in this book’s derivation (Proposition 2.5.3).

  • (b)
    1(P→Q)∧(P∨Q)asm, for →I
    2P→Q∧E 1
    3P∨Q∧E 1
    4Pasm, for ∨E
    5Q→E 2, 4
    6Qasm, for ∨E
    7Q∨E 3, 4–5, 6–6
    8((P→Q)∧(P∨Q))→Q→I 1–7

    Box 1 comes from step 2. Boxes 4 and 6 come from step 3: the resource P∨Q is split by ∨E, both cases ending in the goal Q (the case Q is a one-line box). Lines 2 and 3 need nothing new. Read aloud: if P implies Q, and P or Q holds, then Q holds.

  • (c)
1(P→Q)→Qasm, for →I
2Q→Pasm, for →I
3¬Pasm, for RAA
4P→QVI 3
5Q→E 1, 4
6P→E 2, 5
7⊥¬E 6, 3
8PRAA 3–7
9(Q→P)→P→I 2–8
10((P→Q)→Q)→((Q→P)→P)→I 1–9

Boxes 1 and 2 come from step 2. Box 3 comes from step 5: the goal P is a letter, and the resources wait for P→Q, which nothing in hand gives.

Exercise (B2: Two directions)

Show that (P∧Q)→R⊣⊢(P∧¬R)→¬Q.

  • (a) The search for (⇐) has reached the stage below. Name the move, then complete it.
  • (b) Derive (⇒).
  • (c) Which direction used a classical rule, and why did the other not need one?
1(P∧¬R)→¬Q
2P∧Qasm, for →I
⋮
9R
10(P∧Q)→R→I 2–9

Solution.

  • (a) First the lines that need nothing new, P and Q by ∧E. Then the move is step 5: the current goal R is a letter, no resource gives it, and nothing clashes, so assume ¬R for RAA.
    1(P∧¬R)→¬Q
    2P∧Qasm, for →I
    3P∧E 2
    4Q∧E 2
    5¬Rasm, for RAA
    6P∧¬R∧I 3, 5
    7¬Q→E 1, 6
    8⊥¬E 4, 7
    9RRAA 5–8
    10(P∧Q)→R→I 2–9
  • (b)
    1(P∧Q)→R
    2P∧¬Rasm, for →I
    3P∧E 2
    4¬R∧E 2
    5Qasm, for ¬I
    6P∧Q∧I 3, 5
    7R→E 1, 6
    8⊥¬E 7, 4
    9¬Q¬I 5–8
    10(P∧¬R)→¬Q→I 2–9
  • (c) (⇐) used RAA at line 9, because its goal R is a letter. (⇒) needed none, because its goal ¬Q is a negation, which ¬I builds. This is a claim about our two derivations only.

In words: to prove “if P and Q, then R”, it is enough to prove “if P and not R, then not Q”, a contrapositive in one hypothesis.

Exercise (B3: Derive or break, used later)

For each claim, derive it or break it. Try to break it first. To break a claim, give statements that make its counterexample set true.

  • (a) ¬P∨¬Q⊢¬(P∨Q)
  • (b) ¬(P↔Q), P⊢¬Q
  • (c) P→Q, ¬P→(R∨Q), ¬R⊢Q
  • (d) P→Q, ¬P→(R∨Q), ¬R⊢P
  • (e) (P→Q)→R, ¬R⊢P
  • (f) (P→Q)→R, ¬R⊢Q
  • (g) P∨Q, P⊢¬Q
  • (h) P∨Q, ¬(P∧Q), P⊢¬Q
  • (i) ¬(P∨Q)→P⊢P∨Q

Solution. The verdict comes first, then the derivation or the break. In every break, x is a real number.

  • (a) Breaks. Take P: “x>2”, Q: “x>0”, at x=1. ¬P is true, so ¬P∨¬Q is true; Q is true, so P∨Q is true and ¬(P∨Q) is false. (The De Morgan law with this premise is ¬P∨¬Q⊢¬(P∧Q), Proposition 2.5.5 (c); here the wrong connective sits inside the negation.)

  • (b) Derive.

    1¬(P↔Q)
    2P
    3Qasm, for ¬I
    4Pasm, for ↔I
    5QR 3
    6Qasm, for ↔I
    7PR 2
    8P↔Q↔I 4–5, 6–7
    9⊥¬E 8, 1
    10¬Q¬I 3–9

    This is the first box of Exercise (B5: Derive or break, used later) (f).

  • (c) Derive. Step 5: the goal Q is a letter, and the first two premises wait for P and for ¬P, so LEM on P. DS matches as stated in Section 2.3, refuting the left disjunct R.
    1P→Q
    2¬P→(R∨Q)
    3¬R
    4P∨¬PLEM
    5Pasm, for ∨E
    6Q→E 1, 5
    7¬Pasm, for ∨E
    8R∨Q→E 2, 7
    9QDS 8, 3
    10Q∨E 4, 5–6, 7–9
  • (d) Breaks. Take P: “x>5”, Q: “x>0”, R: “x>10”, at x=1. P is false, so P→Q is true; ¬P and Q are true, so ¬P→(R∨Q) is true; ¬R is true; and P is false. Trying to break it first: with P false, the premises force Q true and R false, and nothing clashes. The tempting step from “P gives Q” and “Q holds”, which (c) derives, to P is affirming the consequent (Section 1.3).

  • (e) Derive.

    1(P→Q)→R
    2¬R
    3¬(P→Q)MT 1, 2
    4¬Pasm, for RAA
    5P→QVI 4
    6⊥¬E 5, 3
    7PRAA 4–6
  • (f) Breaks. Take P: “x>0”, Q: “x>2”, R: “x>3”, at x=1. P→Q is false, so (P→Q)→R is true; ¬R is true; and Q is false.

  • (g) Breaks; it is affirming a disjunct (Section 1.6). Take P: “x>1”, Q: “x>2”, at x=3: P∨Q and P are true, and ¬Q is false.

  • (h) Derive. The premise P∨Q is not needed.

1P∨Q
2¬(P∧Q)
3P
4Qasm, for ¬I
5P∧Q∧I 3, 4
6⊥¬E 5, 2
7¬Q¬I 4–6
  • (i) Derive. Step 2 postpones the disjunction. The premise waits for ¬(P∨Q), which RAA on the goal supplies; step 4 then manufactures the clash partner P∨Q from line 3 by ∨I, a manufactured clash and not a detour.
1¬(P∨Q)→P
2¬(P∨Q)asm, for RAA
3P→E 1, 2
4P∨Q∨I 3
5⊥¬E 4, 2
6P∨QRAA 2–5

Read aloud: a statement whose failure would force one of its own sides holds.

  • (c) and (d), and (e) and (f), are look-alike pairs: each pair has the same premises and differs in the conclusion. (h) is (g) repaired by “not both”. (a) is a De Morgan look-alike with the wrong connective inside.
Exercise (B4: Derive ⊥, or make every member true, used later)

For each list, either derive ⊥ from it, or give statements that make every member true at once.

  • (a) P→Q, Q→¬P, P
  • (b) P∨Q, P→¬Q, Q→¬P
  • (c) ¬(P→Q), Q∨¬P
  • (d) P→(Q∧¬Q)
  • (e) ¬(P∨Q), P∨(Q∧R)
  • (f) ¬(P∧Q), ¬(P∧¬Q), ¬(¬P∧Q)

Solution.

  • (a) Derive ⊥: 4 Q, →E 1, 3; 5 ¬P, →E 2, 4; 6 ⊥, ¬E 3, 5.

  • (b) True at once. Take P: “x>0”, Q: “x<0”, at x=1: P∨Q is true; ¬Q is true, so P→¬Q is true; and Q→¬P is true, since Q is false.

  • (c) Derive ⊥.

    1¬(P→Q)
    2Q∨¬P
    3Qasm, for ∨E
    4Pasm, for →I
    5QR 3
    6P→Q→I 4–5
    7⊥¬E 6, 1
    8¬Pasm, for ∨E
    9P→QVI 8
    10⊥¬E 9, 1
    11⊥∨E 2, 3–7, 8–10
  • (d) True at once, with P false (P: “0=1”, any Q). A member that mentions a contradiction is not itself a clash: with P false every member is true, so the claim that the list derives ⊥ breaks.

  • (e) Derive ⊥.

    1¬(P∨Q)
    2P∨(Q∧R)
    3Pasm, for ∨E
    4P∨Q∨I 3
    5⊥¬E 4, 1
    6Q∧Rasm, for ∨E
    7Q∧E 6
    8P∨Q∨I 7
    9⊥¬E 8, 1
    10⊥∨E 2, 3–5, 6–9
  • (f) True at once, with P and Q both false (P: “1>2”, Q: “2>3”): each conjunction has a false member, so each negation is true. Adding a fourth member ¬(¬P∧¬Q) gives a list from which ⊥ can be derived: the four exclude every way for P and Q to be. Use LEM on P and, inside each case, on Q; each of the four cases builds the conjunction that one member negates, by ∧I, and clashes with it.

Section 4.7 shows that a list made true at once, as in (b), (d) and (f), is consistent.

C. Going deeper

Exercise (C1: Exit check: the counterexample set, used later)

Let Γ be the list P→(Q∨R), Q→S, R→S.

  • (a) Write the counterexample set of Γ⊢P→S.
  • (b) Show that it is inconsistent.
  • (c) What does Proposition 3.2.2 conclude? Give also a direct derivation of Γ⊢P→S, and compare the two.
  • (d) Replace one premise so that the claim breaks, and break it.

Solution.

  • (a) P→(Q∨R), Q→S, R→S, ¬(P→S).

  • (b) The goal is ⊥, and the clash partner ¬(P→S) is already on a line (Section 3.1), so aim at P→S.

    1P→(Q∨R)
    2Q→S
    3R→S
    4¬(P→S)
    5Pasm, for →I
    6Q∨R→E 1, 5
    7Qasm, for ∨E
    8S→E 2, 7
    9Rasm, for ∨E
    10S→E 3, 9
    11S∨E 6, 7–8, 9–10
    12P→S→I 5–11
    13⊥¬E 12, 4
  • (c) By part (b) of the proposition, Γ⊢P→S. The direct derivation is lines 1–3 and 5–12 of (b), renumbered: 11 lines. The route through the counterexample set adds the premise ¬(P→S) and one ¬E line, and gains nothing here. It pays when the goal gives step 2 nothing (a letter, or a disjunction with no side in hand), and then it is step 5.

  • (d) For instance, replace R→S by R→T. Take P: “x>0”, Q: “x>5”, R: “x<2”, S: “x>3”, T: “x<10”, at x=1. P and R are true, so Q∨R and P→(Q∨R) are true; Q→S is true, since Q is false; R→T is true, since T is true; and P→S is false, since S is false. So every member of the new counterexample set is true. Any replacement that a choice of statements breaks is accepted.

Marking scheme. (10 points)

  • 2: the counterexample set, with ¬(P→S), not ¬P→S or P→¬S.
  • 3: the derivation of ⊥: P→S derived (by a box whose cases of Q∨R both end in S, or by Example (Cases on a hypothesis are two implications) and Proposition 1.4.1), and ¬E outside every box.
  • 2: the conclusion drawn by the proposition, and the direct derivation.
  • 3: (d), a changed premise, with statements checked against all four members of the new counterexample set.

Fatal errors (0 for the step): ⊥ written inside the box of P and taken as the end; a “break” in (d) that leaves a premise false.

Exercise (C2: Challenge: Splitting an inconsistency, used later)

Let Γ be a list and φ a statement.

  • (a) Prove that if Γ,φ and Γ,¬φ are both inconsistent, then so is Γ.
  • (b) Deduce: if Γ is consistent, then at least one of Γ,φ and Γ,¬φ is consistent.
  • (c) Does (b) say which one?

Solution.

  • (a) Since Γ,φ is inconsistent, Proposition 3.2.2 (a) gives Γ⊢¬φ. Since Γ,¬φ is inconsistent, part (b) gives Γ⊢φ. So (iii) of Proposition 3.2.1 holds with χ the statement φ, and Γ is inconsistent.

  • (b) This is the contrapositive of (a): if both lists were inconsistent, Γ would be.

  • (c) No. It says that one of the two lists is consistent and gives no way to tell which. Deciding that would need a way to show a list consistent, which this chapter does not have.

Section 4.10 (optional) adds statements to a consistent list one at a time, in exactly this way.

Marking scheme. (10 points)

  • 4: (a) obtains Γ⊢¬φ by part (a) of the proposition or Γ⊢φ by part (b), and combines it with the other inconsistency, directly (by Cut, Lemma 2.3.3 (b)) or by the other part.
  • 3: (a) concludes by Proposition 3.2.1, by Lemma 2.3.3 (c) with one ¬E, or by Cut (Lemma 2.3.3 (b)).
  • 2: (b) as the contrapositive.
  • 1: (c) “no”.

Fatal error: (b) claimed to show that a particular list is consistent.