1. In deductive systems enjoying a disjunction and negation , the axiom scheme:
2. The principle asserting the validity of the foregoing axiom scheme. The principle is interpreted as an axiomatic representation of the related principle of bivalence, according to which every statement is either true or false. Excluded middle and bivalence part ways in some circumstances, e.g., in supervaluationist semantics in which there are precisifications in which there are atoms in which neither nor is true (i.e., is neither supertrue nor superfalse) although for every formula , is valid in all models.
A related notion is the weak principle of excluded middle, frequently encountered in the context of intuitionistic and superintuitionistic logics:
The validity of an instance of this scheme with respect to a formula corresponds to the intutionistic notion of ’s being testable. While weak excluded middle is not valid intuitionistically, it may be added to intuitionistic logic to yield the superintuitionistic logic known as .
As a thesis concerning consequence—that is, that may always be a theorem—the principle of excluded middle is dual to the principle of explosion, according to which should always be an antitheorem, so that entails all formulae. As deductive systems not observing the principle of explosion are known as paraconsistent, systems for which excluded middle fails are sometimes called paracomplete.
3. In multiple-conclusion logic, in which consequence is a relation between sets of formulae and , the assertion that any in which formulae is a consequence of an arbitrary set of premises . Given the reading of consequence in multiple-conclusion logic, i.e., that holds if whenever all formulae in are true, some formula in is true, the inference asserts that either is true or is true. That this inference is valid suggests that this formulation of excluded middle is more intimately related to the principle of bivalence than the version involving the scheme .
Although the principle is frequently referred to as tertium non datur or excluded third, some—like philosopher Michael Dummett (1925–2011)—have used tertium non datur to denote the related scheme: