Formal Logic/Sentential Logic/Inference Rules

From Wikibooks, open books for an open world
< Formal Logic‎ | Sentential Logic
Jump to: navigation, search
← Derivations ↑ Sentential Logic Constructing a Simple Derivation →



Inference Rules[edit]

Overview[edit]

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 can be abbreviated as 'CE'. We can apply this rule if formulae having the forms above the line appear as active lines 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 will be 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. Most textbooks avoid giving any special terminology here; they just leave it up to the classroom teaching assistant to make it up as they go.

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[edit]

Negation[edit]

Negation Introduction (NI)

Deferred to a later page.


Negation Elimination (NE)

Deferred to a later page.

Conjunction[edit]

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[edit]

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[edit]

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[edit]

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[edit]

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 add to a derivation

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

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

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).