3.5.2. An example

As an example of the use of the basic system, let us look at the further derivation for the argument of 3.2.x 2d that was promised in 3.3.3. The possible ways of proceeding at each stage are described in the commentary at the left.


Stage 1. 

We have two premises and a goal and we look to any of them for our starting point. But our premises are negations and can be exploited only in a reductio argument—that is, only when the goal is ⊥. So we must begin by planning for the goal, and RAA is the rule for doing that.

  │¬ (A ∧ B)  
│¬ (C ∧ ¬ B)
├─
├─
│¬ (A ∧ C)

Stage 2.

After applying RAA, the goal is ⊥. There is no rule to plan for such a goal; but we have three resources, and we are now in a position to exploit any one of them. The rule Ext for exploiting conjunctions is easy, and it sometimes leads to a shorter derivation to do that as soon as possible, so that is what we will do. But there would be nothing wrong with exploiting either of the premises with CR; we will eventually need to do that in any case.

  │¬ (A ∧ B)
│¬ (C ∧ ¬ B)
├─
││A ∧ C
│├─
││
││
││
│├─
││⊥ 1
├─
1 RAA │¬ (A ∧ C)

Stage 3.

The use of Ext has given us two new active resources in addition to the two premises, and our goal is still ⊥. The two added resources are atomic sentences and can never be exploited, so we must now exploit one of the premises by CR. Either one will do, but let us choose the first.

│¬ (A ∧ B)
│¬ (C ∧ ¬ B)
├─
││A ∧ C 2
│├─
2 Ext ││A
2 Ext ││C
││
││
││
│├─
││⊥ 1
├─
1 RAA │¬ (A ∧ C)

Stage 4.

This use of CR has set our goal as the conjunction A ∧ B, and we can plan to get that by Cnj. Indeed, that’s all we can do because we cannot exploit the second premise until our goal is again ⊥.

│¬ (A ∧ B) 3
│¬ (C ∧ ¬ B)
├─
││A ∧ C 2
│├─
2 Ext ││A
2 Ext ││C
││
│││
│││
│││
││├─
│││A ∧ B 3
│├─
3 CR ││⊥ 1
├─
1 RAA │¬ (A ∧ C)

Stage 5.

The use of Cnj has divided the gap into two open gaps, and we could go on to work on either of them. The goal of the first is also one of its resources, so we can close it immediately by QED and that’s what we will do. But it would be fine to leave it open while we developed the second gap. It would even be possible to develop the first gap by planning for its goal with IP. While, of course, that would make for a longer derivation, we would eventually run out of things to do and would be forced to notice that the gap could be closed. (It would close on different grounds but, because the rules are safe and sufficient, there would be some reason for closing it.)

│¬ (A ∧ B) 3
│¬ (C ∧ ¬ B)
├─
││A ∧ C 2
│├─
2 Ext ││A
2 Ext ││C
││
││││
││││
││││
│││├─
││││A 4
│││
││││
││││
││││
│││├─
││││B 4
││├─
4 Cnj │││A ∧ B 3
│├─
3 CR ││⊥ 1
├─
1 RAA │¬ (A ∧ C)

Stage 6.

Now that the first gap is closed by RAA, we have only the second to work on. And, since the goal of this gap is not ⊥, we cannot exploit the second premise. Moreover, our other two resources are atomic sentences. So we must plan for the atomic goal, and the rule for doing that is IP.

│¬ (A ∧ B) 3
│¬ (C ∧ ¬ B)
├─
││A ∧ C 2
│├─
2 Ext ││A (5)
2 Ext ││C
││
││││●
│││├─
5 QED ││││A 4
│││
││││
││││
││││
│││├─
││││B 4
││├─
4 Cnj │││A ∧ B 3
│├─
3 CR ││⊥ 1
├─
1 RAA │¬ (A ∧ C)

Stage 7.

The use of IP has made our goal ⊥ again, so we are forced to turn to our resources for guidance. We have added one, ¬ B; but it is the negation of an atomic sentence so, like A and C, it will never be exploited. But, since we are again working on a reductio argument, we can now exploit the second premise by CR.

│¬ (A ∧ B) 3
│¬ (C ∧ ¬ B)
├─
││A ∧ C 2
│├─
2 Ext ││A (5)
2 Ext ││C
││
││││●
│││├─
5 QED ││││A 4
│││
│││││¬ B
││││├─
│││││
│││││
│││││
││││├─
│││││⊥ 6
│││├─
6 IP ││││B 4
││├─
4 Cnj │││A ∧ B 3
│├─
3 CR ││⊥ 1
├─
1 RAA │¬ (A ∧ C)

Stage 8.

This exploitation of the of the second premise by CR has left us with active resources that are all atomic sentences or negated atomic sentences. They can never be exploited, but our goal is a conjunction so we can plan to derive it by Cnj.

│¬ (A ∧ B) 3
│¬ (C ∧ ¬ B) 7
├─
││A ∧ C 2
│├─
2 Ext ││A (5)
2 Ext ││C
││
││││●
│││├─
5 QED ││││A 4
│││
│││││¬ B
││││├─
││││││
││││││
││││││
│││││├─
││││││C ∧ ¬ B 7
││││├─
7 CR │││││⊥ 6
│││├─
6 IP ││││B 4
││├─
4 Cnj │││A ∧ B 3
│├─
3 CR ││⊥ 1
├─
1 RAA │¬ (A ∧ C)

Stages 9-10.

Cnj has divided the gap in two, but each of these two open gaps can be closed by QED, and we will go on to do that at the next two stages. Each gap also has a goal that we might plan for; and, as noted earlier, there would be nothing wrong with doing that. In fact, doing it in this case would not lead to a much longer derivation since, once we planned for the goals of these gaps, there would be nothing more we could do with either gap except close it.

│¬ (A ∧ B) 3
│¬ (C ∧ ¬ B) 7
├─
││A ∧ C 2
│├─
2 Ext ││A (5)
2 Ext ││C
││
││││●
│││├─
5 QED ││││A 4
│││
│││││¬ B
││││├─
│││││││
│││││││
││││││├─
│││││││C 8
││││││
│││││││
│││││││
││││││├─
│││││││¬ B 8
│││││├─
8 Cnj ││││││C ∧ ¬ B 7
││││├─
7 CR │││││⊥ 6
│││├─
6 IP ││││B 4
││├─
4 Cnj │││A ∧ B 3
│├─
3 CR ││⊥ 1
├─
1 RAA │¬ (A ∧ C)

The complete derivation is shown below. You can replay its development by moving the cursor across the series of numbers above it.

0 1 2 3 4 5 6 7 8 9 10
¬ (A ∧ B) 3
¬ (C ∧ ¬ B) 7
├─
A ∧ C 2
├─
2 Ext A (5)
2 Ext C (9)
├─
5 QED │A 4
¬ B (10)
├─
├─
9 QED C 8
├─
10 QED ¬ B 8
├─
8 Cnj C ∧ ¬ B 7
├─
7 CR 6
├─
6 IP B 4
├─
4 Cnj A ∧ B 3
├─
3 CR 1
├─
1 RAA ¬ (A ∧ C)
Glen Helman 16 Jul 2012