Proof by Cases/Proof Rule/Tableau Form
< Proof by Cases | Proof Rule
Jump to navigation
Jump to search
Proof Rule
Let $\phi \lor \psi$ be a well-formed formula in a tableau proof whose main connective is the disjunction operator.
Let $\chi$ be a well-formed formula such that $\paren {\phi \vdash \chi}$, $\paren {\psi \vdash \chi}$.
Proof by Cases 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: | Proof by Cases | ||||||||
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: | $\operatorname {PBC}$ |
Also defined as
Treatments that refer to this as the rule of or-elimination tend to use the abbreviation $\lor \EE$.
Sources
- 1965: E.J. Lemmon: Beginning Logic ... (previous) ... (next): Chapter $1$: The Propositional Calculus $1$: $3$ Conjunction and Disjunction