Editing Affine logic

'''Affine logic''' is a [[substructural logic]] whose proof theory rejects the [[structural rule]] of [[Idempotency of entailment|contraction]]. It can also be characterized as [[linear logic]] with [[Monotonicity of entailment|weakening]]. 

The name "affine logic" is associated with [[linear logic]], to which it differs by allowing the weakening rule.  [[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 transformation]]s on [[vector space]]s.<ref>[[Jean-Yves Girard]], 1997.  '[http://www.seas.upenn.edu/~sweirich/types/archive/1997-98/msg00134.html Affine]'.  Message to the TYPES mailing list.</ref>

Affine logic predated linear logic.  V. N. Grishin used this logic in 1974,<ref>Grishin, 1974, and later, Grishin, 1981.</ref> after observing that [[Russell's paradox]] cannot be derived in a [[set theory]] without contraction, even with an [[unrestricted comprehension|unbounded comprehension axiom]].<ref>Cf.  [[Frederic Fitch]]'s [[demonstrably consistent set theory]]</ref>  Likewise, the logic formed the basis of a [[Decidability (logic)|decidable]] sub-theory of [[predicate logic]], called 'Direct logic' (Ketonen & Wehrauch, 1984; Ketonen & Bellin, 1989).

Affine logic can be embedded into linear logic by rewriting the affine arrow <math>A \rightarrow B</math> as the linear arrow<math>A \multimap B \otimes \top</math>.

Whereas full linear logic (i.e. propositional linear logic with multiplicatives, additives, and exponentials) is undecidable, full affine logic is decidable.

Affine logic forms the foundation of [[ludics]].

== Notes ==
<references />

==References==
* V.N. Grishin, 1974. “A nonstandard logic and its application to set theory,” (Russian). Studies in Formalized Languages and Nonclassical Logics (Russian), 135–171. Izdat, “Nauka,” Moscow.
* V.N. Grishin, 1981. “Predicate and set-theoretic calculi based on logic without contraction rules,” (Russian).  Izvestiya Akademii Nauk SSSR Seriya Matematicheskaya 45(1):47-68. 239.  Math. USSR Izv., 18, no.1, Moscow.
* J. Ketonen and R. Weyhrauch, 1984, A decidable fragment of predicate calculus. [[Theoretical Computer Science (journal)|Theoretical Computer Science]] 32:297-307.
* J. Ketonen and G. Bellin, 1989. A decision procedure revisited: notes on Direct Logic.  In ''Linear Logic and its Implementation''.

==See also==
* [[Relevant logic]]
* [[Affine type system]], a [[substructural type system]]

[[Category:Substructural logic]]


{{logic-stub}}