I'm trying to prove that $\{(p_1\implies p_2),p_1,(p_2\implies p_3)\}\vdash (p_3\vee p_5)$ which seems easy, but I'm unsure about a step in the way.

I did:

$1.\ p_1\implies p_2 \text{ (Pre)}\\2.\ p_1 \text{(Pre)}\\3. \ p_2\implies p_3 \text{(Pre)}\\ 4.\ p_2 \text{ (By 2. and 1.)}\\ 5.\ p_3 \text{(By 4. and 3.)} \\ 6.\ \neg(p_3\vee p_5) \text{ (Assume)}\\ 6.1.\ (\neg p_3\wedge \neg p_5) \text{(By Morgan)}\\6.2. \ \neg p_3\text{ (By 6.2)}\\7. \ (p_3\vee p_5) \text{ (By contradiction of 6.)}$

Is this right?. I'm unsure about the step 6 where $p_5$ comes from nowhere, should I assume $p_5$ first?


There doesn't seem to be anything strictly wrong with your strategy -- assumptions don't have to come from anywhere as long as they get properly discharged.

But it seems to be a detour. Most natural deduction systems have a rule that allows you to infer directly from $P$ to $P\lor Q$. Doesn't yours?

On the other hand, most natural deduction systems don't include De Morgan's rules as primitive inferences. Are you sure your step from 6 to 6.1 is formally allowed?

  • $\begingroup$ On the other hand this does show that if one considers a system with the rules used in the proof analysis of the OP's proof, that left-disjunction introduction becomes a derivable rule of inference. One might argue that it should be a derivable rule of inference, since from just conditional introduction and conditional elimination we have p $\vdash$ CCpqq, and since the truth table for CCpqq and Apq match, we can think of this as implying that left-disjunction introduction is a valid rule of inference. $\endgroup$ – Doug Spoonwood Jul 22 '14 at 4:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.