1.6 Using Or: Proof by Cases
The previous section met a goal the rules could not
reach: from
1.6.1. A proof that needs two cases
The absolute value of a real number is defined in two
cases:
So the proof we want has the shape “every real number
is
1.6.2. The rule of or-elimination
To use “
The definition block states both rules for
disjunction, so that the pair stands in one place: the
new rule first, then the two schemas of
The first schema is the rule
This rule has conditions that matter; read each one.
- The disjunction. Line
holds a disjunction , available at line . The cases are not ours to invent: they are the two sides of a disjunction we already have, as a premise, an assumption, or a line derived earlier. Writing “Case 1 … Case 2 …” does not create it. - Two boxes. The first box opens with
the left side
as its assumption, the second with the right side . They are separate: the second opens after the first has closed, and the drawing shows a break in the vertical bar between them. So, by the scope rule of Definition 1.4.2, no line of the second box may cite a line of the first. The disjunction does not tell us which side holds, so we must be ready for both, and each case’s assumption is in force only inside its own box. Each case box’s assumption is printed “asm, for ”; read it as “Case 1: …” and “Case 2: …”. - The same last line. Both boxes end
in the same statement
, and in each box is a line of that box itself, not of a box opened inside it. The rule then writes a third time, outside both boxes, where neither nor is assumed. That is honest only because was reached whichever case holds. - Three citations. The justification
“
” cites the disjunction first, then the box of the left side, then the box of the right side, each box as a range. Both boxes must be available at line : closed, and sitting directly in the part of the derivation where line is (Definition 1.4.2). - Any conclusion. The statement
need not mention or . It is whatever we are trying to reach. The next subsection says how to choose it.
Second readingA box of one line
The degenerate case is a box of one line, whose
assumption is already
Warning. A case may use only its
own assumption. Here is the error in its usual form. Let
1.6.3. Cases end in the current goal
Section 1.2 set up two questions: what is the
goal’s main connective? and what are the
available lines’ main connectives? Section 1.5
answered the first for
What should the two boxes end in? The rule leaves
Cases end in the current goal.
The two habits fit together. Faced with a goal
In the Givens/Goal table, each case of a split adds its assumption to the Givens and keeps the same Goal. For the stalled goal:
| Givens | Goal |
|---|---|
Show that
Solution. Idea. For the
first: the goal
The two boxes are separate: the break in the vertical
bar between lines 3 and 4 shows where the first closes
and the second opens. Line 3 uses the second schema of
For the second, the goal is
This is the degenerate case split, in which the two
cases are the same case. The box
Second readingOne line short
Change one line of the first derivation and it stops
being a derivation. Suppose the second box stops at its
assumption
Everything cited exists and is available: the
disjunction, a box opened by
Quick check. A derivation contains
a line
Solution. The clause “two boxes”:
the rule needs one box opened by each side of the
disjunction, and the box opened by
Second readingWhy one common last line loses nothing
Why is the rule built like this?
Drop the second box, and from “
The next derivation splits on a disjunction that is not a premise but an assumption, opened because the goal asked for it.
Show that
Solution. Idea.
Goal-directed: the goal is an implication, so we open a
box with its hypothesis
Line 9 closes the split inside the outer box. It is a
line of the outer box itself, so
Quick check. In the derivation of
Example (Cases on a hypothesis are two implications),
which lines and boxes does the
Solution. Line 9 cites the
disjunction on line 2 and the two case boxes, as ranges:
Section 1.5 derived the converse,
1.6.4. Two cases, two conclusions
When the two cases lead to different statements, each case can still end in the current goal, if the goal is the disjunction of the two.
Show that
Solution. Idea. The goal
With numbers: let
The pattern is called the constructive
dilemma. When
1.6.5. Laws of “or”
Case splits are not only about numbers. The same two rules prove the laws that let us rearrange “and” and “or”. The first says that “and” distributes over “or”, in both directions.
Try it first (ten minutes): derive the first sequent. Which rule will give its last line, and which disjunction will you split on?
Idea. The natural first attempt
reads the goal: it is a disjunction, so end with
For the first derivation: the two case boxes opened, each ending in the goal; then lines 5 and 8 written, and only lines 6 and 9 left to justify.
Before reading on: in the first derivation, which line does each box end on, and why must the two be the same?
Proof. For the first sequent, the
following is a derivation with premise
Lines 5 and 8 may cite line 2, which lies in no box
and so is available everywhere below it. Both boxes end
in the goal, lines 6 and 9, as
For the second sequent, the following is a derivation
with premise
This proves both sequents.
The answer to the prompt: the boxes end on lines 6
and 9, both
In the second derivation, line 8 derives
Second readingDistributivity in words
For a real number
The next derivation shows a case split
inside a case:
Quick check. In the outline, which line closes the inner split, and which line and boxes does it cite?
Solution. Line 11. It cites the
disjunction on line 5 and the boxes
Show that
Solution. Idea. The goal
is a disjunction, and no side of it is in hand:
postpone. The premise is a disjunction: split on it,
with both boxes ending in the current goal
Before reading on: which disjunction does the
inner
Line 11 is the inner case split. It cites the
disjunction on line 5, the assumption of the outer box
it sits in, and the boxes
1.6.6. From a skeleton to a proof about numbers
Almost every proof by cases in analysis has the same skeleton. A known fact supplies the cases, and each case is handled by a separate argument, a small lemma that turns the case’s assumption into the goal. As a derivation, with the fact and the two lemmas as premises:
The idea behind it is the whole method of this
section at its simplest. The goal
In a proof about real numbers, the disjunction is
usually a fact about the order. The facts about
The first example is the smallest, and it is written twice: as a proof in which every step carries its rule in brackets, and as a derivation.
Let
Solution. The goal
We have
or , and we argue by cases . Case
. By the definition of the absolute value, . So . Case
. By the definition, , and ; so , which is the school-algebra fact “if , then ” used on the case’s assumption. So . In either case
, so .
As a derivation, with the order fact, the
definition’s first clause, and the school-algebra fact
about negative numbers as premises, and with
It is the skeleton above, with a weakening at the end
of each box: line 6 takes the right side of the goal
(second schema of
Quick check. In the derivation of Example (A number is at most its absolute value), which statement do lines 6 and 9 both write, and why must they agree?
Solution. Both write
The next two examples are longer, and in each the case split is doing real work.
Let
Solution. We use that
The number
Case
Case
Case
Case
Each inner case split reaches
The structure is two uses of
A case split need not be the obvious one. The triangle inequality has an equally short proof with two cases, if we split on the sign of the right quantity.
Let
Solution. First, every real number
Now
Case
Case
Both cases reach
Two case splits appear here, one after the other
rather than one inside the other. The first proves a
small lemma for an arbitrary number
Warning. A case split must cover
every possibility. A common faulty proof of the triangle
inequality treats “
Warning. Cases must
exhaust, and a split that silently
drops a value is a missing case in disguise. “Every real
Cases may overlap, however. “
Warning. Because “or” is inclusive,
knowing one side of a disjunction says nothing about the
other. The form “from
Quick check. Each of the following
begins a proof that
- (i) Case
; case . - (ii) Case
; case . - (iii) Case
; case .
Solution.
- (i) Exhaustive:
every real number is
or . (ii) Not exhaustive: is in neither case, so the disjunction cited is false. The claim is still true at , but this split never proves it there. (iii) Exhaustive. The cases overlap at , which does no harm: is reached in both.
1.6.7. The rules of this chapter
First, as for each rule before it, the newest rule matched against statements larger than single letters.
| Disjunction | First box | Second box | New line |
|---|---|---|---|
Not an instance. From
This chapter has introduced six rules, one or two at
a time, and the structural clause
| Rule | Shape | You write | Lean |
|---|---|---|---|
| “We show |
constructor |
||
| “In particular, |
h.1 (and h.2) |
||
| “Since |
exact h hp |
||
| box |
“Assume |
intro hp |
|
| “As shown above, |
exact hp |
||
| “So |
left (or Or.inl hp);
right |
||
| “Case 1: |
Or.elim h (or
cases h) |
A written proof often drops the first part of the
phrase for
Warning (Not allowed:
- “Close the split with one case box”: the clause “Two boxes”.
- “Close it when the boxes end in
and in ”: the clause “The same last line”. - “In the second box, cite a line of the first”: the clause “Two boxes” and the scope rule; the boxes are separate (the warning after the rule).
- “Split on ‘case
, case ’”: the clause “The disjunction”; the cases must be the sides of an available disjunction, and is not one (the warning on exhaustive cases). - “Cite the boxes’ lines one by one”: the clause “Three citations”; each box is cited as a range.
Here is the third step as a derivation, wrong on the
left and right on the right, with premises
The wrong line 6 uses the first case’s assumption in
the second case. Its lines never cite premise 2, so they
would “derive”
Here are the rules as schemas. Letters in the number column stand for line numbers; every cited line must be available (Definition 1.4.2), and each box rule needs the box’s last line as a line of that box itself.
Conjunction (Definition 1.2.5):
Implication (Definition 1.4.1):
Disjunction (Definition 1.6.1):
the two forms of
Each rule is also a move in the search for a derivation. Read by the goal’s main connective, the introduction rules say how a goal is built: that is the move read the skeleton off the goal. Read by an available line’s main connective, the elimination rules say how that line is used: use a premise by its main connective.
| Main connective | As the goal (goal-directed) | As an available line (premise-directed) |
|---|---|---|
| two subgoals, one per side; finish with |
take it apart with |
|
| open a box with the hypothesis; the new goal is the
conclusion; close with |
fire it with |
|
| postpone; choose a side with |
split with |
The table of moves as an order in which to try them:
The chart uses only this chapter’s rules, and
following it never writes an illegal line. It is a
guide, not a rule: after asking whether the goal is
already in hand, it reads the table’s goal column and
then its premise column, each from the top, except that
it leaves out two moves. When an available implication
ends in the goal but its hypothesis is on no line, make
the hypothesis the current goal and start the chart
again; items 3, 8 and 10 of Exercise (B7: Fifteen standard sequents)
need this. When the goal is a disjunction and neither
side is in hand, make one side the current goal; item 14
of Exercise (B7: Fifteen standard sequents)
does this in each case. (“Unsplit” at the test for
Named moves
- Try to break it. To test a form, put statements in for the letters that make every premise true and the conclusion false; one such choice shows the form is bad. (Section 1.1)
- Two ways to attack an argument. Show a premise false, or show a step’s form bad; the two attacks are independent. (Section 1.1)
- Read the skeleton off the goal. The
goal’s main connective chooses the introduction rule:
gives two subgoals, a box, a choice to postpone. (Section 1.2) - Use a premise by its main connective. Its elimination rule says what you may do with it: take a conjunction apart, feed an implication its hypothesis, split a disjunction into cases. (Section 1.2)
- Open a box, close a box. An assumption lives exactly as long as its box. (Section 1.4)
- Work from both ends. Premises at the top, the goal at the bottom; fill the gap from both sides. (Section 1.2)
- Postpone a disjunction. Choose a
side of a goal
only when that side is in hand. (Section 1.5) - Cases end in the current goal. Both
boxes of
close on the statement you are trying to reach. (Section 1.6)
Remark (Looking ahead). The rules
for “not”, for
1.6.8. Exercises
A. Check your understanding
(a) State the rule
as a schema, and name the three things its justification cites.(b) For each sentence, taken from a proof, name the disjunction that supplies the cases and the statement both cases end in.
- “If
is even, then is even; if is odd, then is even and so is . Either way, is even.” - “Both possibilities for the sign of
give .”
- “If
(c) Let
be an integer. True or false, with a reason: “If is even, then is even. Since every integer is even or odd, is even” is a correct proof by cases that is even.(d) The following is offered as a derivation of
. Name the line that is not justified and the clause of Definition 1.6.1 it violates.123 asm, for4 2, 35 1, 3–4(e) In the first derivation of Proposition 1.6.1, which line is the disjunction that
cites at line 10, and where did it come from? Why does each box end in rather than in and ?(f) In the same derivation, why does line 6 use
to put on the left? Could line 6 have been ?
Solution.
(a) The schema is the first one of Definition 1.6.1: from a line
holding , a box opened by , and a box opened by , each ending in the same statement as a line of its own, a line holding . The justification “ ” cites the disjunction and the two boxes.(b) In the first, the disjunction is “
is even or is odd”, and both cases end in “ is even”. In the second, it is “ or ” (the sentence does not say it, and a careful reader supplies it), and both cases end in .(c) False. The disjunction “
is even or is odd” does not say which side holds, so needs a second case, reaching “ is even” from “ is odd”, and the argument has none. Here the second case cannot be supplied: at the number is odd, so the claim itself is false.(d) Line 5.
needs two boxes, one opened by each side of the disjunction (the clause “two boxes”); line 5 cites only the box opened by , and no box opened by exists. Nor can a box opened by simply be added: nothing available reaches from . In fact the sequent’s form is bad, so no correct argument should be expected to reach from these premises. Try to break it: for a real number , take : “ ”, : “ ”, : “ ”. At both premises hold and does not.(e) Line 3,
, obtained from the premise by . Each box must end in the current goal, , because line 10 writes one statement, the same one that ends both boxes; boxes ending in and would end in different statements, and could not be applied to them.(f) Line 6 must be the current goal exactly, since both boxes end in it and line 10 writes it. The goal
has as its left side, so line 6 uses the first schema of . The line is also an instance of on line 5 (the second schema), but it is a different statement: the first box would then end differently from the second, whose last line 9 is , and could not cite both boxes.
Each part takes a line or two. The parts run from
reading a split, through a missing line and a
justification column, to whole derivations. Let
(a) “If
, then ; if , then . So .” Name the disjunction that supplies the cases, and the common last line.(b) How many case boxes does the proof of Example (The absolute value of a product) open?
(c) Inside a box whose current goal is
, the available line is split. What do the two case boxes end in?(d) Line 1 is
; a box runs from to , and a box from to . What does “ 1, 2–4, 5–7” write?(e) Line 9 is
, justified “ 2, 3–5, 6–8”, with line 3 and line 6 . What are lines 2, 5 and 8?(f) Justify each line: 1
, 2 , 3 , premises; 4 ; 5 ; 6 ; 7 ; 8 ; 9 . The boxes are and .(g) Two case boxes end in
and . May close the split?(h) Find the illegal line.
1234 asm, for5 2, 46 asm, for7 3, 48 1, 4–5, 6–7(i) Is the split “
or ” exhaustive for integers?(j) “Case
: . Case : . So for every real .” What fails?(k) Line 1 is
. A student opens a box with and a box with , each ending in , and writes “ — 1, 2–4, 5–7”. Correct?(l) Derive
.(m) Derive
.(n) Derive
.(o) Derive
.
Solution.
(a) The disjunction is
, and both cases end in .(b) Six: two for the sign of
, and two inside each of those for the sign of . (The opening remark that for is itself a small split on or , like the lemma in Example (The triangle inequality by cases); counting its two boxes as well gives eight.)(c)
, the current goal at the point of the split.(d)
, the common last line of the two boxes.(e) Line 2 is
, the disjunction whose sides open the boxes at lines 3 and 6; lines 5 and 8 are both , the last line of each box.(f) 4 assumption, for
; 5 2, 4; 6 assumption, for ; 7 6; 8 3, 7; 9 1, 4–5, 6–8.(g) No: both boxes must end in the same statement. Add
and lines so that both end in the current goal, say .(h) Line 7. It cites line 4, which lies in the box
, closed before line 7. It should read “ 3, 6”.(i) No:
is in neither case.(j) The split is not exhaustive:
is false at , so has no disjunction to cite. The conclusion fails there too: .(k) No: the main connective of line 1 is
, so it is no disjunction, and has nothing to split.(l) Box
: 2 , assumption, for ; 3 , 2; 4 , 3. Box : 5 , assumption, for ; 6 , 5. Then 7 , 1, 2–4, 5–6.(m) Box
: 2 , assumption, for ; 3 , 2. Box : 4 , assumption, for ; 5 , 4. Then 6 , 1, 2–3, 4–5.(n) Box
: 3 , assumption, for , already the goal. Box : 4 , assumption, for ; 5 , 2, 4. Then 6 , 1, 3–3, 4–5.(o) Box
: 2 , assumption, for ; 3 , 2; 4 , 3. Box : 5 , assumption, for ; 6 , 5; 7 , 6. Then 8 , 1, 2–4, 5–7.
B. Practice
Show that
Hint: after taking the premise apart, you will need a case split inside a case.
Solution. The goal is a disjunction
with no side in hand, so we postpone it. The premise
gives two disjunctions. Split on
Line 10 cites line 6, the assumption of the enclosing
box, which is still open at line 10. Line 12 cites line
3, which lies in no box. Splitting on
For real numbers
Solution. We have
Case
Case
In either case
Adding the two inequalities gives
(a) A search for
has reached the stage below. Name the move, then complete it.1234 asm, for67 asm, for1011 ?(b) Use (a) to prove: for every integer
, is a multiple of or one more than a multiple of . You may use that every integer is even or odd, and that is even for every integer .
Solution.
- (a) The move is to
split on the premise
, each case ending in the current goal: cases end in the current goal. The goal is a disjunction with no side in hand, so it is postponed, and line 11 will be citing line 1 and the two case boxes. In the case , line 2 fires and weakens to the goal. In the case , line 3 fires, takes out , and weakens it to the goal on the other side.1234 asm, for5 2, 46 57 asm, for8 3, 79 810 911 1, 4–6, 7–10The two boxes reach different statements,
at line 5 and at line 9, and turns both into the common last line . - (b) Take
: “ is even”, : “ is odd”, : “ is a multiple of ”, : “ is odd”, : “ is one more than a multiple of ”. The premise is the fact we may use. For : if for an integer , then . For : if , then , which is odd; and with for an integer , . By (a), . For instance, , and .
For real numbers
Solution. We have
Case
Case
- If
, then , whose negative is . - If
, then , so , whose negative is ; and .
Both inner cases reach the goal, so
For instance, at
For each claim, derive it with the rules of this
chapter, or break it by statements about a real number
- (a)
. - (b)
. - (c)
. - (d)
. - (e)
. - (f)
. - (g)
. - (h)
. - (i)
.
Solution.
- (a) Derive. Split on
line 1; in the case
, build with the premise .123 asm, for4 3, 25 46 asm, for7 68 1, 3–5, 6–7 (b) Break. Take
: “ ”, : “ ”, : “ ”. At , and are true ( , ) and is false, so is false: the counterexample set , is true.(c) Derive, with a split inside a case: the case
is itself a disjunction.123 asm, for4 35 asm, for6 asm, for7 2, 68 79 asm, for10 911 5, 6–8, 9–1012 1, 3–4, 5–11- (d) Derive. The goal
is a disjunction; the left side
can be built, as in Example (A disjunctive hypothesis splits into two implications), and then adds the other side.12 asm, for3 24 1, 35 2–46 5 (e) Break. Take
: “ ”, : “ ”, : “ ”. At , is true, since its hypothesis fails, so the premise is true; is true and false, so is false. The counterexample set is true.(f) Derive.
123 asm, for4 2, 35 46 asm, for7 68 1, 3–5, 6–7- (g) Derive. In the
second case the case’s assumption is an implication, and
the premise
fires it.123 asm, for4 35 asm, for6 5, 27 68 1, 3–4, 5–7 - (h) Derive, with a
split inside a case, inside a box. The goal is an
implication: open the box of
. Inside it, split on the premise; in its case , split again on the box’s assumption , which is available there.
Line 11 cites line 2, the assumption of the box
(i) Break. Take
: “ ”, : “ ”, : “ ”. At , is true, so the premise is true; is true and false, so is false. The counterexample set is true.(ii) and (e) are converses: the original derives and the converse breaks. (i) is a look-alike that drops the shared
from (h)’s conclusion, and breaks. (b) is a look-alike of Exercise (B1: The other distributive law), with the conclusion’s and traded.
Translate each argument into a sequent with the letters given, then derive it or break its form.
- (a) Let
be an integer. is even or is odd. If is even, then is even. If is odd, then is even. If is even, then is even. So is even. Letters: : “ is even”, : “ is odd”, : “ is even”, : “ is even”. - (b) Let
be a real number. If , then . If , then . And . So or . Letters: : “ ”, : “ ”, : “ ”. If the form breaks, say whether the conclusion is still true for every with , and which premise would repair the argument.
Solution.
- (a) The sequent is
. Split on the first premise; in the case the chain of two implications reaches .12345 asm, for6 2, 57 asm, for8 3, 79 4, 810 1, 5–6, 7–9 - (b) The sequent is
, and its form breaks: it affirms the consequent of two implications at once. Keep and , and replace by “ ”. Both implications then hold for every , and at the premise is true and is false, so the counterexample set , , , is true.
With the argument’s own content no number breaks it,
because
Derive each sequent. They are grouped by the move that does the main work.
Read the skeleton off the goal.
- 1.
. - 2.
. - 3.
. - 4.
. - 5.
.
Use a premise by its main connective.
- 6.
. - 7.
. - 8.
. - 9.
. - 10.
.
Cases end in the current goal.
- 11.
. - 12.
. - 13.
. - 14.
. - 15.
.
Solution. 1. Two
arrows at the top of the goal give two nested boxes;
inside,
2. No premises: the skeleton of the goal is two boxes, and everything inside comes from their assumptions.
3. Two boxes from the goal; inside,
4. Two boxes from the goal; the premise fires on a half of the outer assumption, and the implication it gives fires on the inner one.
5. Two boxes from the goal; the inner assumption fires on the outer one, and the premise on the result.
6. One box from the goal; inside,
each line is read off a main connective:
7. No box: the conjunction is taken apart, and its two halves feed the two implications.
8. The first premise needs its whole
hypothesis
9. Both halves of the assumption are
used, one by each premise, and the results meet in a
third
10. The only line mentioning
11. Split on the first premise; in
one case the premise
12. A box from the goal, then a
split inside it, each case ending in the current goal
13. A box from the goal, then a
split inside it; the current goal
14. The goal is a disjunction, so no
box can be opened first: the split comes first, as in Exercise (B3: Two cases, two conclusions)
(a), and each case opens its own
15. Split on the first premise; each
case builds both conjuncts of the goal, and
C. Going deeper
Let
Solution (Hint 1). The triangle
inequality bounds
Solution (Hint 2). In the case
Solution. We use two school facts:
for real numbers
By the first fact,
Case
Case
Both cases reach the goal, which proves the inequality.
The two cases exhaust all possibilities because they
are the two sides of the disjunction “
A split on signs would decide
Marking scheme. (10 points)
- 2: states the disjunction
or and says it holds for all reals. - 3: in the first case, removes the outer absolute
value correctly and derives
from the triangle inequality for . - 3: in the second case, the same with the roles
exchanged, including
. - 2: explains the four sign cases as a split inside each case of another.
Fatal errors (0 for the step): using
Here is a proof, by four cases, that
Case 1:
. Then . Case 1a:
. Then , and is or . Since and , we get . Case 1b:
. Then , and , so . Case 2:
. Then . Case 2a:
. Then , and , so . Case 2b:
. Then . Since and , we have , so , because and . All four cases give
.
- (a) Is the statement true?
- (b) Find the line that is not justified, and name the rule whose conditions it breaks.
- (c) Show with specific numbers that the step fails.
- (d) Repair Case 2b.
Solution.
(a) Yes. For instance, it follows from Example (The triangle inequality by cases) applied to
and , since (shown in the solution of Exercise (C1: Challenge: The reverse triangle inequality)). So the question is not whether the conclusion holds but whether this argument proves it.(b) The sentence “Since
and , we have ” in Case 2b. The assumption is the assumption of Case 1. In derivation terms, it opens the first box of the outer , and Case 2b lies inside the second box, which is opened by . Once the first box has closed, its lines are not available (the scope rule of Definition 1.4.2), so Case 2b may not cite : the rule broken is , each of whose boxes may cite only lines available at it by the scope rule: its own assumption, what has been derived inside it, and what was available before the box opened; so nothing from the first box, which has closed. The sentence is the reasoning of Case 1b copied into Case 2b, where its assumption is no longer in force. So the box of Case 2 does not reach the goal from the lines available to it, and the final has no right to cite it.(c) Take
and , which is Case 2b. Then , which is not , and . The conclusion of Case 2b still holds here ( ), but the step used to reach it is false.(d) In Case 2b,
and , so and . The number is or . Since , we have . Since , we have . So in either case , using only the assumptions of Case 2b.
Derive
Solution. The chart would build the
conjunction by
Line by line: 1 is the premise; 2 is the assumption
of the first case; 3 and 4 are
With premise
Marking scheme. (10 points)
- 2: splits on the premise by
, with two boxes opened by its two sides. - 2: in each box, takes the assumption apart by
into both conjuncts. - 2: in each box, uses
to build from the side in hand, with the correct schema. - 2: in each box, builds the goal by
, so that both boxes end in the same line, the goal. - 2: the
line cites the disjunction and both boxes as ranges, and the final sentences name the changed steps (the lines, now building , and the lines, now with on the left).
Fatal errors (0 for the step): a line in one box citing a line of the other box; a conclusion drawn inside one box only and then used outside it.
A second route is also correct: split the premise
twice, once ending both boxes in
A search for
Solution (Hint 1). Inside the box, what is the current goal, and which available line is a disjunction?
Solution (Hint 2). Line 5 is
Solution. The moves are two. First,
the box of line 4 was read off the goal:
Line 7 cites line 4, the assumption of the outer box,
which contains line 7. Line 10 is a line of the box
R. Review
Let
Solution. The sequent is
Line 4 writes
Show that
Solution. Premise-directed, both
premises are conjunctions and are taken apart by
The chain of lines 7 and 8 was found backwards, from
the subgoal
Is
Solution. Yes. The goal’s main
connective is the outer
The derivation has no premises, so it shows