• README ⤓ .txt 2026-10-22T165042.936 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-20T053058.000 000000000037816
  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-10-22T085212.000 000000000037376
  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-10-22T090631.000 000000000041824
  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-10-22T090413.000 000000000048224
  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; Łukasiewicz found a single axiom for the classical fragment and proved it shortest (1948). Church's simply typed λ-calculus (1940) is its Curry–Howard image, though nobody said so until Howard (1969).
• CRITERIA ⤓ .txt 2026-10-22T180154.561 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).