# Law of excluded middle in intuitionistic formalism

Does intuitionistic formalism accept the law of exluded middle?

• 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?

• 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