Contraction-Free Logic

Origin. 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.

Models. Resources not duplicable. Bounded use. Curry paradox blocked. Relevant and linear connections.

Formalism.

Contraction rule (rejected): A, A, Γ ⊢ B ───────────── A, Γ ⊢ B

Premise used twice ≠ used once. Resource not freely copyable.

Motivation: Curry paradox. Let κ be a sentence with κ ↔ (κ → ⊥) — naive comprehension supplies one.

κ → (κ → ⊥) [from ↔]
κ → ⊥ [contraction on 1 — the only non-trivial step]
κ [from ↔ and 2]
⊥ [modus ponens] Step 2 is contraction and nothing else. Block contraction, block the paradox — this is Grišin's observation.

RW (Relevant without contraction): R minus contraction. Not "affine relevant" — that is a contradiction in terms. Relevant logics reject weakening; affine logics accept it. RW has neither weakening nor contraction. Stronger than linear logic all the same, since it keeps the distribution of ∧ over ∨ that linear logic gives up.

BCK logic: Combinatory variant. B, C, K combinators. No W (which gives contraction). Affine.

Bounded contraction: Allow contraction up to n times. Soft linear logic. Controlled duplication.

Semantics: Multisets of formulas. Ternary relations. No idempotence of fusion. A ◦ A ≠ A.

Type-theoretic view: Affine types. Use at most once. No implicit copying. Rust's ownership intuition.

Curry-Howard: No diagonal/contraction. Linearity constraint. Resource typing.

Symbols.

Symbol	Unicode	Name	Meaning
◦	U+25E6	White bullet / Fusion	Intensional conjunction; not idempotent
⊢	U+22A2	Right tack / Turnstile	Sequent derivability
→	U+2192	Rightwards arrow / Implication	Residual of fusion
↔	U+2194	Left right arrow / Biconditional	Equivalence, as in the Curry sentence
⊥	U+22A5	Up tack / Falsum	Absurdity; the conclusion Curry derives
κ	U+03BA	Kappa	The Curry sentence, κ ↔ (κ → ⊥)
Γ	U+0393	Gamma / Context	Multiset of premises
∧	U+2227	Logical and	Extensional conjunction; distributes over ∨ in RW
∨	U+2228	Logical or	Extensional disjunction
!	U+0021	Exclamation mark / Bang	Exponential; restores contraction in its scope
C	—	Contraction	The rejected structural rule
W	—	Duplicator	Contraction combinator, absent
RW	—	R without W	Relevant logic minus contraction
BCK	—	BCK logic	Affine implicational combinatory logic

Metatheory. Dropping contraction is precisely what blocks Curry's paradox: Grišin, "Predicate and set-theoretic calculi based on logic without contractions" (1982), proved that unrestricted comprehension is consistent over a contraction-free logic, and Terui, "Light affine set theory: a naive set theory of polynomial time" (2004), sharpened this by showing that naive comprehension over light affine logic is consistent and that its provably total functions are exactly the polynomial-time computable ones. Contraction-free sequent calculi admit cut elimination, and since no rule copies a formula, proof search on the exponential-free fragments terminates: MALL is PSPACE-complete while full propositional linear logic is undecidable (Lincoln, Mitchell, Scedrov and Shankar 1992), the difference being that ! reintroduces contraction. Algebraically the models are residuated lattices that need not be square-increasing, so fusion is not idempotent and A ◦ A ≠ A. Restall, "How to be really contraction free" (1993), showed that absence of the structural rule is not by itself sufficient, since a logic may still contain a contracting implication.

Applies to. Type theory. Paradox blocking. Resource logic. Programming languages.

Limitations. Blocking contraction costs a great deal of ordinary mathematics, since induction and recursion normally use a hypothesis more than once; Terui's light affine set theory secures consistency while capturing only the polynomial-time functions, which is far short of arithmetic. The deduction theorem fails in its unrestricted form, and A → (A → B) no longer yields A → B. Contraction-freedom alone does not secure non-triviality: Restall showed that a logic can lack the structural rule and still validate a contracting implication, and Rogerson and Restall, "Routes to triviality" (2004), exhibited paths to triviality that do not pass through contraction, so each proposed system has to be defended individually rather than by appeal to a general theorem. Restoring duplication through an unrestricted exponential reinstates Curry's derivation inside its scope, so ! cannot be admitted freely alongside naive comprehension.