Derivation Rules for Propositional Logic

Proof Sequence

A proof sequence is a sequence of wffs in which each wff is either a hypothesis or the result of applying one of the formal system's derivation rules to earlier wffs in the sequence.

Using formal logic to prove that \(Q\) is a valid conclusion from \(P_1, ..., P_n\), we must produce a proof sequence of the form:

\(P_1\)     (hypothesis)
\(P_2\)     (hypothesis)
\(P_n\)     (hypothesis)
\(wff_1\)     (obtained by applying a derivation rule to earlier wffs.)
\(wff_2\)     (obtained by applying a derivation rule to earlier wffs.)
\(Q\)     (obtained by applying a derivation rule to earlier wffs.)

Derivation Rules for Propositional Logic

The derivation rules for propositional logic fall into two categories, equivalence rules and inference rules. Equivalence rules allow individual wffs to be rewritten, while inference rules allow new wffs to be derived from previous wffs in the proof sequence.

• Equivalence Rules:
Equivalence rules state that certain pairs of wffs R and S are equivalent. Remember that \(R ⇔ S\) means that \(R ↔ S\) is a tautoloy and that \(S\) can be substituted for \(R\) in any wff with no change to the truth value of that wff. Equivalence rules are therefore truth-preserving; a true wff remains true if such a substitution is done within it.

Table 1: Equivalence Rules
Expression Equivalent to Name/Abbrevision for Rule
\(P ∨ Q\)
\(P ∧ Q \)
\(Q ∨ P\)
\(Q ∧ P \)
Commutative -- comm
\((P ∨ Q) ∨ R\)
\((P ∧ Q) ∧ R \)
\(P ∨ (Q ∨ R)\)
\(P ∧(Q ∧ R) \)
Associative -- ass
\( (P ∨ Q)' \)
\( (P ∧ Q)' \)
\( P' ∧ Q' \)
\( P' ∨ Q' \)
De Morgan's Laws -- De Morgan
\( P → Q\) \( P' ∨ Q\) Implication -- imp
\(P\) \((P')'\) Double negation -- dn
\(P ↔ Q\) \((P → Q) ∧ (Q → P)\) Definition of equivalence -- equ

The equivalence rules allow substitution in either direction. For example, we replaced \(A' ∨ B'\) with \((A ∧ B)'\), but in some other proof sequence, using the same rule, we might replace \((A ∧ B)'\) with \(A' ∨ B'\).

• Inference Rules:

Inference rules say that if one or more wffs that match the first part of the rule pattern are already part of the proof sequence, we can add to the proof sequence a new wff that matches the last part of the rule pattern. Table 2 shows the propositional inference rules we will use, again along with their identifying names.

Table 2: Inference Rules
From Can Derive Name/Abbrevision for Rule
\(P, P → Q\) \( Q \) Modus ponens -- mp
\(P → Q, Q'\) \( P' \) Modus tollens -- mt
\(P,Q\) \( P ∧ Q \) Conjunction -- con
\(P ∧ Q\) \( P,Q \) Simplification -- sim
\(P\) \(P ∨ Q \) Addition -- add

Unlike equivalence rules, inference rules do not work in both directions. We cannot "reverse" the addition rule in Table 2; from \(P ∨ Q\), we cannot infer eithr \(P\) or \(Q\).

Example 1

Let's have a complete proof of an argument.Using propositional logic, prove that the argument

\(A ∧ (B → C) ∧ [(A ∧ B) → (D ∨ C')] ∧ B → D\)

is valid.

We must produce a proof sequence that begins with the hypotheses and ends with the conclusion. There are four hypotheses, so this gives us lots of "ammunition" to use in the proof. The beginning of the proof is easy enough because it just involves listing the hypotheses:

1. \(A\) (hyp)
2. \(B → C\) (hyp)
3. \((A ∧ B) → (D ∨ C')\) (hyp)
4. \(B\) (hyp)

Our final goal is to arrive at \(D\), the conclusion. But without even looking ahead, there are a couple of fairly obvious steps we can take that may or may not be helpful:

5. \(C\) (2,4,mp)
6. \(A ∧ B\) (1,4,con)
7. \( D ∨ C'\) (3,6,mp)

At least at this point we have introduced \(D\), but it's not by itself. Note that from step 5 we have \(C\), which we haven't made use of. If only we had \(C → D\), we'd be home free. Ah, look at the form of step 7; it's a disjunction, and the implication rule says that we can transform a disjunction of a certain form into am implication. The disjunction must have a negated wff on the left. We can do that:

8. \(C' ∨ D\) (7,comm)
9. \(C → D\) (8,imp)


10. \(D\) (5,9, mp)

Example 2

Using propositional logic, prove the validity of the argument.

\( [(A ∨ B') → C] ∧ (C → D) ∧ A → D \)

1. \((A ∨ B') → C\) (hyp)
2. \(C → D\) (hyp)
3. \(A\) (hyp)

4. \( A ∨ B' \) (3 add)
5. \(C\) (1,4 mp)
6. \(D\) (2,5,mp)

Deduction Method

Suppose the argument we seek to prove has the form:

\( P_1 ∧ P_2 ∧ P_3 ∧ ... ∧ P_n → (R → S)\)

where the conclusion is itself an implication. Instead of using \(P_1,...,P_n\) as the hypotheses and deriving \(R → S\), the deduction method lets us add \(R\) as an additional hypothesis and then derive \(S\). In other words, we can instead prove:

\(P_1 ∧ P_2 ∧ P_3 ∧ ... ∧ P_n ∧ R → S\)

Reminder: Use the deduction method when the conclusion of what you want to prove is an implication.

Example 3

Using propositional logic, prove that the following is a valid argument.

\( (A' ∨ B) ∧ (B → C) → (A → C)\)
1. \(A' ∨ B\) (hyp)
2. \(B → C\) (hyp)
3. \(A\) (hyp)

4. \( A → B\) (1, imp)
5. \(B\) (3,4 mp)
6. \(C\) (2,5 mp)


1. Use propositional logic to prove
\((A → B) ∧ (C' ∨ A) ∧ C → B\)


saylor academy