How to understand the Definitions of existential and disjunction of intuitionistic logic. 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?
 A: 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) 
$$
