[SL11] Derivations

Now you will learn how to make derivations in sentential logic. A derivation displays step by step reasoning from premises to conclusion. Each step along the way follows the rules.

The sort of system of rules you will study is often called a natural deduction system because it is somewhat like the way people actually deduce conclusions from premises. It isn't really natural -- it is an artificial, formal system -- but a natural deduction system can be easier to use and understand than other available methods.

§1. An example derivation

Here is an example of a derivation in our system:

This example shows, step by step, that "C" follows from "(A & D)" together with "(A → (B & C))". That is, starting with "(A & D)" and "(A → (B &C))" one can reach the conclusion "C" by following the rules of the system. In short, "C" is derivable in our system from "(A & D)" and "(A → (B & C))".

In symbols:

(A & D), (A → (B & C)) ⊢ C

The symbol "⊢" is sometimes called the "turnstile". We will use it to mean that the formula on the right is derivable in our natural deduction system from the formulas, if any, on the left.

§2. The parts of a derivation

Let's examine the sample derivation in detail.

The middle column is a numbered list of well-formed formulas of sentential logic. This is the heart of the derivation. Each formula in the list is numbered. In this case there are five formulas, numbered from 1 to 5.

The right column tells us what rule is followed. In this derivation three different rules are used. In line 1 "(A & D)" was written down by Rule A, the Rule of Assumption. The Rule of Assumption is also used on line 2. On lines 3 and 5 Rule &E is followed, and line 4 employs rule →E. There are twelve different rules in all in our system.

The left column contains a list of zero or more dependencies. For example, line 1 depends on line 1, and line 5 depends on lines 1 and 2. We'll see more about what the dependencies mean as we go along.

In short, at each step in making a derivation you write down three things: a formula (with a line number), a note on the right saying which rule you have applied, and, on the left, a list of dependencies (if any).

§3. Three rules

You have just seen three rules in action. Let us see more precisely how to use each of these three rules.

The Rule of Assumption says that you can write down any well-formed formula of SL you like. The dependency is that formula itself.

For example, we just saw this rule used twice:

It may seem odd to be able to write down any formula you want at any time. But that does not mean you can derive anything at all. The rule does not merely say you can write down any formula. The rule says that you can write down any formula depending on itself.

In effect, for any formula φ, the rule lets you say that φ follows from itself; φ is derivable from itself.

In this case, for example, line 1 means that "(A & D)" is derivable from "(A & D)":

(A & D) ⊢ (A & D)

And line 2 means that "(A → (B & C))" is derivable from "(A → (B & C))":

(A → (B & C)) ⊢ (A → (B & C))

The & Elimination Rule, &E, says that if you have a line which is a conjunction you can write down either of the conjuncts. In other words, if you have a line (φ&ψ), you can write down φ or ψ.

The new line depends on everything the conjunction depends on.

That rule is used at line 3 of the sample derivation:

One can use &E to write down "A" at line 3 because line 1 is a conjunction, "(A & D)". Line 3 depends on everything line 1 depends on. Line 1 depends only on line 1. So line 3 depends only on line 1. The annotation on the right says that you applied &E to line 1.

The → Elimination Rule, →E, says that you can write down ψ if you have a line (φ→ψ) and another line φ. The new formula ψ depends on everything that (φ→ψ) depends on, together with everything that φ depends on. This rule is commonly called Modus Ponens.

But we call it the → Elimination Rule to emphasize the similarity between this and other elimination rules, such as &E. Using an elimination rule, one writes down part of an earlier formula. So elimination rules let one move from longer formulas to shorter formulas.

→E is used at line 4 of the sample derivation:

In this case, we have "A" on line 3, and "(A → (B & C))" on line 2, so we can write down "(B & C)", depending on everything line 2 and line 3 depend on.

Now you have seen 3 rules: &E, →E, and A. It is time to prove some things yourself! Make derivations to show the following, using only these 3 rules, if you can. Try not to look at the answers until you have finished your derivation, or have decided that it can't be done.

Show the following using only &E, →E, and A.

  1. (A & B) ⊢ A
  2. ((A ∨ B) & (B→A)) ⊢ A
  3. (A → (B & C)), A ⊢ B
  4. A,B ⊢ (A & B)
  5. A, (A → (B → (C → (D → (E → F))))) ⊢ F
previous tutorial next tutorial


© 2004-2024 Joe Lau & Jonathan Chan