In intuitionistic first-order logic, can the "nothing" quantifier define either of the universal or existential quantifiers?

Question

In classical first-order logic, the nothing quantifier $Nx$, which means "there are no x such that", can define both the universal and existential quantifiers. I suspect this is not the case in intuitionistic first-order logic. I don't think that quantifier can define either of the universal or existential quantifiers. Is this true, and what is the proof?

Answer 1

Your quantifier, which I'll denote $И$, cannot be used to define either the universal or the existential quantifiers in intuitionistic logic. I offer a proof-theoretic argument: needless to say, one needs to know the sequent calculus and the cut-elimination theorem to understand what follows.

I. Frankly, I was not entirely sure why my right and learned colleague grilled you on the inference rules that the $И$ quantifier should satisfy, since there is exactly one sensible way to assign rules to the $И$ quantifier. What's more, it's easy to verify that both possible classical formalizations of $Иx.P(x)$, as either $\forall x. \neg P(x)$ or $\neg \exists x. P(x)$, yield intuitionistically equivalent quantifiers.

Let me start by proving this claim, as it plays a crucial role in the proof I give below.

II. The formulae $\forall x. \neg P(x)$ and $\neg \exists x. P(x)$ are equivalent in intuitionistic logic. An informal natural deduction proof follows.

First, assume that $\forall x. \neg P(x)$ holds, and assume for a contradiction that $\exists x. P(x)$ also holds. By this second assumption we have $P(s)$ for some term $s$, so we can set $x$ to $s$ in the first assumption to obtain $\neg P(s)$, a contradiction. This proves the implication $(\forall x. \neg P(x)) \rightarrow \neg \exists x. P(x)$.

Now assume that $\neg \exists x. P(x)$ holds. Take any $y$, and assume for a contradiction that $P(y)$ holds. Then $\exists x. P(x)$ also holds, contradicting our first assumption. Thus $\neg P(y)$ holds. But we had an arbitrary $y$, so we get $\forall x. \neg P(x)$, and we can conclude $(\neg \exists x. P(x)) \rightarrow \forall x. \neg P(x)$.

So we can define the meaning of $Иx.M(x)$ as either $\forall x. \neg M(x)$ or equivalently as $\neg \exists x. M(x)$, whichever we find more convenient in any given context.

III. From here on, we will use the following general proof-theoretic facts about intuitionistic logic. All three are easily provable by induction on cut-free derivations.

• Existence-disjunction property (see Theorem 4.2.4. of [1], we could use much weaker results): if $\Gamma$ does not contain any existential quantifiers, and $\Gamma \vdash \exists x. M(x)$, then we can find terms $t_1,t_2,\dots t_n$ such that $\Gamma \vdash M(t_1) \vee M(t_2) \vee \dots \vee M(t_n)$.

• Disjunction property: if $\Gamma$ does not contain any disjunction connectives or existential quantiifers, and $\Gamma \vdash M \vee N$, then we can find a proof of either $\Gamma \vdash M$ or $\Gamma \vdash N$.

• Universal independence: If $\Gamma$ contains no universal quantifier, and $\Gamma \vdash \forall x. M(x)$, then $\Gamma \vdash N$ for any formula $N$.

III. Let us prove that $\exists$ cannot be defined in terms of the quantifier $И$ and the usual connectives $\rightarrow, \neg, \vee, \wedge$.

Take a unary atomic predicate symbol $P(x)$ and suppose that we could find a formula $Q$ in the $\{\rightarrow, \neg, \vee, \wedge, И \}$ fragment of Intuitionistic Logic such that $Q \vdash \exists x. P(x)$ and $\exists x. P(x) \vdash Q$ both hold. Given the result of Section II, we can interpret the quantifier $Иx.M$ as an abbreviation for $\forall x. \neg M$. Thus, $Q$ belongs to the $\{\rightarrow, \neg, \vee, \wedge, \forall \}$ fragment of intuitionistic logic.

Since $Q \vdash \exists x. P(x)$, the existence-disjunction property allows us to find $t_1,t_2,\dots t_n$ such that $Q \vdash P(t_1) \vee P(t_2) \vee \dots \vee P(t_n)$. Choose a variable symbol $y$ that does not occur in any of the terms $t_1,t_2,\dots t_n$. We have $P(y) \vdash \exists x. P(x)$. From $\exists x. P(x) \vdash Q$ and the cut rule we get a proof that $P(y) \vdash Q$. From $Q \vdash P(t_1) \vee P(t_2) \vee \dots \vee P(t_n)$ and the cut rule we get a proof that $P(y) \vdash P(t_1) \vee P(t_2) \vee \dots \vee P(t_n)$. Using the disjunction property we could then have $P(y) \vdash P(t_m)$ for some $m$, which is impossible since $y$ does not occur in any of the terms $t_1,t_2,\dots t_n$.

Hence our supposed formula $Q$ cannot exist.

IV. Let us prove that $\forall$ cannot be defined in terms of the quantifier $И$ and the usual connectives $\rightarrow, \neg, \vee, \wedge$.

Take a unary atomic predicate symbol $P(x)$ and suppose that we could find a formula $Q$ in the $\{\rightarrow, \neg, \vee, \wedge, И \}$ fragment of Intuitionistic Logic such that $Q \vdash \forall x. P(x)$ and $\forall x. P(x) \vdash Q$ both hold. This time, given the result of Section II, we interpret the quantifier $Иx.M$ as an abbreviation for $\neg \exists x. M$. Thus, $Q$ belongs to the $\{\rightarrow, \neg, \vee, \wedge, \exists \}$ fragment of intuitionistic logic: in particular $Q$ contains no universal quantifiers. From $Q \vdash \forall x. P(x)$, universal independence gives that $Q \vdash \neg \forall x. P(x)$. Cutting this against our assumption $\forall x. P(x) \vdash Q$ would yield $\forall x. P(x) \vdash \neg \forall x. P(x)$, but we can immediately see that the latter admits no proof.

Hence our supposed formula $Q$ cannot exist.

---

[1] A. S. Troelstra, H. Schwichtenberg: Basic Proof Theory, 2nd edition, web