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\)

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:

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,

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\)

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.,

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: