4.7 Disjunction elimination

This is the most complicated rule, mainly because if we are given a phrase with or, like ``it's Thursday or Friday'', what can we deduce from it? That it's Thursday? No, it may be Friday. That it's Friday? No, it may be Thursday. That it's Thursday or Friday? Well, yes, but we already knew that...

The rule (now I explain it):

m & A \vee B \\
& \fh A & H \\
... C \\
& C & E$\vee$\ m,n,p
\end{fitch*} \end{displaymath}

We need more information besides the $A\vee B$. If, luckily, we happen to know $A\Rightarrow C$, and also $B\Rightarrow C$, then we do know what happens when $A\vee B$: both one option and the other drive us to $C$, so $C$ is true.

This type of things only happen when the exercise is prepared so that the disjunction elimination appears, or when $A$ and $B$ are similar (then we will find some $C$ which is implied by both).

Now an example: when I contracted my ADSL access to the Internet, it was with Telefónica or Terra, but I'm not sure of with which one (even they didn't know it). And in my country (Spain), any option was slow, awfully expensive, and loaded with problems. Typical Spanish. If we call all those features $M$ (for mockery, misery, ...), then basically any Internet Service Provider was an $M$. Concretely, $Telefonica\Rightarrow M$ and $Terra\Rightarrow M$, so undoubtedly my ADSL had to be $M$, both if I had one or the other ISP. And indeed, I needed 9 months to fully subscribe to the service... Luckily all this happened now several years ago.

This derivation rule is also called proof by cases, since we have to check each possible case to see that they all involve the same conclusion.

Daniel Clemente Laboreo 2005-05-17