← Theorems

↑ Sentential Logic

Disjunctions in Derivations →

Derived Inference Rules

This page introduces the notion of a derived inference rule and provides a few such rules.

Deriving inference rules

The basics

Now we can carry the abbreviation a step further. A derived inference rule is an inference rule not given to us as part of the derivation system but which constitutes an abbreviation using a previously proved theorem. In particular, suppose we have proved a particular theorem. In this theorem, uniformly replace each sentence letter with a distinct Greek letter. Suppose the result has the following form. [Comment: This and what follows seems to me to be potentially confusing to students. The intention stated in earlier sections to avoid metatheory makes for a problem here as one really should know about the Deduction Theorem for this to make more sense.]

We may then introduce a derived inference rule having the form

An application of the derived rule can be eliminated by replacing it with (i) the previously proved theorem, (ii) enough applications of Conjunction Introduction (KI) to build up the theorem's antecedent, and (iii) an application of Conditional Elimination (CE) to obtain the theorem's consequent. The previously proved theorem can then be eliminated as described above. That would leave you with an unabbreviated derivation.

Please remember, removing the abbreviations from a derivation is not desirable. It will make the derivation more complicated and harder to read. Rather, the fact that a derivation could be unabbreviated if so desired (even though we don't really desire it) is what justifies the abbreviation, what permits us to employ the abbreviation in the first place.

Repetition

Our first derived inference rule will be based on T1, which is

Replace the sentence letters with Greek letters, and we get:

We now generate the derived inference rule:

Repetition (R)

Now we can show how this rule could have simplified our proof of T2.

1.       Assumption        2.         Assumption    3.         1 R     4.       2–3 CI   5.     1–4 CI

While this is only one line shorter than our original proof of T2, it is less obnoxious. We can use an inference rule instead of a silly trick. As a result, the derivation is easier to read and understand (not to mention easier to produce).

Double negation rules

The next two theorems—and the derived rules based on them—exploit the equivalence between a doubly negated formula and the unnegated formula.

Double Negation Introduction

1.       Assumption        2.         Assumption    3.         1 R     4.       2–3 NI   5.     1–4 CI

T3 justifies the following rule.

Double Negation Introduction (DNI)

Double Negation Elimination

1.       Assumption        2.         Assumption    3.         1 R     4.       2–3 NE   5.     1–4 CI

T4 justifies the following rule.

Double Negation Elimination (DNE)

Additional derived rules

Contradiction

1.       Assumption        2.         Assumption    3.         1 S 4.         1 S     5.       2–4 NE   7.     1–5 CI

Our next rule is based on T5.

Contradiction (Contradiction)

This rule is occasionally useful when you have derived a contradiction but the discharge rule you want is not NI or NE. This then avoids a completely trivial subderivation. The rule of Contradiction will be used in the proof of the next theorem.

Conditional Addition

1.       Assumption        2.         Assumption    3.         1, 2 Contradiction     4.       2–3 CI   5.     1–4 CI

On the basis of T2 and T6, we introduce the following derived rule.

Conditional Addition, Form I (CAdd)

Conditional Addition, Form II (CAdd)

The name 'Conditional Addition' is not in common use. It is based on the traditional name for Disjunction Introduction, namely 'Addition'. This rule does not provide a general means of introducing a conditional. This is because the antecedent line you would need is not always derivable. However, when the antecedent line just happens to be easily available, then applying this rule is simpler than producing the subderivation needed for a Conditional Introduction.

Modus Tollens

1.       Assumption        2.         Assumption    3.         1 KE 4.         2, 3 CE 5.         1 KE     6.       2–5 NI   7.     1–6 CI

Now we use T7 to justify the following rule.

Modus Tollens (MT)

Modus Tollens is also sometimes known as 'Denying the Consequent'. Note that the following is not an instance of Modus Tollens, at least as defined above.

The premise lines of Modus Tollens are a conditional and the negation of its consequent. The premise lines of this inference are a conditional and the opposite of its consequent, but not the negation of its consequent. The desired inference here needs to be derived as below.

1.     Premise 2.     Premise 3.     2 DNI 4.     1, 3 CE 5.     4 DNE

Of course, it is possible to prove as a theorem:

Then you can add a new inference rule—or, more likeley, a new form of Modus Tollens—on the basis of this theorem. However, we won't do that here.

Additional theorems

The derived rules given so far are quite useful for eliminating frequently used bits of obnoxiousness in our derivations. They will help to make your derivations easier to generate and also more readable. However, because they are indeed derived rules, they are not strictly required but rather are theoretically dispensable.

A number of other theorems and derived rules could usefully be added. We list here some useful theorems but leave their proofs and the definition of their associated derived inference rules to the reader. If you construct many derivations, you may want to maintain your own personal list that you find useful.

Theorems with biconditionals

Theorems with negations