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

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$$

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.
• Thank you, @lemontree ! I will fix the typo and read your answer carefully. Commented Oct 27, 2020 at 14:40
• When I finish the proof: do I edit it, or paste it below again with the changes ? Commented Oct 27, 2020 at 14:45
• Best copy-paste it so future readers can still make sense of the correction suggestions. Commented Oct 27, 2020 at 14:50
• When you said: "After that, performing a $\lnot Elim$ with assumption $\lnot \phi$ would first lead to $\bot$", did you mean $\lnot \psi$ ? Commented Oct 27, 2020 at 16:44
• Well yes -- normally, mathematical trees grow upside-down, with the root (greatgreat...grandmother) of at the top, but an ND tree grows like a natural tree, so here "ancestor" means futher down in the tree. Commented Oct 27, 2020 at 21:51

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