One of the most familiar non-classical logics is intuitionism, which, in simple terms, is based upon the rejection of the law of excluded middle: (P ∨ ¬P). There are both philosophical and technical arguments that can be offered in favor of this restriction upon classical logic. Intuitionism was originally developed as a view about the philosophy of mathematics, which maintained that mathematical objects are mental constructions, and that therefore certain branches of traditional mathematics—those involving non constructible objects, such as a completed infinity—are illegitimate. It similarly followed that some mathematical statements involving objects that had not yet been constructed were neither true nor false, and thus the law of excluded middle was invalid. A related line of argument has also been advanced within the philosophy of language. If we suppose that meaning is in part determined by use, then some statements (for example, inaccessible statements about the past) must be understood in terms of their assertibility conditions rather than their truth conditions; the fact that there will be circumstances in which it is not appropriate to assert a statement does not entail that it is appropriate to assert its negation.
Both lines of thought are philosophically controversial.
Another argument for restricting classical logic with respect to the law of excluded middle is based on a consideration of the nature of the logical connectives themselves. It seems reasonable to suppose that any formal language must be entirely neutral with respect to its subject matter; that is, it does not add anything to a proof not already present. One way to make this requirement explicit is for the introduction and elimination rules for the logical connectives to balance each other out, in which case they are said to be harmonious. The introduction and elimination rules for “&” are clearly harmonious in this sense, since we can only introduce (P & Q) if we have already assumed P and Q separately (&-Introduction), and the elimination of (P & Q) only allows us to derive P and Q (&-Elimination). By contrast, however, the introduction and elimination rules for double negation are not harmonious. If we can derive a contradiction on the assumption of ¬P, then we can derive ¬¬P (Reductio ad Absurdum), and from ¬¬P we can derive P (Double Negation Elimination). The elimination rules, therefore, leave us with something that was not previously assumed in the proof (that is, P). Intuitionists therefore conclude that the introduction and elimination rules for double negation must be abandoned, and since this rule is necessary to derive the law of excluded middle, we reach the intended result.
There are several different ways to formalize intuitionist logic. In terms of semantics, it is important to note that while intuitionists reject the law of excluded middle, they do not posit a third (that is, indeterminate) truth value. It is, therefore, not possible to provide a finite truthtable interpretation for intuitionist logic. It is, however, possible to provide an interpretation of the language within a possible worlds framework, with structural similarities to S4. By contrast, in terms of a natural deduction proof theory, it is sufficient to remove the introduction and elimination rules for double negation, along with the Reductio ad Absurdum rule, but it is also necessary to replace them with a more restrictive rule:
Ex Contradictione Quodlibet: “From contradiction, anything [follows]”; given a contradiction (ψ & ¬ψ), we can derive any proposition φ.
This allows a similar range of derivations but without the problematic consequences of unrestricted double negation elimination.
