Why $\phi \lor \neg \phi $ is not allowed in intuitionistic logic?

Question

Why is $\phi \lor \neg\phi$ not allowed in intuitionistic logic? My professor said this was because intuitionistic logic must have concrete construction.

Further, why is it not possible to write a truth table in intuitionistic logic?

Answer 1

Intuitionistic logic does not consider $\phi\lor\neg\phi$ to be universally valid because that's the way "intuitionistic logic" is defined.

The word "intuitionistic" refers to the intuitionists, a grouping of mathematicians who in the first part of the 1900s made up one side of a Great Controversy about what should be considered a valid proof. Among the arguments they didn't accept were ones of the form

Either $\phi$ is true or it is not. We don't know which, but in each of those cases $\psi$ must be true, so $\psi$ is definitely true.

What we call "intuitionistic logic" today is, however, not the work of the intuitionists themselves. On the contrary the most prominent intuitionists tended to vehemently deny that the validity of an argument could be reduced to a system of rigid rules -- they appealed instead to the mathematician's intuition, hence the name. The system taught in modern textbooks is later workers' attempt to nevertheless find a formal definition that would align more-or-less with what the intuitionists were known to consider good proofs.

So arguably "the reason" why intuitionistic logic doesn't allow the law of excluded middle is simply that it is designed to mimic the opinions of Brouwer and his followers, who did not accept arguments of the above form.

From a modern perspective one might say that intuitionistic logic is by definition the study of what is still provable if one excludes appeals to the law of excluded middle (or other principles that turn out to be equivalent to it).

Even more, though, intuitionistic logic is well suited for expressing arguments in a style where proving something exists also provides an algorithm for constructing it. (The logic is only one part of this program; one also needs to choose one's axioms so they correspond to meaningful "constructive" steps). This is of importance in computer science and allied fields of mathematics, which is a main reason intuitionistic logic is still being studied as more than a technical curiosity.

It so turns out that the resulting notion of provability cannot be described using truth tables in the simple way classical propositional logic can. This is not a design goal, however -- it's just what happens to follow from the set of proof rules we're studying.