Rule of Or-Elimination
Contents
Proof Rule
The rule of or-elimination is a valid deduction sequent in propositional logic:
If we can conclude $p \lor q$, and:
- $(1): \quad$ By making the assumption $p$, we can conclude $r$
- $(2): \quad$ By making the assumption $q$, we can conclude $r$
then we may infer $r$.
The conclusion $r$ does not depend upon either assumption $p$ or $q$.
It can be written:
- $\displaystyle {p \lor q \quad \begin{array}{|c|} \hline p \\ \vdots \\ r \\ \hline \end{array} \quad \begin{array}{|c|} \hline q \\ \vdots \\ r \\ \hline \end{array} \over r} \lor_e$
Sequent Form
The Rule of Or-Elimination can be symbolised by the sequent:
- $p \lor q, \left({p \vdash r}\right), \left({q \vdash r}\right) \vdash r$
Tableau Form
Let $\phi \lor \psi$ be a propositional formula in a tableau proof whose main connective is the disjunction operator.
Let $\chi$ be a propositional formula such that $\left({\phi \vdash \chi}\right)$, $\left({\psi \vdash \chi}\right)$.
The Rule of Or-Elimination is invoked for $\phi \lor \psi$ as follows:
Pool: | The pooled assumptions of $\phi \lor \psi$ | ||||||
The pooled assumptions of the instance of $\chi$ which was derived from the individual assumption $\phi$ | |||||||
The pooled assumptions of the instance of $\chi$ which was derived from the individual assumption $\psi$ | |||||||
Formula: | $\chi$ | ||||||
Description: | Rule of Or-Elimination | ||||||
Depends on: | The line containing the instance of $\phi \lor \psi$ | ||||||
The series of lines from where the assumption $\phi$ was made to where $\chi$ was deduced | |||||||
The series of lines from where the assumption $\psi$ was made to where $\chi$ was deduced | |||||||
Discharged Assumptions: | The assumptions $\phi$ and $\psi$ are discharged | ||||||
Abbreviation: | $\lor \mathcal E$ |
Explanation
We know $p \lor q$, that is, either $p$ is true or $q$ is true, or both.
Suppose we assume that $p$ is true, and from that assumption we have managed to deduce that $r$ has to be true.
Then suppose we assume that $q$ is true, and from that assumption we have also managed to deduce that $r$ has to be true.
Therefore, it has to follow that the truth of $r$ follows from the fact of the truth of $p \lor q$.
Thus we can eliminate a disjunction from a sequent.
Also known as
This is also known as proof by cases, but this is also used for an extension of this concept.
Also see
Technical Note
When invoking the Rule of Or-Elimination in a tableau proof, use the OrElimination template:
{{OrElimination|line|pool|statement|base|start1|end1|start2|end2}}
where:
-
line
is the number of the line on the tableau proof where the Rule of Or-Elimination is to be invoked -
pool
is the pool of assumptions (comma-separated list) -
statement
is the statement of logic that is to be displayed in the Formula column, without the$ ... $
delimiters -
base
is the line of the tableau proof where the disjunction being eliminated is situated -
start1
is the start line of the block of the tableau proof upon which the demonstration of the first disjunct directly depends -
end1
is the end line of the block of the tableau proof upon which the demonstration of the first disjunct directly depends -
start2
is the start line of the block of the tableau proof upon which the demonstration of the second disjunct directly depends -
end2
is the end line of the block of the tableau proof upon which the demonstration of the second disjunct directly depends
Sources
- Donald Kalish and Richard Montague: Logic: Techniques of Formal Reasoning (1964)... (previous)... (next): $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 5$
- E.J. Lemmon: Beginning Logic (1965)... (previous)... (next): $\S 1.3$: Conjunction and Disjunction
- Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems (2000)... (previous)... (next): $\S 1.2.1$: Rules for natural deduction