Affine logic: Difference between revisions

Content deleted Content added

Inline

Latest revision as of 13:45, 28 February 2024

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.

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 transformations on vector spaces.^[1]

Affine logic predated linear logic. 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.^[3] Likewise, the logic formed the basis of a 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 $A\rightarrow B$ as the linear arrow $A\multimap B\otimes \top$ .

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

^ Jean-Yves Girard, 1997. 'Affine'. Message to the TYPES mailing list.
^ Grishin, 1974, and later, Grishin, 1981.
^ Cf. Frederic Fitch's demonstrably consistent set theory

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 32:297-307.
J. Ketonen and G. Bellin, 1989. A decision procedure revisited: notes on Direct Logic. In Linear Logic and its Implementation.

@@ Line 1: / Line 1: @@
-A [[substructural logic]] that denies the [[structural rule]] of [[Idempotency_of_entailment|contraction]]. It can also be characterized as [[linear logic]] with [[weakening]].
+'''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 can be embedded into linear logic by rewriting the affine arrow <math>A \rightarrow B</math> as the linear arrow <math>A {-\!\circ} B \otimes \top</math>.
+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).
-Whereas full linear logic (ie. linear logic with multiplicatives, additives and exponentials) is undecidable, full affine logic is decidable.
+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.
-* Gianluigi Bellin, 1991.  '[http://www.seas.upenn.edu/~sweirich/types/archive/1991/msg00083.html affine logic]'.  Message to the TYPES mailing list.
+* 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.
-* [[Jean-Yves Girard]], 1997.  '[http://www.seas.upenn.edu/~sweirich/types/archive/1997-98/msg00134.html Affine]'.  Message to the TYPES mailing list.
+* 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]]
-* [[Linear logic]]
-* [[Strict logic]] and [[relevant logic]]
-* [[Substructural logic]]
-* [[Ludics]]
-[[Category:Logic]]
 [[Category:Substructural logic]]
 {{logic-stub}}