 Axiom X [\(\neg p \rightarrow(p \rightarrow q)\)] may not seem intuitively clear. As a matter of fact, it adds to the precision of the definition of implication. You remember that \(p \rightarrow q\) can be asserted if and only if we possess a construction which, joined to the construction \(p\), would prove \(q\). Now suppose that \(\vdash \neg p\), that is, we have deduced a contradiction from the supposition that \(p\) were carried out. Then, in a sense, this can be considered as a construction, which, joined to a proof of \(p\) (which cannot exist) leads to a proof of \(q\). (Heyting 1956: 102)