Does intuitionistic formalism accept the law of exluded middle?

  • 2
    Please do not pose a question and then unregister your account. It means that you will not be able to reply to comments and that your question will never have an accepted answer. Regarding your question, the existence of undecidable propositions in logical systems may lead some to reject the law of the excluded middle.
    – NWR
    Jul 25 '15 at 18:19

In the context of the answer given to your related question, you are using two different definitions of 'intuitionism' from two different historical contexts.

Tarski's notion of intuitionism would eventually accept "tertium non datur" in a weakened form such as that eventually proposed by Quine, as long as the formal process that defines the meaning of a formula is something that can be trained into some natural use. His goal is to capture the feeling of intuitive meaning that individual statements have for readers.

Brower's notion of intuitionism immediately rejected "tertium non datur" because it leads naive speculation directly into paradox. His goal was to keep his reasoning as naive as possible without facing paradox, in the belief that naive reasoning captures an ultimately reliable aspect of human intuition.

The two have virtually nothing in common, and they give different answers to your question.


In general, intuitionism is considered one form of constructivism. The latter forbids to use the law of excluded middle "A or non A". Hence the answer to your question is "No".

In a non-constructivist context the law of excluded middle is the basis for all indirect proofs: In order to prove "A", you show that "non A" is false. According to the law of excluded middle then "A" is true.

As a consequence, indirect proofs are not allowed in an intuitionistic context. That's a severe restriction for the "working mathematician".

Note. Do you mean with "intuitionistic formalism" just a formalization of the principles of intuitionism?

  • 1
    As noted elsewhere, Brower's Intuitionism is not, in intention or effect, a form of constructivism. It is an attempt to propose an alternative to set theory as a resolution of Russel's paradox.
    – user9166
    Jul 27 '15 at 17:43

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.