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	Meaning
C	—	contraction (rejected)
RW	—	R without contraction
BCK	—	B, C, K combinatory logic
◦	U+25E6	fusion (non-idempotent)

Metatheory. Substructural. No contraction. Curry paradox. Resource semantics.

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

Limitations. Weakened reasoning. Proof complexity. Unfamiliar. Mathematical practice uses contraction.