In classical logic, the law of the excluded middle is formulated as an inference rule that allows one to deduce for any proposition, . I.e., we can assume, for any proposition , that either or its negation can be asserted.

This gets applied in the form of inferring after proving (i.e. we assume not-, then derive a contradiction, and conclude that is assertable).

External links