# I don't trust my proof of $\neg ( \phi \rightarrow \neg \psi) \vdash \phi$

I have just given an axiomatic proof of conjunction elimination, but I don't trust it. I wonder if anyone will take a look. Note that $$\phi$$ $$\wedge$$ $$\psi$$ is viewed here as an abbreviation of $$\neg (\phi \rightarrow \neg \psi)$$. I am allowed the following axioms plus any derived rules, and I have derived $$\neg \neg$$E, $$\rightarrow$$I and $$\phi$$,$$\neg \phi$$ $$\vdash \psi$$ (EFQ) myself:

$$(A1) \hspace{0.1cm}\phi \rightarrow (\psi \rightarrow \phi)\$$

$$(A2)\hspace{0.1cm} \phi \rightarrow (\psi \rightarrow \chi) \rightarrow ((\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \chi))\$$

$$(A3)\hspace{0.1cm}(\neg \phi \rightarrow \neg \psi) \rightarrow (\psi \rightarrow \phi)$$

1. $$\neg (\phi \rightarrow \neg \psi)\hspace{2cm}$$ Premise
2. $$\neg \phi \hspace{3.5cm}$$ assumption
3. $$\phi \hspace{3.75cm}$$ assumption
4. $$\neg \psi \hspace{3.4cm}$$ Ex falso Quodlibet
5. $$\phi \rightarrow \neg \psi \hspace{2.35cm}$$ Conditional Intro
6. $$\neg \neg \phi \hspace{3.1cm}$$ Negation Intro
7. $$\phi \hspace{3.6cm}$$ Double-negation Elim

So I suppose $$\neg \phi$$ and $$\phi$$, derive $$\neg \psi$$ by EFQ, and then discharge $$\phi$$ to get $$\phi \rightarrow \neg \psi$$, which contradicts my premise, so I discharge $$\neg \phi$$ and get $$\neg \neg \phi$$. The rest is straightforward.

• It works........ Nov 8, 2022 at 7:26
• sounds fair enough to me as well.. Nov 8, 2022 at 20:31
• I suppose my main worries were to do with the conditional intro. In particular, whether I should be allowed to say $\phi \rightarrow \neg \psi$ or whether, because it was introduced afterwards, it really should be $\neg \phi \rightarrow \neg \psi$, but my feeling is that I should be allowed to do $\rightarrow$ intro with any of them, since at that stage in the proof we are supposing both to be true. Nov 9, 2022 at 11:19