Non-classical logic

Intuitionistic logic was Brouwer's protest against classical mathematics' free use of indirect proof. To assert P ∨ ¬P, one ought to have either a proof of P or a proof of ¬P; otherwise the disjunction is unwarranted. The same point rejects double-negation elimination: ¬¬P does not by itself give P.

Heyting formalised Brouwer's position in the 1930s. The proof-theoretic strength is comparable to classical logic, but the meaning is different: a proof is a construction, not a demonstration of truth-in-the-abstract. The Curry-Howard correspondence later showed that intuitionistic proofs and typed lambda-calculus programs are the same kind of object.

Łukasiewicz's three-valued logic (1920) adds an indeterminate value I between true and false, for propositions about the future or about vague borderline cases (his original motivation was Aristotle's puzzle of tomorrow's sea-battle). Conjunction, disjunction, and the conditional are redefined as functions on the three-valued lattice.

Once the move is made, the truth-value set can be arbitrary. Boolean two-valued logic is the special case where the set is {T, F}; fuzzy logic (below) is the special case where it is the unit interval.

Fuzzy logic generalises many-valued logic to a continuum: a proposition's truth is a real number between 0 and 1, and connectives are defined as continuous functions on that interval. The operators most commonly used — min for conjunction, max for disjunction, 1 − x for negation — are due to Zadeh's original fuzzy-set framework.

The motivation is to model gradable properties (tall, red, hot) and statements that admit of degree. Fuzzy systems are heavily used in control engineering and consumer electronics; their philosophical credentials as logics are contested, since the semantics is operational rather than truth-conditional.

Classical logic explodes from a contradiction: from P and ¬P, any Q follows. Paraconsistent logics block this. They are appropriate wherever a theory is inconsistent but not therefore worthless — naïve set theory, the early calculus, the contents of large databases, certain dialectical or legal contexts.

Two main strategies. Relevant logics (next entry) require a content-overlap between premises and conclusion. Dialetheism (Priest) accepts that some contradictions are true, then designs a logic that handles them. Both block explosion without giving up too much else.

Classical material implication makes 'If the moon is green, then 2 + 2 = 4' true, because the antecedent is false. Relevant logic refuses this. A valid implication requires a content-overlap between premises and conclusion — formally enforced through tracking which atoms are used in a proof.

Relevant logics are the most natural setting in which to develop paraconsistent reasoning: if irrelevant inferences are blocked, explosion from a contradiction (whose negated atom is irrelevant to most other atoms) is blocked too.

Classical and intuitionistic logics treat premises as stable facts: a proof may invoke a premise as many times as it likes, or not at all. Linear logic treats them as resources: using a premise consumes it. If you have 'one dollar' and 'a dollar buys a coffee', you can derive 'a coffee', but you no longer have the dollar.

Linear logic introduces new connectives that handle the absence of contraction (multiplicative versus additive conjunction and disjunction) and exponentials (the !-operator) that explicitly mark resources eligible for duplication. The system is computationally rich; it underwrites a substantial body of work in concurrency, type theory, and the semantics of computation.