Valid Moves ⊢
Chapter 5 · pp. 146–225

Sentential Logic: Derivations

The syntactic side of SL. Instead of searching through truth-value assignments, we show a conclusion follows by deriving it step by step, using eleven rules that each look only at the form of sentences.

How to type a derivation
Derive: A ⊃ C
| A ⊃ B          Assumption
| B ⊃ C          Assumption
| | A            A / ⊃I
| | B            1, 3 ⊃E
| | C            2, 4 ⊃E
| A ⊃ C          3–5 ⊃I

Each | is a scope line. Type > for ⊃, v for ∨, = for ≡.

Section 5.1

The derivation system SD

pp. 146–174 · exercises 5.1E

Truth-tables and trees are semantic: they look for truth-value assignments. Derivations are syntactic: they track the kind of step-by-step reasoning people use when they argue, with each step licensed by a rule about sentence forms.

Eleven rules

Reiteration, plus an introduction and an elimination rule for each connective. Introduction rules produce a sentence with that main connective; elimination rules start from one.

Assumptions and scope

Primary assumptions sit at the top, against the main scope line. An auxiliary assumption starts a new scope line and a subderivation. The book annotates it with the rule that will discharge it, as in A / ⊃I; only ⊃I, ~I, ~E, ∨E and ≡I use subderivations.

AccessibilityA sentence or subderivation is accessible at line n when every scope line to its left also continues to line n. Once a subderivation ends, nothing inside it can be cited again; only the whole subderivation can be cited, by range.

Common mistakes

  • Applying a rule of inference to part of a line. &E works on B & C, not on A ⊃ (B & C).
  • Citing a line inside a subderivation that has already ended.
  • Assuming the goal "because you can assume anything". You can, but the assumption has to be discharged, and the goal ends up inside its scope.

Justification format

Assumptionprimary assumption
A / ~Eauxiliary assumption, to be discharged by ~E
3 &Eone line cited
1, 4 ⊃Etwo lines cited
2–6 ⊃Ia subderivation cited by range
4, 5–7, 8–10 ∨Ea line and two subderivations
Reference

The rules of SD

▷ marks the sentence the rule lets you enter. Bars show subderivations.

Section 5.2

Basic concepts of SD

pp. 175–178 · exercises 5.2E
Derivable in SDΓ ⊢ P: there is a derivation whose primary assumptions are all in Γ and where P lies in the scope of those assumptions only.
Valid in SDThe conclusion is derivable from the set of premises.
Theorem in SD⊢ P: derivable from the empty set, with no primary assumptions. Such a derivation is a proof.
Equivalent in SDEach sentence is derivable from the other's unit set. Two derivations are needed unless the sentences are identical.
Inconsistent in SDSome sentence and its negation are both derivable from Γ.

A derivation shows that one of these properties holds. Failing to find a derivation shows nothing: you may simply not have found it yet. Chapter 6 proves that SD matches the semantic notions exactly (soundness and completeness).

Semantic and syntactic pairs

Chapter 3Chapter 5
TF-truetheorem in SD
TF-equivalentequivalent in SD
TF-inconsistentinconsistent in SD
TF-validvalid in SD
TF-entailment ⊨derivability ⊢

There's no standard syntactic counterpart of TF-falsity or indeterminacy, though one is easy to define.

Section 5.3

Strategies for constructing derivations

pp. 179–213 · exercises 5.3E

Work from both ends. From the bottom, ask which rule could produce the current goal and write its requirements as subgoals (the book marks them G). From the top, derive whatever the accessible sentences make easy.

The book's strategies, in order

  1. If the goal can be obtained by Reiteration, do that.
  2. If it can be obtained by non-subderivation rules, do that.
  3. Otherwise use the subderivation rule that matches the goal's main connective: ⊃I for a conditional, ≡I for a biconditional, ~I for a negation.
  4. If nothing else works, try ~E (assume the negation of the goal) or ∨E (if a disjunction is accessible).
  5. When using a negation rule, pick an accessible negation as the ~ Q you aim to contradict.

When two strategies both look possible, the book's advice is to pick one and go. Backing out is cheap.

Goal analysis, by main connective

GoalTry
P & Qderive P and Q, then &I
P ∨ Qderive P or Q, then ∨I; else ∨E or ~E
P ⊃ Qassume P, derive Q, ⊃I
P ≡ Qtwo subderivations, ≡I
~ Passume P, find Q and ~ Q, ~I
atomic⊃E, &E, ≡E, ∨E, or ~E
Section 5.4

The derivation system SD+

pp. 214–225 · exercises 5.4E

SD+ adds convenience rules. It proves exactly the same things as SD, but often in fewer lines.

Rules of inference (MT, HS, DS) work on whole lines, like SD's rules. Rules of replacement are two-way and may replace any sentential component, including the whole sentence. Each application needs its own line, and the component must match the rule's form exactly, sometimes after a DN step to make it fit.

Rules of inference

MTP ⊃ Q, ~ Q ▷ ~ P
HSP ⊃ Q, Q ⊃ R ▷ P ⊃ R
DSP ∨ Q, ~ P ▷ Q  ·  P ∨ Q, ~ Q ▷ P

Rules of replacement (◁▷)

ComP & Q ◁▷ Q & P  ·  P ∨ Q ◁▷ Q ∨ P
AssocP & (Q & R) ◁▷ (P & Q) & R  ·  same for ∨
ImplP ⊃ Q ◁▷ ~ P ∨ Q
DNP ◁▷ ~ ~ P
DeM~ (P & Q) ◁▷ ~ P ∨ ~ Q  ·  ~ (P ∨ Q) ◁▷ ~ P & ~ Q
IdemP ◁▷ P & P  ·  P ◁▷ P ∨ P
TransP ⊃ Q ◁▷ ~ Q ⊃ ~ P
ExpP ⊃ (Q ⊃ R) ◁▷ (P & Q) ⊃ R
DistP & (Q ∨ R) ◁▷ (P & Q) ∨ (P & R)  ·  P ∨ (Q & R) ◁▷ (P ∨ Q) & (P ∨ R)
EquivP ≡ Q ◁▷ (P ⊃ Q) & (Q ⊃ P)  ·  P ≡ Q ◁▷ (P & Q) ∨ (~ P & ~ Q)
Tool

Derivation checker

Build a derivation one line at a time: type the sentence, click the rule, then click the line numbers it cites. Scope lines are handled for you. Every line is checked as you go. Pick an exercise to load its premises and goal; your work is saved in this browser.

Or type the whole derivation as text

One line per derivation line. Each | is a scope line. Justifications look like Assumption, A / ⊃I, 1, 3 ⊃E, 2–4 ~I.

Practice

Practice sets for Chapter 5

Quick checks on rules and accessibility. For full derivations, use the exercises in the checker above.

For our session

Discussion questions

  1. The book says Reiteration and ~I could be dropped from SD without losing anything. Show how to do without each.
  2. Why must a rule of inference apply to a whole line, while a rule of replacement can apply to a part?
  3. Deriving Q and ~ Q inside a subderivation doesn't show the primary assumptions are inconsistent. What does it show?
  4. If you can't find a derivation, what can you conclude? Compare with a truth-tree that won't close.
  5. Why would anyone want SD+ if it proves nothing new?
Your notes

Questions for our session

Saved in this browser only.

Supplementary reading

Nothing assigned from other texts for this chapter yet.