$⊢(\phi ∨ \psi) → (¬\phi → \psi)$

Question

I tried to solve this deduction but I got stuck:

assumed $\phi ∨ \psi$

assumed $¬\phi$

what can I do now?

Answer 1

I don't know if the system you use has an explicit contradiction symbol and related inference rules, but if it does, this might work:

Answer 2

If A or B:

  If not A:

    A or B.   [(1) You need to use this and the only way is disjunction elimination.]

    If A:

      ?   [(3) You may need principle of explosion or proof by contradiction here.]

    If B:

      ?

    B.   [(2) This is your goal so you should aim to deduce this in both of the above cases.]

Answer 3

With natural deduction:

(1) $\phi \lor \psi \qquad$ Hyp.

(2) $\lnot \phi \qquad$ Hyp.

(3) $\phi \lor \psi\qquad $ Rep (1)

(4) $\phi \qquad$ Hyp.

(5) $\lnot \psi \qquad$ Hyp.

(6) $\phi \qquad$ Hep. (4)

(7) $\lnot \phi \qquad$ Rep. (2)

(8) $\phi \land \lnot \phi \qquad \land$ Intro. (6),(7)

(9) $\lnot \lnot \psi \qquad \lnot$ Intro. (5)-(8)

(10) $\psi \qquad \lnot$ Elim. (9)

(11) $\phi \rightarrow \psi \qquad \rightarrow$ Intro. (4)-(10)

(12) $\psi \qquad$ Hyp.

(13) $\psi \qquad$ Rep. (12)

(14) $\psi \rightarrow \psi \qquad \rightarrow$ Intro. (12)-(13)

(15) $\psi \qquad \lor$ Elim. (3),(11),(14)

(16) $\lnot \phi \rightarrow \psi \qquad \rightarrow$ Intro. (2)-(15)

(17) $\left(\phi \lor \psi\right) \rightarrow \left(\lnot \phi \rightarrow \psi \right) \qquad \rightarrow$ Intro. (1)-(16)