I want to show, using deduction thorem that $\vdash((b\rightarrow (\neg c\rightarrow(b\rightarrow c))$

I know, thanks to the Deduction theorem that

$\phi_1,\phi_2,...\phi_{n-1}\vdash\phi_n\rightarrow\psi \Leftrightarrow \phi_1,\phi_2,...\phi_{n-1},\phi_n\vdash\psi$


$b\vdash\neg c\rightarrow\neg(b\rightarrow c)$ (DT)

$b, \neg c\vdash\neg(b\rightarrow c)$ (DT)

But what to do from here? Any hint appreciate.

  • 2
    $\begingroup$ If $b$ is true and $c$ is false the statement $(b\to(\neg c\to(b\to c)))$ becomes false, so you won't be able to show that it is a tautology. $\endgroup$ – Christoph Oct 21 '15 at 10:51
  • 1
    $\begingroup$ However, $(b\to (\neg c\to \color{red}{\neg}(b\to c)))$ is a tautology. So typographical error? $\endgroup$ – Graham Kemp Oct 21 '15 at 11:23
  • $\begingroup$ You need a rule like : if $\varphi, \psi \vdash \sigma$ and $\varphi, \psi \vdash \lnot \sigma$, then $\varphi \vdash \lnot \psi$. It is easy with Natural Deduction; in Hilbert-style, it can be derived from axioms. $\endgroup$ – Mauro ALLEGRANZA Oct 21 '15 at 11:34
  • $\begingroup$ If the typo works along the lines that Graham Kemp suggested, and your axiom set is the Frege inspired {CxCyx, CCxCyzCCxyCxz, CNNxx, CxNNx, CCxyCNyNx}, prove prefixing: CCxyCCzxCzy, and modus ponens: CxCCxyy. Using CCxyCCzxCzy, CxCCxyy, and CCxyCNyNx, you can then derive CxCNyNCxy, since CCCxyyCNyNCxy is an instance of CCxyCNyNx. $\endgroup$ – Doug Spoonwood Oct 21 '15 at 12:53

Your Answer

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

Browse other questions tagged or ask your own question.