README⤓ .txt 2026-07-17T121634.146 000000000000768 Logics that drop weakening in order to enforce relevance: the antecedent of a valid implication must actually be used in deriving the consequent, blocking the paradoxes of material and strict implication. The characteristic semantics is the Routley-Meyer ternary relation, with the variable-sharing property as a hallmark.
Ackermann Logic⤓ .md 2026-07-17T120407.600 000000000000832 Ackermann (1956). Rigorous implication. No paradoxes of implication. Relevance precursor. Foundation of relevant logic.
Contraction-Free Logic⤓ .md 2026-07-15T235628.000 000000000016040 Grišin (1982) showed naive comprehension is consistent without contraction; Girard's linear logic (1987) made the rule's absence systematic; Restall, "How to be really contraction free" (1993); Rogerson and Restall (2004) on the residual paradoxes. Various (Grišin, Girard, Restall, Rogerson). No contraction rule. Resource sensitivity. Curry paradox avoidance. Foundation of substructural semantics.
Mingle Logic⤓ .md 2026-07-17T120407.600 000000000000808 Anderson, Belnap (1960s). R plus mingle. Weakened relevance. Intermediate system. Between R and classical.
Relevance Logic⤓ .md 2026-07-15T054404.000 000000000027544 Ackermann's "rigorous implication" (1956). Developed extensively by Alan Anderson and Nuel Belnap (Entailment, 1975, 1992). Motivated by "paradoxes of material implication": in classical logic, A → B holds whenever A is false or B is true, regardless of connection. Relevance logic requires the antecedent be relevant to the consequent.
Relevant Implication⤓ .md 2026-07-15T064408.000 000000000015776 Moh Shaw-Kwei (1950), Anderson and Belnap (1975). Antecedent must be "used" in deriving consequent. Rejects A → (B → A). Variable sharing property. Foundation for relevance logic family.
RM3⤓ .md 2026-07-16T004722.000 000000000030744 The three-element Sugihara matrix, from Sugihara's work on mingle (1955); the logic R-mingle (RM) is Anderson and Belnap's (Entailment I, 1975, §29), and RM3 is its three-valued characteristic matrix, due to Dunn (1970), who proved RM's completeness for the Sugihara algebras and RM3's role among them.
Substructural Logics⤓ .md 2026-07-15T053340.000 000000000028192 Identified through Gentzen's sequent calculus (1934) by analyzing structural rules. Lambek calculus for linguistics (1958). Relevance logic (Anderson & Belnap, 1960s-70s) rejected irrelevant implications. Linear logic (Girard, 1987) rejected contraction and weakening. Unified perspective emerged recognizing the family structure.
Ticket Entailment⤓ .md 2026-07-15T072403.000 000000000014304 Anderson and Belnap (1975). Between strict implication and relevant. Ticket analogy: proof uses but needn't consume. Variable sharing without use constraint. System T.
CRITERIA⤓ .txt 2026-07-17T121634.146 000000000000784 Not sufficient: Variable sharing imposed as a content condition without a substructural calculus (Hyperintensional). Dropping contraction alone (Affine) or exchange alone (Ordered). A linear calculus keyed to exact resource use rather than relevance (Linear).