Krdytkyu

Can we prove that $exists x lnot F$ follows from $lnot forall x F$ by natural deduction using the intuitionistic rules, and RAA (reductio ad absurdum) just once?

It is usually done by using RAA twice on the assumptions $lnot F$ and $lnot exists x lnot F$. I know that $forall x F$ doesn't follow from $lnot exists x lnot F$ in intuitionistic logic, so we cannot derive $exists x lnot F$ from $forall x F, lnot forall x F$. Moreover, if we introduced $exists x lnot F$ by RAA, we would have to derive $bot$ from $lnot exists x lnot F, lnot forall x F$; if we introduced $exists x lnot F$ by $exists$-intro, we would have to derive $lnot F$ from $lnot forall x F$ using RAA just once, which seems not quite likely... In both cases I don't know how to proceed.

You cannot derive $lnotforall x F(x) rightarrow exists xlnot F(x)$ in an intuitionistic system without RAA. This is because there is a Soundness Theorem for intuitionistic logic with respect to Kripke Semantics (https://en.wikipedia.org/wiki/Kripke_semantics#Semantics_of_intuitionistic_logic; I spell them out a bit below): if we could derive that implication using the rules (without RAA), then the formula would be valid in all Kripke Models. However, we can construct a counter-example in which $lnotforall x F(x) rightarrow exists xlnot F(x)$ does not hold, so it cannot be derived.

Consider the following Kripke Structure $mathcal{K} = (K, leq, D, Vdash)$:

Since $0leq1$, $1notVdash F(b)$ and $bin D(1)$, we have $0notVdashforall x F(x)$, and also $1notVdashforall x F(x)$, so $0Vdash lnotforall x F(x)$. But at 0, there is no $din D(0)$ satisfying $lnot F(d)$, so $0notVdashexists x lnot F(x)$. Hence, $0notVdashlnotforall x F(x) rightarrow exists xlnot F(x)$.

In case you're unfamiliar with Kripke Structures. $(K, leq)$ is a partially ordered set where you can consider the elements of $K$ to be "states of knowledge": at each stage $kin K$ we "know" some theorems but perhaps not others, which may be proved or refuted at a later stage $k' geq k$. Each state has a domain of objects, $D(k)$, and $Vdash$ tells us which sentences hold at each node.

Two observations:

1. Objects do not "disappear" once constructed: $k leq k' implies D(k) subset D(k')$.


2. Proved theorems remain proved: $k Vdashvarphi implies k' Vdashvarphi$ for all $k' geq k$.

(You can easily see that the example above satisfies these conditions.)

We can now stipulate the conditions under which $k Vdashvarphi$:

• 
  $kVdash F(d) iff$ $F(d)$ holds at $k$ and $din D(k)$;


• 
  $kVdash lnotvarphi iff$ for all $k'geq k$, $k'notVdashvarphi$;


• 
  $kVdash varphilandpsi iff kVdashvarphi text{ and } kVdashpsi$;


• 
  $kVdash varphilorpsi iff kVdashvarphi text{ or } kVdashpsi$;


• 
  $k Vdash varphirightarrowpsi iff $ for all $k' geq k$, $k'Vdashvarphi$ implies $k'Vdashpsi$;


• 
  $kVdashforall x F(x) iff $ for all $k' geq k$ and all $din D(k')$, $k'Vdash F(d)$;


• 
  $kVdashexists x F(x) iff $ there is a $din D(k)$ such that $kVdash F(d)$;

We say that a formula $varphi$ is Kripke valid if, for all Kripke Structures $mathcal{K} = (K, D, Vdash)$ and all $kin K$, $kVdashvarphi$, and we write "$Vdashvarphi$". Writing "$vdash_ivarphi$" for "$varphi$ is intuitionistically provable", we have

Soundness Theorem If $vdash_ivarphi$, then $Vdashvarphi$.

Hence, since we showed that $notVdashlnotforall x F(x) rightarrow exists xlnot F(x)$ (by providing a Kripke Structure as a counter-example), it follows from the Soundness Theorem that $notvdash_ilnotforall x F(x) rightarrow exists x lnot F(x)$.