Transformations More about propositional logic

If a formula A logically entails a formula B and B also entails A, written  A ⊣⊢ B,  then we say that A and B are logically equivalent. In propositional logic, what this amounts to is that they have the same truth table, or express the same truth function. It is a fundamental feature of logic that if two formulae are logically equivalent then either may replace the other in any well-formed context without changing the truth value or inferential properties of anything. That is, if A and B are equivalent, and if A occurs as a subformula of some longer formula C, then the result of replacing A in that context by B is a formula equivalent to C.

This principle of replacement of equivalents is obviously correct on the semantic account of logical validity, since the truth value of C on any chosen interpretation may depend on the truth value of its subformula A but not on how A comes to have that truth value, so substituting any other formula B with the same truth value can have no effect on the truth value of the whole. On the syntactic side of the street, however, things are not quite so obvious. The fact that replacement of equivalents preserves the existence of deductions calls for a proof, which for present purposes we assume done.

Some of the important equivalences involving conjunction (AND) and disjunction (OR) are:

1. p AND p   ⊣ ⊢   p
2. p AND q   ⊣ ⊢   q AND p
3. (p AND q) AND r   ⊣⊢   ⊣ ⊢ p AND (q AND r)
4. p OR p   ⊣ ⊢   p
5. p OR q   ⊣ ⊢   q OR p
6. (p OR q) OR r   ⊣ ⊢   p OR (q OR r)
7. p AND (p OR q)   ⊣ ⊢   p
8. p OR (p AND q)   ⊣ ⊢   p
9. p OR (q AND r)   ⊣ ⊢   (p OR q) AND (p OR r)
10. p AND (q OR r)   ⊣ ⊢   (p AND q) OR (p AND r)

The diligent reader may click on the turnstiles to verify these sequents with the proof editor.

In the light of the first threee of these, the conjunction of a set {A₁, ..., A_n} of formulae is logically independent of the order in which they occur, how many times each is repeated and how the compound conjunction is parenthesised. By equivalences 4 – 6, the same is true of multiple disjunctions. The upshot of that is that we can justifiably be casual about writing a big conjunction (or a big disjunction) as   A₁ AND ... AND A_n   (respectively   A₁ OR ... OR A_n)  without internal parentheses and with the conjuncts in, say, alphabetical order (or any other order we choose).

The last two, 9 and 10, are also useful. If we have a formula in which a lot of conjunction and disjunction operations occur all mixed up, by applying these distribution principles we can transform it into an equivalent in which all the disjunction happens outside the conjunction, or vice versa if we wish.

Negation gives rise to some more important equivalences, and more fun for the diligent reader. First, a negated conjunction is equivalent to the disjunction of the negated conjuncts, and vice versa. These duality principles are known in the literature of logic as De Morgan's laws:

11. NOT(A AND B)   ⊣ ⊢   NOTA OR NOTB
12. NOT(A OR B)   ⊣ ⊢   NOTA AND NOTB

Using these and the equivalence between NOTNOTA and A, it is easy to derive the variants:

• NOT(NOTA AND B)   ⊣ ⊢   A OR NOTB
• NOT(NOTA AND NOTB)   ⊣ ⊢   A OR B
• NOT(NOTA OR B)   ⊣ ⊢   A AND NOTB
• NOT(NOTA OR NOTB)   ⊣ ⊢   A AND B

Negated (and unnegated) conditionals can be transformed similarly:

13. NOT(A IMP B)   ⊣ ⊢   A AND NOTB
14. A IMP B   ⊣ ⊢   NOTA OR B

It is clear that by repeatedly applying 13 and 14, the implication connective can be removed from formulae altogether without changing their semantics. Similarly, repeated applications of the De Morgan dualities can be used to drive negation inside AND and OR until it applies only to atoms.

An atom such as p or a negated atom such as NOTq is called a literal. So every formula has an equivalent built up out of literals by compounding under AND and OR. Such a formula is said to be in negation normal form or NNF. By equivalences 7 and 8, together with appeals to 1 – 6 as required, we may further regularise any formula in NNF by pushing all occurrences of AND inside OR or vice versa. A formula in NNF in which OR never occurs inside the scope of AND is a disjunction

A₁  OR  ...  OR  A_n

where each of the constituent disjuncts A_i is a conjunction

B₁  AND  ...  AND  B_k

where in turn each B_j is a literal. Such a formula is in disjunctive normal form (DNF). Even more important is the dual CNF or conjunctive normal form. A formula in CNF is a conjunction of (one or more) disjunctions of (one or more) literals. A disjunction of literals is known as a clause, so every formula is equivalent to the conjunction of a set of clauses.

For example, consider the formula

(p IMP q) IMP (r OR NOT(NOTp OR s))

This may be transformed into equivalent forms as follows. First turn the main connective from IMP into OR, negating the antecedent in accordance with equivalence 14 above. Also rewrite the negated disjunction NOT(NOTp OR s) using the appropriate variant of 12:

NOT(p IMP q) OR r OR (p AND NOTs)

Rewrite ¬(p IMP q) as p AND NOTq by 13:

(p AND NOTq) OR r OR (p AND NOTs)

Now the formula is in DNF. To turn it into a CNF equivalent, apply 5 and 9 to (p AND NOTq) OR r:

((p OR r) AND (NOTq OR r)) OR (p AND NOTs)

and use 5 and 9 again:

(p OR r OR (p AND NOTs)) AND (NOTq OR r OR (p AND NOTs))

and again:

(p OR r OR p) AND (p OR r OR NOTs) AND (NOTq OR r OR p) AND (NOTq OR r OR NOTs)

This is in CNF, being a conjunction of disjunctions of literals. However, it can be simplified by applying equivalences 4 – 6 to the first of the four clauses:

(p OR r) AND (p OR r OR NOTs) AND (NOTq OR p OR r) AND (NOTq OR r OR NOTs)

The second clause is now subsumed by the first, making it redundant, so it can be eliminated by appeal to equivalence 7:

(p OR r) AND (NOTq OR p OR r) AND (NOTq OR r OR NOTs)

Finally, re-shuffling NOTq OR p OR r and applying 7 again:

(p OR r) AND (NOTq OR r OR NOTs)

Evidently the same sort of transformation can be applied to any formula. Moreover, any sequent  X ⊢ A  is equivalent to  X, NOTA ⊢ BAD  which by reduction to CNF can be turned into an equivalent  Y ⊢ BAD  where Y is a set of clauses. This means that any mechanism for detecting inconsistency in sets of clauses is in effect sufficient to carry out deduction; this fact is the basis for many automated reasoning systems, so it is very important to the mechanisation of logic.

It is easy to check that the two formulae  (p IMP q) IMP (r OR NOT(NOTp OR s))  and  (p OR r) AND (NOTq OR r OR NOTs)  are indeed equivalent by examining their truth tables or by constructing a tableau. It is less easy to derive each from the other by natural deduction, though it can of course be done. For that kind of reason, if the natural deduction calculus is to be used in the development of real theories, we shall want to enhance it by adding rules, redundant in principle but useful in practice, allowing transformations like those in the list above to be made in one step. We do not consider such an "enhanced" deduction system in these notes, because the focus here is on the conceptual basics rather than on applications, but clearly it is open to anyone to take natural deduction in that direction.