# Overview

Section 2.6 introduces a method for abbreviating derivations. The software calls it “queuing.” Section 2.7 discusses some theorems. Section 2.8 introduces derived rules.

# Queuing

Here is the idea. Consider the following derivation:

$$P{\mathbin{\wedge}}Q\ .\ P{\mathbin{\rightarrow}}R\ {\therefore\ }R$$

1Show$$R$$

2$$P{\mathbin{\wedge}}Q$$pr

3$$P$$2 s

4$$P{\mathbin{\rightarrow}}R$$pr

5$$R$$4 5 mp

65 dd

We have already seen two ways in which this can be shortened: we can use the premises directly instead of bringing them down; we can apply ‘dd’ to the end of line (5) instead of entering it on a separate line:

1Show$$R$$

2$$P$$pr1 s

3$$R$$2 pr2 mp dd

Let’s pause and consider both of these shortcuts.

Line (2) combines two steps into one:

• bring down PR2 (to get $$P{\mathbin{\wedge}}Q$$)
• to the result above, apply S (to get $$P$$)

Line (3) also combines two steps into one:

• to line (2) and the result of bringing down PR2, apply MP (to get $$R$$)
• given that result, box and cancel by DD

You can combine steps like this on any line. So, for example,

1Show$$R$$

2$$R$$pr1 sl pr2 mp dd

To unpack this, work from left to right:

• bring down PR1
• to the result, apply SL (to get $$P$$);
• to the result ($$P$$) and PR2, apply MP (to get $$R$$)
• given that result ($$R$$), box and cancel by DD

Here is a second example.

$$P{\mathbin{\vee}}Q\ .\ {\mathbin{\sim}}Q{\mathbin{\wedge}}R {\therefore\ }P$$

1Show$$P$$

2$$P{\mathbin{\vee}}Q$$pr

3$${\mathbin{\sim}}Q{\mathbin{\wedge}}R$$pr

4$$P$$3 sl 2 mtp

5dd

On line (4), we have combined a two steps into one line:

• to (3), apply SL (to get $${\mathbin{\sim}}Q$$)
• to the result and line (2), apply MTP (to get $$P$$)

We could compress the derivation yet further, if we wished, e.g.,

1Show$$P$$

2$$P$$pr2 sl pr1 mtp dd

Queuing makes derivations more difficult to read. I recommend using it judiciously if you feel quite confident in your ability to construct derivations. Otherwise, I don’t recommend using it at all.

# Theorems and Derived Rules

Consider the theorem 24 (T24 in the software and the book, problem 2.024 in the software):

$P{\mathbin{\wedge}}Q{\mathbin{\leftrightarrow}}Q{\mathbin{\wedge}}P$

This theorem tells us that the order in which conjuncts occur does not matter to the truth of a conjunction. Note that the same would not be true if we replaced the $${\mathbin{\wedge}}$$’s with $${\mathbin{\rightarrow}}$$’s.

Here is a derivation of the theorem:

1Show$$P{\mathbin{\wedge}}Q{\mathbin{\leftrightarrow}}Q{\mathbin{\wedge}}P$$

2Show$$P{\mathbin{\wedge}}Q{\mathbin{\rightarrow}}Q{\mathbin{\wedge}}P$$

3$$P{\mathbin{\wedge}}Q$$ass cd

4$$P$$3 sl

5$$Q$$3 sr

6$$Q{\mathbin{\wedge}}P$$4 5 adj cd

7Show$$Q{\mathbin{\wedge}}P{\mathbin{\rightarrow}}P{\mathbin{\wedge}}Q$$

8$$Q{\mathbin{\wedge}}P$$ass cd

9$$Q$$8 sl

10$$P$$8 sl

11$$P{\mathbin{\wedge}}Q$$9 10 adj cd

12$$P{\mathbin{\wedge}}Q{\mathbin{\leftrightarrow}}Q{\mathbin{\wedge}}P$$2 7 cb dd