# Reductio ad absurdum, but just once

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.

• 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. – 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)$$:

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)$$.

• 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 \}$. – Daniel Schepler Dec 6 '18 at 0:32
• 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. – ryan221b Dec 6 '18 at 2:04
• 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)$? – Daniel Schepler Dec 6 '18 at 4:26
• 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. – ryan221b Dec 6 '18 at 11:11
• 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... – Daniel Schepler Dec 6 '18 at 18:12