Is $\lor$ definable in intuitionistic logic? The Wikipedia page mentions that $\{\lor,\leftrightarrow,\bot\}$ and $\{\lor,\leftrightarrow,\neg\}$ are complete sets of operators for intuitionistic logic, and also gives a few equivalences for other operators in terms of $\lor$, but there are no equivalences listed for $\lor$ itself. So my question is whether it is possible to define an expression in $\{\land,\to,\neg\}$ (which also includes $\leftrightarrow,\bot$) that is intuitionistically equivalent to $\lor$ in the sense that it satisfies the "definition"
$$((A\lor B)\to C)\iff((A\to C)\land(B\to C)).\tag{1}$$
(I suspect the answer is no, but I'd like a proof.) This question extends to the classification of all minimal complete operator subsets of $\{\land,\lor,\to,\leftrightarrow,\neg,\top,\bot\}$. Depending on the answer to this question, it seems that we have
$$\{\lor,\leftrightarrow,\neg\},\{\lor,\leftrightarrow,\bot\},\{\lor,\land,\to,\neg\},\{\lor,\land,\to,\bot\}$$
if it is true, otherwise
$$\{\land,\to,\neg\},\{\land,\to,\bot\},\{\land,\leftrightarrow,\neg\},\{\land,\leftrightarrow,\bot\},\{\lor,\leftrightarrow,\neg\},\{\lor,\leftrightarrow,\bot\},\{\to,\leftrightarrow,\neg\},\{\to,\leftrightarrow,\bot\}.$$
 A: I will give the proof of undefinability of $\lor$ using $\land$, $\to$, $\lnot$ in propositional intutionistic logic. Notice that I referred the exercises 2.24 - 2.26 in "Lectures on the Curry-Howard isomorphism" by Morten Heine B. Sørensen and Paweł Urzyczyn.
The formula $\phi$ is negative if every propositional variable occurs only in the form $\lnot p$ and $\lor$ does not occur in $\phi$; that is, it only contains $\land$, $\to$ and $\lnot$ as logical connectives. A notable result is, if $\phi$ is negative formula then $\lnot\lnot\phi\to\phi$ holds intutionistically.
I will give the sketch of the proof. At first, we can prove that following formulas are provable from intutionistic logic:


*

*$\lnot\lnot (\phi\to\psi)\to (\lnot\lnot\phi\to\lnot\lnot\psi)$,

*$\lnot\lnot (\phi\land\psi)\to (\lnot\lnot\phi\land\lnot\lnot\psi)$,

*$\lnot\lnot\lnot\phi\to \lnot\phi$.
From these results and inductive argument, you can prove the theorem.
If $p\lor q$ is equivalent to for some formula $\phi(p,q)$ which occurs only $\land$, $\to$ and $\lnot$, then from above theorem we get
$$\lnot\lnot(\lnot p\lor\lnot q)\to (\lnot p\lor\lnot q).$$
However, it is not intuitionistically valid. You can check it from Heiting algebra given by open subsets of $\Bbb{R}$, taking $p=(-\infty,0)\cup(1,\infty)$ and $q=(-\infty,1)\cup(2,\infty)$.
Note that second-order intutionistic logic can define $\lor$ from second-order quantifier and $\to$ like as:
$$p\lor q := [\forall r :(p\to r)\to ((q\to r)\to r)]$$
