I have constructed the following proof of $\phi \vdash \neg \neg \phi$ using an axiomatic proof system as well as $(\neg$I) and ex falso quodlibet ($\phi,\neg \phi \vdash \psi$) and ($\rightarrow$I), which I've already proved. I get suspicious whenever I use EFQ, so I'm doubting my proof, but perhaps it's fine:

  1. $\phi \hspace{5cm} premise$
  2. $\neg \phi \hspace{4.6cm} assumption$
  3. $\neg \phi \hspace{4.6cm} EFQ, 1,2$
  4. $\phi \rightarrow \neg \phi \hspace{3.55cm} \rightarrow I\hspace{0.3cm}1,3$
  5. $\neg \phi \hspace{4.55cm} MP \hspace{0.4cm} 1,4 $
  6. $\neg \neg \phi \hspace{4.2cm} \neg$I

So I suppose $\neg \phi$, derive $\neg \phi$ by EFQ, and so I can assert $\phi \rightarrow \neg \phi$ and by modus ponens get to $\neg \phi$, which is obviously a contradiction, so we must have $\neg \neg \phi$, when $\phi$ is a premise. I do think that works, but let me know if you spot a blunder! The line that I have some doubts about is the $\rightarrow$ introduction.

To expand, I now ask myself: why can't I just do the following?

  1. $\phi \hspace{5cm} premise$
  2. $\neg \phi \hspace{4.6cm} assumption$
  3. $\neg \phi \hspace{4.6cm} EFQ, 1,2$
  4. $\neg \neg \phi \hspace{4.2cm} \neg$I

NOTE: 'assumption' means something we are going to discharge eventually, whereas 'premise' as an actual premise/assumption.

EDIT: The axioms I can use, along with the derived rules I mentioned above, are:

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

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

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


1 Answer 1


I don't think your proof is correct. It's hard to say anything exact without knowing the proof system you are working in. Some remarks for your first proof:

  1. For 3. you don't need EFQ, as you already have $\neg\phi$ available in 2.
  2. The introduction of the implication does not work. The assumption is 2., not 1., so the resulting implication is $\neg\phi \to \neg\phi$, which is not very useful.
  3. I do not know which form of negation introduction you are using. I don't understand the conclusion 6.

One way to construct the proof, is to use the definition $\neg\psi := \psi \to \bot$. Then we have a proof

  1. $\phi$ (premise)
  2. $\neg \phi$ (assumption)
  3. | $\phi \land \neg \phi$ ($\land$ introduction)
  4. | $\bot$ (contradiction)
  5. $\neg \phi \to \bot$ (implication introduction)
  6. $\neg\neg \phi$ (definition)

(The lines starting with | are subject to the assumption).

Another way to proceed is to use the negation introduction in https://en.wikipedia.org/wiki/Negation_introduction .

  • $\begingroup$ I am using an axiomatic proof system, the axioms being: $$ (A1) \hspace{1cm} \phi \rightarrow (\psi \rightarrow \phi)\ $$ $$ (A2) \hspace{1cm} \phi \rightarrow (\psi \rightarrow \chi) \rightarrow ((\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \chi))\ $$ $$ (A3) \hspace{1cm}(\neg \phi \rightarrow \neg \psi) \rightarrow (\psi \rightarrow \phi) $$ $\endgroup$
    – Dan Öz
    Commented Nov 4, 2022 at 14:33
  • $\begingroup$ The form of negation introduction I am using is this: if $\Gamma, \phi \vdash \psi$ and $\Gamma, \phi \vdash \neg \phi$, then $\gamma \vdash \neg \phi$ $\endgroup$
    – Dan Öz
    Commented Nov 4, 2022 at 14:39
  • $\begingroup$ So I can't use natural deduction rules such as and-introduction unless I derive them myself. $\endgroup$
    – Dan Öz
    Commented Nov 4, 2022 at 14:53
  • $\begingroup$ I assume you meant: if $\Gamma, \phi \vdash \psi$ and $\Gamma, \phi \vdash \neg \psi$, then $\Gamma \vdash \neg\phi$? $\endgroup$
    – Mentastin
    Commented Nov 4, 2022 at 14:57
  • $\begingroup$ In which case, you immediately have the derivation $\phi, \neg \phi \vdash \phi$ and $\phi, \neg\phi \vdash \neg \phi$ implies $\phi \vdash \neg\neg \phi$, where $\phi$ plays the role of $\Gamma$ and $\psi$ $\endgroup$
    – Mentastin
    Commented Nov 4, 2022 at 14:59

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .