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.

  • $\begingroup$ It works........ $\endgroup$ Nov 8, 2022 at 7:26
  • $\begingroup$ sounds fair enough to me as well.. $\endgroup$
    – Ettore
    Nov 8, 2022 at 20:31
  • $\begingroup$ 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. $\endgroup$
    – Dan Öz
    Nov 9, 2022 at 11:19


You must log in to answer this question.

Browse other questions tagged .