In intuitionist type theory that I know, $\neg \phi$ is interpreted as a function that takes a proof of $\phi$ and outputs a proof of false.
It seems to me that this is different from the way that classical logicians think of $\neg \phi$. They simply think of it as "not $\phi$", and then think of "$\phi \to \textbf{false}$" as a proof of "not $\phi$".
It seems to me that inuitionist logic is kind of "sneaking an axiom" into the logic by defining $\neg \phi$ as $\phi \to \textbf{false}$, namely the axiom that $(\phi \to \textbf{false})\to \neg \phi$. From my perspective, this should really be seen as a logical axiom, not as a definition of $\neg \phi$.
If you accept that view, then it seems to me that the difference between "proof of negation" and "proof by contradiction" explained in this article becomes less hard.
So how does $\neg \phi \leftrightarrow (\phi\to \textbf{false}) $ fit within the intuitionist philosophy? How is this justified?