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

Question

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.

Answer 1

This is correct.

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.