Natural Deduction Rules

Question

I am familiar with the main rules of natural deduction:

$∧i, ∧e1, ¬¬e, ⇒e, ⇒i, ∨i, ∨e$ (slightly).

However, when presented with the following premise:

$$\sim a ∧ (a ∨ b)$$

I used $∧ e$ to obtain:

$$\sim a , (a ∨ b)$$

Now I am stuck on what exact 'rule' to apply here. I have clearly derived $\sim a$ to be true, and thus a must be false. This means that from the truth expression $(a ∨ b)$ we can deduce $b$. However I don't know what rule says we can just eliminate $∨$ this way, since the only $∨$ elimination rule I am aware of includes proving both assuming both $a$ and $b$ and proving a result.

Answer 1

The key to this is indeed the $\lor \ E$ rule, which is the most difficult rule to master for most beginning students of formal logic.

Yes, this rule has you assume each of the disjuncts of some disjunction that you have, and derive the same result in each case, so that you can therefore conclude that that result follows from the very disjunction.

Applied to your situation: you have the disjunction $a \lor b$, and so you do two subproofs: one in which you assume that $a$ is true, and one in which you assume that $b$ is true.

Ok, but what should be the 'same result' that yu should be looking for in each of these subproofs? Well, given that you are ultimately looking for $b$, it makes sense to see if you can indeed derive that in each of the cases $a$ and $b$.

Now, let's first focus on the second subproof, i.e the one where you assume that $b$ is true. So here you are looking to derive $b$ .... but that is trivial: if $b$ is assumed to be true, then of course you can derive $b$. Ok, so we can indeed derive $b$ in this second subproof.

OK, but what about the first subproof, i.e. the one where you assume $a$? Can you derive $b$ in that case as well? Well, sure! Note that aside from the assumption $a$, you also have $\neg a$, since you had derived that earlier. So, you have both $a$ and $\neg a$. But that is a contradiction, and from a contradiction you can infer anything you want (tis is sometimes called the Principle of Explosion) ... including $b$. OK, so yes, we should be able to infer $b$ in the first subproof as well.

Finally, then, we use the $\lor \ E$ rule: we have a disjunction $a \lor b$, so we know that at least one of $a$ and $b$ is true, but we don't know which one. However, we have also shown that whichever one of these is true, we can always derive $b$. OK, but that means that $b$ is definitely true ... and that is what the $\lor \ E$ can now conclude.

Now, the specific way some of these rules ar formally implemented differs from formal proof system to formal proof system, so I can't tell you exactly what this formalproof is going to look like, but it will be along these conceptual lines.

Answer 2

$$\lnot a, a\lor b\vdash b$$

This is actually the disjuctive syllogism, although sometimes called disjunctive elimination to confuse students.   They are closely related concepts, but not quite the same.

The rule of inference used to prove it is disjunction elimination ($\lor e$).   This is the "Proof by Cases" inference.   One of the subproofs is trivial, as the assumption is the desired conclusion.   The other case involves deriving a contradiction ($\lnot a$ and $a$), then using the principle of explosion (ex falso quodlibet); sometimes called contradiction elimination.

$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline #2\end{array}} {\fitch{~1.~\lnot a \land (a \lor b)\hspace{10ex}\textsf{Premise}}{~2.~\lnot a\hspace{19ex}\textsf{Conjunction Elimination }(\land\mathsf e,1)\\~3.~a\lor b\hspace{17ex}\textsf{Conjunction Elimination }(\land\mathsf e,1)\\\fitch{~4.~a\hspace{18ex}\textsf{Assumption}}{~5.~\bot\hspace{17ex}\textsf{Negation Elimination }(\lnot\textsf e,2,4)\\~6.~b\hspace{18ex}\textsf{Explosion (ex falso quodlibet) }(\bot\mathsf e,5)}\\\fitch{~7.~b\hspace{18ex}\textsf{Assumption}}{}\\~8.~b\hspace{21ex}\textsf{Disjunction Elimination }(\vee\mathsf e,3,4{-}6,7{-}7)}\\\blacksquare}$$