How to prove rigorously that neither the universal nor the existential quantifier can define the other in intuitionistic logic?

Question

I know that in classical first-order logic, each of the universal and existential quantifier can be used to define the other, and I suspect that in intuitionistic first-order logic, neither can define the other. But how to prove it rigorously? More precisely, how does one prove that neither the universal quantifier nor the existential quantifier can be used to define the other, using the connectives $\land$, $\vee$, $\rightarrow$, and $\neg$, and also the equality symbol $=$?

Answer 1

Partial answer: I show that we can’t define $\exists$ in terms of $\forall$.

We work in the empty language for concrete was, so there are no function symbols or predicate symbols. But the only important detail is that there are no constant symbols.

I claim the following

Lemma: all propositions $\phi(x_1, \ldots, x_n)$ which do not contain an existential quantifier, under the assumptions $\neg \neg \exists x \top$ and $\forall x, y (x = y)$, we can either constructive prove $\phi(x_1, \ldots, x_n)$, or we can constructively prove $\neg \phi(x_1, \ldots, x_n)$.

This can be shown by a simple induction on $\phi$. If $\phi$ is of the form $\top, \bot,$ or $x_1 = x_2$, this is trivial. Equally trivial are the inductive steps for the propositional connectives. Clearly, if we can constructively prove $\phi(x_1, \ldots, x_n, y)$, then we can constructively prove $\forall y (\phi(x_1, \ldots, x_n, y))$. Suppose we can constructively prove $\neg \phi(x_1, \ldots, x_n, y)$. We can prove $\neg \forall y (\phi(x_1, \ldots, x_n, y))$ as follows. Suppose $\forall y (\phi(x_1, \ldots, x_n, y))$. Now suppose $\exists x \top$. Take some $x$. Then $\phi(x_1, \ldots, x_n, x)$. Contradiction. Therefore, $\neg \exists x \top$. Contradiction. Therefore, $\neg \forall y (\phi(x_1, \ldots, x_n, y))$.

This completes the proof of the Lemma. $\square$

Now in particular, if we could write $\exists x \top$ without using an existential quantifier, we could constructively prove one of the following: (1) $\forall x, y (x = y) \land \neg \neg \exists x \top \implies \exists x \top$, or (2) $\forall x, y (x = y) \land \neg \neg \exists x \top \implies \neg \exists x \top$. Obviously, we can’t constructively prove (2), since (2) does not hold in the simple model of a 1-element set. So we must be able to constructively show (1).

However, we cannot constructively show (1) either. We can come up with an extremely simple Kripke model where this fails. Consider the frame $W = \{0, 1\}$ with the usual order, and define $M_0 = \emptyset$ and $M_1 = $ a 1-element set. This Kripke frame satisfies $\forall x, y (x = y)$ and satisfies $\neg \neg \exists x \top$, but it does not satisfy $\exists x \top$.

We can also see this in a purely syntactic way. Define a function $f$ which takes a proposition in the empty language for first-order logic, and outputs a proposition in propositional logic, as follows:

• $f(x = y) = \top$
• $f(\forall y (Q(x_1, \ldots, x_n, y))) = P \implies f(Q(x_1, \ldots, x_n, y))$
• $f(\neg Q(x_1, \ldots, x_n)) = \neg f(Q(x_1, \ldots, x_n))$ (and similarly for $\top, \bot$, and binary connectives)
• $f(\exists y (Q(x_1, \ldots, x_n, y))) = P \land f(Q(x_1, \ldots, x_n, y))$

We can then prove that if we can derive $Q(x_1, \ldots, x_n)$ in first-order logic, we can derive $f(Q(x_1, \ldots, x_n))$ in propositional logic.

In particular, if we could derive $\forall x, y (x = y) \land \neg \neg \exists x \top \implies \exists x \top$, then we could also derive $\neg \neg P \to P$. But this is constructive logic, so can’t derive $\neg \neg P \to P$.