Description: Law of excluded middle, also called the principle oftertium non datur.
Theorem *2.11 of WhiteheadRussell p. 101. It says that something is
either true or not true; there are no in-between values of truth. This is
an essential distinction of our classical logic and is not a theorem of
intuitionistic logic. In intuitionistic logic, if this statement is true
for some ph , then ph is decidable. (Contributed by NM, 29-Dec-1992)