README⤓ .txt 2026-07-17T121634.146 000000000000752 Logics that drop the structural rule of contraction while retaining weakening. A hypothesis may be used at most once, but need not be used at all: resources are consumable but discardable. This is the "use-at-most-once" discipline, weaker than linear logic's exact-use requirement.
Affine Logic⤓ .md 2026-07-15T060307.000 000000000020624 Affine logic is linear logic plus weakening (1980s-90s). Resources can be discarded but not duplicated. "At most once" rather than "exactly once." Related to affine types in programming languages. Girard's work on linear logic provides foundation.
BCK Logic⤓ .md 2026-07-15T072715.000 000000000013248 Meredith (1960s), named for B, C, K combinators. Implication without contraction or weakening. Between minimal and intuitionistic. Combinator correspondence. Foundation for weak implications.
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.
Implicational Calculus⤓ .md 2026-07-17T120407.600 000000000000824 Frege's Begriffsschrift (1879) already isolates it; Łukasiewicz and Tarski studied the axiomatics through the 1920s–30s; Tarski and Bernays gave the standard three axioms; C. A. Meredith (1953) found a single axiom for the classical fragment. Church's simply typed λ-calculus (1940) is its Curry–Howard image, though nobody said so until Howard (1969).
CRITERIA⤓ .txt 2026-07-15T204726.000 000000000006616 Not sufficient: Dropping weakening as well as contraction (Linear). Dropping exchange (Ordered). Dropping weakening for relevance (Relevant). Full structural rules (a classical or intuitionistic base belongs in Algebraic).