Actually, there is no "neither true nor false" in intuitionistic logic as well, because there is no True and False in a first place. There is only Proven and not Proven.
Don't think in terms of true and false, think in terms of proofs
As I understand it, one can have a proof, or one can have a disproof (I.e. a machine that takes as input a proof of the statement and produces a proof of Falsum), or one can just, not have either of those things.
You never have a “I don’t have a proof” with which to do things with, even if you don’t have a proof.
Regarding the truth of a given statement, you can either say that there is a proof of it, or you can stay silent about it (while possibly saying something about another statement, e.g. saying that there is a proof of the negation of the original statement).
The article states: ¬A is A → ⊥.
But how would you logically express "A is neither proven nor disproven"?
It seems to me that if "A" is proven, and "~A" is disproven, then maybe "~~A" is neither proven nor disproven. Is that right? Since intuitionist logic doesn't have the double negation elimination axiom?
Indeed, that is what ¬A means. "¬A" does not mean "not proven". It means that A implies a contradiction. I.e. It means not A. To have a proof of ¬A is to have a disproof of A.
"A is not proven" is not a statement in the language. You can't express it in the language. (if you want to add on some provability logic on top of intuitionistic logic, you can do that, but the basic language of intuitionistic logic does not have any way of expressing "it hasn't been proven that A".)
The "either it has been proven, or it hasn't been proven" isn't a statement made in the language, but a statement about, how to reason using the language.
"~~A" does not mean "neither proven nor disproven", it means -- -- well, it means what it says. It means not(not(A)) .
If you have a proof of A, you can use that to produce a proof of ~~A , but not the other way around. A proof of ~~A is, a disproof of ~A, essentially saying "if it could be shown that A implied a contradiction, that implication itself would imply a contradiction".