Does intuitionistic negation of A mean that there does not exist a proof of A?

Question

Section 13 of Kleene's Intoduction to Metamathematics introduces briefly Brouwer's informal intuitionistic school of thought. There he writes that the interpretation of not A is meant to be taken as A implies a contradiction.

From this definition, is it wrong to also interpret not A as there does not exist a proof of A?

If this were the case I would better understand the non-acceptance of double negation elimination. Because then, not not A asserts that there doesn't exist a disproof of A however, from only that assertion we cannot construct an existential proof of A.

Answer 1

It is not the same. The semantics of intuitionistic logic is proof theoretic, so A → B is interpreted as "given a proof of A a proof of B can be constructed". Then A → F means a contradiction can be derived given a proof of A, i.e. a disproof of A can be constructed. The double negation elimination is blocked because a proof of F from ¬A does not give us a (constructive) proof of A. The law of excluded middle is blocked because we may not be able to prove either A → F or ¬A → F, A may be undecidable. See Can one prove by contraposition in intuitionistic logic? on Math SE for more insight.

That there does not exist a proof of A is much weaker than its negation. Negation as failure to find a proof is used in some automated proof systems, like Prolog, as a pragmatic backstop.