# Creative Commons Attribution-Share Alike 3.0 Unported (http://creativecommons.org/licenses/by-sa/3.0/)
# {{header
# | title = Law of the excluded middle
# | subtitle = (''tertium non datur'')
# | left =
# | right =
# | shortcut =
# | notes = The [[w:tertium non datur|law of the excluded middle]] is so named because it states that a proposition must be true or false, with no middle ground. It is also known as the ''tertium non datur''.
# }}
#
# {{modules
# | parameters = ''None''
# | importedby = [[From intuitionistic to classical propositional logic]]
# | exportedby = [[Principia Mathematica propositional logic]]
# }}
# To state the axiom, we need formulas including disjunction and negation. The parameter here can be any flavor of propositional logic which defines them, including intuitionistic or classical logic.
param (PROPOSITIONAL Classical_propositional_calculus.ghi () "")
tvar (formula p)
#
# Here is the axiom:
stmt (TertiumNonDatur () () (∨ p (¬ p)))
#
# == Equivalent axioms ==
# Assuming [[Interface:Intuitionistic propositional logic]], a variety of axioms all have the effect of producing classical propositional logic. The law of the excluded middle is one of them. A few others are:
#
# - double negation elimination
# - ¬ ¬ p → p
# - transposition elimination
# - (¬ q → ¬ p) → (p → q)
# - case elimination
# - (p → q) ∧ (¬ p → q) → q
# - Peirce's law
# - ((p → q) → p) → p
#

#
# [[Category:Subsystems of classical logic|{{PAGENAME}}]]