• 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-08-19T200546.000 000000000024560
  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-08-19T200425.000 000000000018568
  Meredith (1960s), named for B, C, K combinators. Implication with weakening but without contraction — K is weakening, so it is contraction alone that is dropped. This is the affine implicational fragment, strictly weaker than the intuitionistic one. Combinator correspondence. Foundation for weak implications.
• Contraction-Free Logic ⤓ .md 2026-08-19T210405.000 000000000019760
  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. No contraction rule. Resource sensitivity. Curry paradox avoidance. Foundation of substructural semantics.
• Implicational Calculus ⤓ .md 2026-08-19T195755.000 000000000036864
  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-17T135416.643 000000000000768
  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).