The Law of Excluded Middle

The law of the excluded middle (LEM)* (aka tertium non datur) refers to a formula of the form

P \oplus P^\perp

where

• (-)^\perp is some kind of negation
• \oplus is some kind of disjunction

In classical logic

When applied to logics, the adjective classical means that they satisfy some form of the law of excluded middle. For example:

• the formula P \lor \lnot P is a theorem of classical propositional logic
• the formula P ⅋ P^\perp is a theorem of classical linear logic

In intuitionistic logic

Conversely, logics are called intuitionistic exactly when they explicitly reject the law of the excluded middle.

Is LEM constructive?

There is a fine line between intuitionistic and constructive logic. The former term refers to the rejection of LEM, while the second usually means that a logic has "computational content."

Pre-1990s literature conflated the two notions, as LEM was seen as the main obstacle to linking logic with computation. However, the advent of linear logic, and later on the discovery of a computational interpretation of classical logic created the need to separate them.

For example, classical linear logic has computational content, so it is constructive. On the other hand, it proves a form of LEM, so it is not intuitionistic. However, the fragment of it that is known as intuitionistic linear logic is an intuitionistic logic.