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. Various (Grišin, Girard, Restall, Rogerson). 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: Y = λx.x(x) → ⊥. Y(Y) → ⊥ and Y(Y) from Y(Y) → Y(Y) → ⊥. Needs contraction. Block contraction, block paradox.

RW (Relevant without contraction): R minus contraction. Affine relevant logic. Stronger than linear.

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.