Proof by Cases/Proof Rule/Tableau Form

From ProofWiki
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