Intuitionistic negation (Q2534157)

\textit{A. Heyting} [Intuitionism. An introduction. Amsterdam: North-Holland (1956; Zbl 0070.00801)], uses two distinct types of negation. Suppose \(p\) is a proposition and \(F\) is any contradiction. First, the negation of \(p\) has been proved, \(\vdash\,\sim p\), if it has been shown that the supposition of \(p\) leads to a contradiction, \(\vdash\,p\to F\). Heyting calls this ``de jure'' falsity. Secondly, \(\vdash\,\sim p\) if it is certain that \(p\) can never be proved. I have called this ``in absentia'' falsity. In this paper I argue that ``de jure'' falsity and ``in absentia'' falsity are incompatible in intuitionistic mathematics.