Formal Logic/Sentential Logic/Inference Rules

← Derivations

↑ Sentential Logic

Constructing a Simple Derivation →

Inference Rules

Overview

Inference rules will be formated as in the following example.

Conditional Elimination (CE)

$(\varphi \rightarrow \psi )\,\!$

${\underline {\varphi \quad \quad \quad }}\,\!$

$\psi \,\!$

The name of this inference rule is 'Conditional Elimination', which is abbreviated as 'CE'. We can apply this rule if formulae having the forms above the line appear as active lines of text in the derivation. These are called the antecedent lines for this inference. Applying the rule adds a formula having the form below the line. This is called the consequent line for this inference. The annotation for the newly derived line of text is the line numbers of the antecedent lines and the abbreviation 'CE'.

Note. You might see premise line and conclusion line for antecedent line and consequent line. You may see other terminology as well, as most textbooks avoid giving any special terminology here.

Each sentential connective will have two inference rules, one each of the following types.

• An introduction rule. The introduction rule for a given connective allows us to derive a formula having the given connective as its main connective.

• An elimination rule. The elimination rule for a given connective allows us to use a formula already appearing in the derivation having the given connective as its main connective.

Three rules (Negation Introduction, Negation Elimination, and Conditional Introduction) will be deferred to a later page. These are so-called discharge rules which will be explained when we get to subderivations.

Three rules (Conjunction Elimination, Disjunction Introduction, and Biconditional Elimination) will have two forms each. We somewhat arbitrarily count the two patterns as forms of the same rule rather than separate rules.

The validity of the inferences on this page can be shown by truth table.

Inference rules

Negation

Negation Introduction (NI)

Deferred to a later page.

Negation Elimination (NE)

Deferred to a later page.

Conjunction

Conjunction Introduction (KI)

$\varphi \,\!$

${\underline {\psi \quad \quad \ \ }}\,\!$

$(\varphi \land \psi )\,\!$

Conjunction Introduction traditionally goes by the name Adjunction or Conjunction.

Conjunction Elimination, Form I (KE)

${\underline {(\varphi \land \psi )}}\,\!$

$\varphi \,\!$

Conjunction Elimination, Form II (KE)

${\underline {(\varphi \land \psi )}}\,\!$

$\psi \,\!$

Conjunction Elimination traditionally goes by the name Simplification.

Disjunction

Disjunction Introduction, Form I (DI)

${\underline {\varphi \quad \quad \ \ }}\,\!$

$(\varphi \lor \psi )\,\!$

Disjunction Introduction, Form II (DI)

${\underline {\psi \quad \quad \ \ }}\,\!$

$(\varphi \lor \psi )\,\!$

Disjunction Introduction traditionally goes by the name Addition.

Disjunction Elimination (DE)

$\varphi \lor \psi \,\!$

$(\varphi \rightarrow \chi )\,\!$

${\underline {(\psi \rightarrow \chi )}}\,\!$

$\chi \,\!$

Disjunction Elimination traditionally goes by the name Separation of Cases.

Conditional

Conditional Introduction (CI)

Deferred to a later page.

Conditional Elimination (CE)

$(\varphi \rightarrow \psi )\,\!$

${\underline {\varphi \quad \quad \quad }}\,\!$

$\psi \,\!$

Conditional Elimination traditionally goes by the Latin name Modus Ponens or, less often, by Affirming the Antecedent.

Biconditional

Biconditional Introduction (BI)

$(\varphi \rightarrow \psi )\,\!$

${\underline {(\psi \rightarrow \varphi )}}\,\!$

$(\varphi \leftrightarrow \psi )\,\!$

Biconditional Elimination, Form I (BE)

$(\varphi \leftrightarrow \psi )\,\!$

${\underline {\varphi \quad \quad \quad }}\,\!$

$\psi \,\!$

Biconditional Elimination, Form II (BE)

$(\varphi \leftrightarrow \psi )\,\!$

${\underline {\psi \quad \quad \quad }}\,\!$

$\varphi \,\!$

Examples

Inference rules are easy enough to apply. From the lines

(1)    $\mathrm {P} \land \mathrm {Q} \rightarrow (\mathrm {S} \leftrightarrow \mathrm {T} )\,\!$

and

(2)    $\mathrm {P} \land \mathrm {Q} \,\!$

we can apply Conditional Elimination to add

(3)    $\mathrm {S} \leftrightarrow \mathrm {T} \,\!$

to a derivation.

The annotation will be the line numbers of (1) and (2) and the abbreviation for Conditional Elimination, namely '1, 2, CE'. The order of the antecedent lines does not matter; the inference is allowed regardless of whether (1) appears before or after (2).

It must be remembered that inference rules are strictly syntactical. Semantically obvious variations is not allowed. It is not allowed, for example, to derive (3) from (1) and

(4)    $\mathrm {Q} \land \mathrm {P} \,\!$

However, you can get from (1) and (4) to (3) by first deriving

(5)    $\mathrm {Q} \,\!$

and

(6)    $\mathrm {P} \,\!$

by Conjunction Elimination (KE). Then you can derive (2) by Conjunction Introduction (KI) and finally (3) from (1) and (2) by Conditional Elimination (CE) as before. Some derivation systems have a rule, often called Tautological Implication, allowing you to derive any tautological consequence of previous lines. However, this should be seen as an (admittedly useful) abbreviation. On later pages, we will implement a restricted version of this abbreviation.

It is generally useful to apply break down premises, other assumptions (to be introduced on a later page) by applying elimination rules—and then continue breaking down the results. Supposing that is why we applied CE to (1) and (2), it will likely be useful to derive

(7)    $\mathrm {S} \rightarrow \mathrm {T} \,\!$

and

(8)    $\mathrm {T} \rightarrow \mathrm {S} \,\!$

by applying Biconditional Elimination (BE) to (3). To further break this down, you might then attempt to derive $\mathrm {S} \,\!$ or $\mathrm {T} \,\!$ so that you can apply CE to (7) or (8).

If you know what line you want to derive, you can build it up by applying introduction rules. That was the strategy for deriving (2) from (5) and (6).