# Propositional Logic: Validity of sequent $\lnot\Phi_1 \land \lnot \Phi_2 \vdash \Phi_1 \rightarrow \Phi_2$

Propositional Logic: Validity of sequent $\lnot\Phi_1 \land \lnot \Phi_2 \vdash \Phi_1 \rightarrow \Phi_2$

1. $\lnot \Phi_1 \land \lnot \Phi_2$ (premise)
2. $\Phi_1$ (assumption)
3. $\lnot \Phi_1$ ($\land e_1$) 1
4. $\bot$ ($\lnot e$) 2,3
5. $\Phi_2$ ($\bot e$) 4

6. $\Phi_1 \rightarrow \Phi_2$ ($\rightarrow i$) 2,5

All this look really weird to me. I work with $\Phi_1$ and $\lnot \Phi_1$ at the same time.

Can someone tell me how to proceed and why this is valid? Taken from the book "Logic in Computer Science" by Michael Huth and Mark Ryan.

• The question is a strange one - are you sure you've stated it correctly? The deduction theorem lets you rephrase as $\{\neg \phi_1 \wedge \neg \phi_2 , \phi_1 \} \vdash \phi_2$, which is true by explosion. – Patrick Stevens Sep 18 '15 at 8:29
• I'm sure. Check the image I've uploaded on the book I'm working on. I'm trying to get into logic programming by reading this book. – Shuzheng Sep 18 '15 at 8:33

If we already know $\neg \Phi_1$ holds then the implication $\Phi_1\rightarrow \Phi_2$ is just saying that "If $\Phi_1$ is also true (i.e. both true and false) then we may conclude anything, such as $\Phi_2$". The whole statement is all about the principle of explosion ($\bot \vdash P$ for any $P$) and contradiction.
You can finnish the proof by using that we have a contradiction, deduce whatever you want hence conclude $\Phi_2$ and complete the proof by using $\rightarrow$ introduction.
• Thanks @OveAhlman. Would you mind looking at my updated solution? Why do the premise include $\lnot \Phi_2$ - I don't use it for anything. Have I made a mistake? – Shuzheng Sep 18 '15 at 8:40
• @NicolasLykkeIversen The updated solution is correct. As you point out, $\neg \Phi_2$ is not used for anything, and I think it is included in the exercise just to make the exercise more perplexing and look even more contradictory. – Ove Ahlman Sep 18 '15 at 9:35