How to proof ¬P∨Q entails P→Q by Natural deduction

Question

I can easily proof that $P \to Q$ entails $\lnot P \lor Q$ by Natural deduction,

but I cannot find a way to proof $\lnot P \lor Q$ entails $P \to Q$.

Could you show me the way by using Natural Deduction?

Answer 1

The details -- surprise, surprise! -- will depend on the natural deduction system.

In most Fitch-style systems as taught to students, though, the proof will overall look like this:

$(\neg P \lor Q)\\ \quad\quad | \quad P\\ \quad\quad | \quad \vdots\\ \quad\quad | \quad Q\\ (P \to Q)$

You assume $P$ as a temporary assumption, deduce $Q$ and then use Conditional Proof to discharge the assumption and derive the conditional conclusion.

So the issue becomes how to get from $P$ to $Q$. This is trivial in an ND system with Disjunctive Syllogism as a primitive rule. But I guess since you are asking this question, you are just having to use the standard Disjunction Elimination rule. So you want a proof that now looks like this:

$(\neg P \lor Q)\\ \quad\quad | \quad P\\ \quad\quad | \quad\quad | \quad\neg P\\ \quad\quad | \quad\quad | \quad\vdots\\ \quad\quad | \quad\quad | \quad Q\\ \quad\quad | \quad\quad / \\ \quad\quad | \quad\quad | \quad Q\\ \quad\quad | \quad\quad | \quad \vdots\\ \quad\quad | \quad\quad | \quad Q\\ \quad\quad | \quad Q\\ (P \to Q)$

You argue from each disjunct of the original premiss to $Q$ and conclude therefore that, either way, $Q$.

The second new subproof is trivial! The first is the problem case. IN a standard natural deduction system, however, we have some version of "Explosion" either as a primitive rule or otherwise available. This is the inference that will take us for contradictory wffs like $P$ and $\neg P$ to any wff at all, and hence to $Q$. That's what you need to plug in to complete the proof in standard systems.

---

It is worth noting that this shows there is something odd about the standard Disjunction Elimination rule in the usual textbooks. For isn’t the appeal to explosion here decidedly unnatural? Return to informal argumentation for a moment. Suppose you have established that a disjunction A or B holds. Then suppose you discover that the first disjunct is inconsistent with something else you accept, X. In this case, you simply rule out the first option A, and immediately conclude that B, without further fuss. You don’t think that you have to pause to show that A plus X together entail B.

So a more natural disjunction elimination rule goes: given $A \lor B$, and two subproofs, one from $A$ to $C$ or absurdity, the other from $B$ to $C$ or absurdity, then infer $C$ unless both proofs end in absurdity in which case infer absurdity.

With this revised rule, something like the following simplified and surely more natural line of proof becomes available

$(\neg P \lor Q)\\ \quad\quad | \quad P\\ \quad\quad | \quad\quad | \quad \neg P\\ \quad\quad | \quad\quad | \quad \bot\\ \quad\quad | \quad\quad / \\ \quad\quad | \quad\quad | \quad Q\\ \quad\quad | \quad Q\\ (P \to Q)$