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.


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.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.