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?

enter image description here

Taken from the book "Logic in Computer Science" by Michael Huth and Mark Ryan.

  • $\begingroup$ 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. $\endgroup$ – Patrick Stevens Sep 18 '15 at 8:29
  • $\begingroup$ 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. $\endgroup$ – Shuzheng Sep 18 '15 at 8:33

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.

  • $\begingroup$ 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? $\endgroup$ – Shuzheng Sep 18 '15 at 8:40
  • $\begingroup$ @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. $\endgroup$ – Ove Ahlman Sep 18 '15 at 9:35
  • $\begingroup$ Thank you for your assistance @OveAhlman. $\endgroup$ – Shuzheng Sep 18 '15 at 9:45

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.