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 space
In mathematics and physics, a vector space (also called a linear space) is a set (mathematics), set whose elements, often called vector (mathematics and physics), ''vectors'', can be added together and multiplied ("scaled") by numbers called sc ...
s.
Affine logic predated linear logic. V. N. Grishin used this logic in 1974, after observing that
Russell's paradox cannot be derived in a
set theory
Set theory is the branch of mathematical logic that studies Set (mathematics), sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory – as a branch of mathema ...
without contraction, even with an
unbounded comprehension axiom.
[Cf. Frederic Fitch's demonstrably consistent set theory] 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
as the linear arrow
.
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
* 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
Theoretical computer science is a subfield of computer science and mathematics that focuses on the Abstraction, abstract and mathematical foundations of computation.
It is difficult to circumscribe the theoretical areas precisely. The Associati ...
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
Substructural logic
{{logic-stub