Show $\vdash (\phi \to \psi) \land (\lnot \phi \to \psi) \to \psi$.

Question

Note: $\lnot \phi$ is an abbreviation of $\phi \to \bot$. Using Dirk van Dalen. "Logic and Structure (Universitext)" as reference book.

Derivation:

$ \def\be{\mathsf{\tiny{\leftrightarrow} Elim}} \def\bi{\mathsf{\tiny{\leftrightarrow} Intro}} \def\ce{\mathsf{\tiny{\land} Elim}} \def\ne#1{\mathsf{\tiny\neg Elim^{#1 }}} \def\ni#1{\mathsf{\tiny\neg Intro^{#1}}} \def\ii#1{\mathsf{\tiny{\to}Intro^{#1}}} \def\ie{\mathsf{\tiny{\to}Elim}} \def\RAA#1{\mathsf{\tiny RAA^{#1}}} $

$ \dfrac{ \dfrac{ \dfrac{ \dfrac{ \dfrac{ \dfrac{}{[\lnot \psi]_3}\dfrac{ \dfrac{}{[\phi]_2}\dfrac{ [(\phi \to \psi) \land (\lnot \phi \to \psi)]_1 }{\phi \to \psi}\ce }{\psi}\ie }{\bot}\ie }{\lnot \phi}\ni 2 \dfrac{ [(\phi \to \psi) \land (\lnot \phi \to \psi)]_1 }{\lnot \phi \to \psi}\ce }{\psi}\RAA 3 \dfrac{}{[\lnot \psi]_4} }{\psi}\ne 4 }{(\phi \to \psi) \land (\lnot \phi \to \psi) \to \psi}\ii 1 $

My questions are:

• Is the hypotesis of $\lnot \psi$ labeled with a sub-index "4" correctly discharged ?
• Is this proof correct ?

EDIT:

Revised derivation:

$ \dfrac{ \dfrac{ \dfrac{ \dfrac{ \dfrac{ \dfrac{ \dfrac{}{[\lnot \psi]_3}\dfrac{ \dfrac{}{[\phi]_2}\dfrac{ [(\phi \to \psi) \land (\lnot \phi \to \psi)]_1 }{\phi \to \psi}\ce }{\psi}\ie }{\bot}\ie }{\lnot \phi}\ii 2 \dfrac{ [(\phi \to \psi) \land (\lnot \phi \to \psi)]_1 }{\lnot \phi \to \psi}\ce }{\psi}\ie \dfrac{}{[\lnot \psi]_3} }{\bot}\ie }{\psi}\RAA 3 }{(\phi \to \psi) \land (\lnot \phi \to \psi) \to \psi}\ii 1 $

Answer 1

Your derivation up until $\neg \phi, \neg \phi \to \psi$ as well as the very last step are correct. Your idea that we need to get rid of the assumption $\neg \psi$ and for that purpose provoke a contradiction in order to then apply $RAA$ thereby discharging the assumption is also correct, but you got the rules a bit mixed up there.
The next step which combines $\neg \phi$ and $\neg \phi \to \psi$ to yield $\psi$ is not RAA, but $\to Elim$. This rule does not allow to discharge assumptions and we still need to get rid of the assumption $\neg \psi$. So even though we already established the desired conclusion $\psi$, we need to make a detour with further steps in order to kill the remaining assumption along the way.
Performing a $\neg Elim$ with assumption $\neg \psi$ first leads to $\bot$. From that you can then conclude $\psi$ by an application of $RAA$, thereby discharging both occurrences of the assumption $\neg \psi$ (the one that was still open from earlier and the one we just opened).
This allows you to then complete the proof with $\to Intro$.

[-psi]3
  ...            ...
 -phi        -phi -> psi
------------------------- (-> E)
           psi                     [-psi]3
          ------------------------------ (- E)
                        ⊥
                       --- (RAA)3
                       psi            
     ------------------------------------- (-> I)1
      (phi -> psi) ^ (-phi -> psi) -> psi

These are two common patterns in ND proofs that are "difficult":

• We already established some desired formula but still got open assumptions to deal with, so we apply a couple extra steps ending up with the same formula but killing some assumptions along the way.
• We open the same assumption at different points in the proof, and eventually discharge all occurrences in the same step.

Answer 2

Using quite another proof system -- apologies -- but this may help...