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.

  • $\begingroup$ It seems to me that it shouldn't be possible if you're just using RAA on $\exists x. \neg F$. It's a bit fuzzy for me, but if I recall correctly, the existence property for intuitionistic FOL (since we've already used our one alotted instance of RAA, we're working in intutionistic logic from this point onward) should imply that $\neg \forall x. F, \neg \exists x. \neg F \not\vdash \exists x. \neg F$. Of course, that doesn't rule out a more creative use of RAA, but I don't see how it can be done. $\endgroup$ – user181407 Feb 11 '17 at 21:45

You cannot derive $\lnot\forall x F(x) \rightarrow \exists x\lnot 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 $\lnot\forall x F(x) \rightarrow \exists x\lnot F(x)$ does not hold, so it cannot be derived.

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

enter image description here

Since $0\leq1$, $1\not\Vdash F(b)$ and $b\in D(1)$, we have $0\not\Vdash\forall x F(x)$, and also $1\not\Vdash\forall x F(x)$, so $0\Vdash \lnot\forall x F(x)$. But at 0, there is no $d\in D(0)$ satisfying $\lnot F(d)$, so $0\not\Vdash\exists x \lnot F(x)$. Hence, $0\not\Vdash\lnot\forall x F(x) \rightarrow \exists x\lnot 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 $k\in 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 \Vdash\varphi \implies k' \Vdash\varphi$ 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 \Vdash\varphi$:

  • $k\Vdash F(d) \iff$ $F(d)$ holds at $k$ and $d\in D(k)$;
  • $k\Vdash \lnot\varphi \iff$ for all $k'\geq k$, $k'\not\Vdash\varphi$;
  • $k\Vdash \varphi\land\psi \iff k\Vdash\varphi \text{ and } k\Vdash\psi$;
  • $k\Vdash \varphi\lor\psi \iff k\Vdash\varphi \text{ or } k\Vdash\psi$;
  • $k \Vdash \varphi\rightarrow\psi \iff $ for all $k' \geq k$, $k'\Vdash\varphi$ implies $k'\Vdash\psi$;
  • $k\Vdash\forall x F(x) \iff $ for all $k' \geq k$ and all $d\in D(k')$, $k'\Vdash F(d)$;
  • $k\Vdash\exists x F(x) \iff $ there is a $d\in D(k)$ such that $k\Vdash F(d)$;

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

Soundness Theorem If $\vdash_i\varphi$, then $\Vdash\varphi$.

Hence, since we showed that $\not\Vdash\lnot\forall x F(x) \rightarrow \exists x\lnot F(x)$ (by providing a Kripke Structure as a counter-example), it follows from the Soundness Theorem that $\not\vdash_i\lnot\forall x F(x) \rightarrow \exists x \lnot F(x)$.

| cite | improve this answer | |
  • $\begingroup$ I interpreted the question regarding "only one RAA" as meaning: could you prove something along the lines of $\lnot \forall x, F(x) \rightarrow \lnot\lnot \exists x, \lnot F(x)$. (For which my counterexample in a Heyting algebra model - which I'm much more familiar with personally - would be: Heyting algebra is open subsets of $\mathbb{R}$, domain of discourse is $\mathbb{R}$, $F(x) = \mathbb{R} \setminus \{ x \}$. $\endgroup$ – Daniel Schepler Dec 6 '18 at 0:32
  • $\begingroup$ In the above structure we also have $0\Vdash\lnot\lnot\exists x \lnot F(x)$, so it serves as a counter-example to both implications. $\endgroup$ – ryan221b Dec 6 '18 at 2:04
  • $\begingroup$ If $0 \Vdash \lnot\lnot \exists x \lnot F(x)$ then how is it a counterexample to $\lnot \forall x F(x) \rightarrow \lnot\lnot \exists x \lnot F(x)$? $\endgroup$ – Daniel Schepler Dec 6 '18 at 4:26
  • $\begingroup$ I meant $0\not\Vdash\lnot\lnot\exists x \not F(x)$, but I don't think that actually holds in my example now, I'll need a different counterexample. $\endgroup$ – ryan221b Dec 6 '18 at 11:11
  • 1
    $\begingroup$ How about: $\mathbb{P} = (\mathbb{N}, \le)$; $D(k) = \mathbb{N}$ for all $k$; and $k \Vdash F(n)$ if and only if $k \ge n$. If I'm not mistaken, in this example, $0 \Vdash \lnot \forall x F(x)$ but $0 \not\Vdash \lnot\lnot \exists x \lnot F(x)$ (and in fact $0 \Vdash \lnot \exists x \lnot F(x)$). But I'm not that confident in my computations here... $\endgroup$ – Daniel Schepler Dec 6 '18 at 18:12

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.