Does the equivalence ($P \rightarrow Q$) $\iff$ ($\lnot P \lor Q$) hold in intuitionistic logic?

Question

Does it maybe hold in one direction but not the other?

Answer 1

$\Leftarrow$ holds but $\Rightarrow$ does not hold.

To show that $\Leftarrow$ holds, suppose $\neg P \vee Q$ holds. Then if $P$, I claim that $P \to Q$ holds. In the first case, $\neg P$ and $P$ form a contradiction, so $Q$. If $Q$, then clearly $Q$. Thus $P \to Q$.

To show that $\Rightarrow$ does not hold, find a model of intuitionistic logic where $P \to Q$ holds but $\neg P \vee Q$ does not hold. Intutionistic logics are modeled by Heyting algebras, so to prove that $P \to Q$ does not imply $\neg P \vee Q$, it suffices to find a Heyting algebra where $((P \to Q) \Rightarrow (\neg P \vee Q))$ is not 1. An Heyting algebra where this is true is given by the third example on this Wikipedia page. Let $P = ½$, $Q = ½$. Then $P \to Q = 1$ but $\neg P \vee Q = ½$. Then $((P \to Q) \Rightarrow (\neg P \vee Q)) = 0$, which is not 1, so we are done.