Is the following a rule which is derivable in intuitionistic logic:

$\neg \neg \forall \neg \neg A \leftrightarrow \forall \neg \neg A$

I thought that I read it somewhere,... hope that someone can help me.

Thank you in advance.

  • $\begingroup$ $\neg \neg A$ is a $\neg\neg$-stable formula (because it's the negation of some formula) hence $\forall x, \neg\neg A$ is as well $\endgroup$ – Max Apr 28 '18 at 14:44

The right to left is trivial, because $p \to \lnot \lnot p$ holds intuitionistically.

For the left to right:

1) $\lnot \lnot \forall x \lnot \lnot A$ --- premise

2) $\lnot A$ --- assumed [a]

3) $\forall x \lnot \lnot A$ --- assumed [b]

4) $\lnot \lnot A$ --- from 3) by $\forall$-elim

5) $\bot$ --- from 2) and 4) by $\to$-elim

6) $\lnot \forall x \lnot \lnot A$ --- from 3) by $\to$-intro, discharging [b]

7) $\bot$ --- from 1) and 6) by $\to$-elim

8) $\lnot \lnot A$ --- from 2) and 7) by $\to$-intro, discharging [a]

9) $\forall x \lnot \lnot A$ --- from 8) by $\forall$-intro.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.