How to understand the Definitions of existential and disjunction of intuitionistic logic.

Question

In the testbook I have learnt that with the natural deduction rules:
$ A \lor B \to (A \to C) \to (B \to C) \to C$

$\exists x A \to \forall x ( A \to B) \to B$

after put $\bot$ into C, B respectively, we get disjunction and existential of intuitionistic logic:

$A \lor B := \lnot A \to (\lnot B \to \bot)$

$\exists x A := \lnot \forall x \lnot A$

---

My question: what's the meaning of putting a $\bot$ here, and why we can constuct intuitionistic disjunction and existential in such a manner?

Answer 1

There are actually two things (two pairs rather) being defined here.

• Your textbook gives the rules $A \lor B \to (A \to C) \to (B \to C) \to C$ and $(\exists x : A(x)) \to \forall x (A(x) \to C) \to C$ which specify how disjunctions $\lor$ and existential formulas $\exists x : A(x)$ are used during a proof. For example to first rule tells us that in order to prove that $C$ follows from $A\lor B$ we must give a proof that $C$ follows from $A$ and an additional proof that $C$ follows from $B$. More specifically, the rules you listed are the elimination rules of $\lor$ and $\exists$ respectively. (Pretty much the same definition can be used in type theory to define sum and $\Sigma$ types)
• To clarify matters, the second pair of definitions should rather be written as $$ A \lor_c B := \neg A \to \neg B \to \bot \hspace{3em} \exists_c x: A(x) := \neg \forall x: \neg A(x). $$ The use of different symbols $\lor_c$ and $\exists_c$ hopefully highlights that they differ from $\lor$ and $\exists$. They are what you could call "classical versions" of $\lor$ and $\exists$ inside of intuitionistic logic and they indeed behave like the classical counterparts. For example you can intuitionistically prove that $$ \neg \forall x: A(x) \leftrightarrow \exists_cx:\neg A(x) $$ which is not possible if we have $\exists$ instead of $\exists_c$ on the right. The two quantifiers are connected though, since we can also show $$ \exists x: A(x) \to \exists_cx: A(x) ~~~~~\text{and}~~~~~ \exists_cx: A(x) \leftrightarrow \neg \neg \, \exists x: A(x) $$