Law of excluded middle in intuitionistic formalism

Question

Does intuitionistic formalism accept the law of exluded middle?

Answer 1

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.

Answer 2

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?