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

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?

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)$

• Thank you for your detail explanation, and I find another way solving this problem by using OR elimination in my book just now. Thanks again – TonyWang Jan 2 '18 at 10:47
• @PeterSmith I really like that revised rule, and have often thought that this would be an improvement myself ... it certainly would make it similar to what happens in truth trees, and in fact I have been working on some software that implements the rule exactly this way. Do you know of any existing systems that define the rule this way? – Bram28 Jan 2 '18 at 14:44
• @Bram28 The revised rule has for a long time been advocated by Neil Tennant, and it is incorporated in the system he now calls Core Logic (most carefully set out in his book of that title). – Peter Smith Jan 2 '18 at 14:57
• @PeterSmith Good to know, thanks! – Bram28 Jan 2 '18 at 15:03