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 ∧ Q . P → R ∴ 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 ∧ 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 ∨ Q .  ∼ Q ∧ R∴ P

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

• to (3), apply SL (to get  ∼ 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 ∧ Q ↔ Q ∧ 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 ∧’s with →’s.

Here is a derivation of the theorem: