Affine logic

Affine logic is a substructural logic whose proof theory rejects the structural rule of contraction.

It can also be characterized as linear logic with weakening.

Jean-Yves Girard introduced the name as part of the geometry of interaction semantics of linear logic, which characterizes linear logic in terms of linear algebra; here he alludes to affine transformations on vector spaces.

V. N. Grishin used this logic in 1974,[2] after observing that Russell's paradox cannot be derived in a set theory without contraction, even with an unbounded comprehension axiom.

Affine logic forms the foundation of ludics.