nLab affine logic

Affine logic is a substructural logic which omits the contraction rule but not the weakening rule.

Categorically, affine logic is modeled by (symmetric) monoidal categories whose tensorial unit II is terminal, also known as semicartesian monoidal categories, an example of which is the category of affine spaces, giving rise to the name of the logic.

A more general notion of model would be given by monoidal categories equipped with a natural (in AA) family AIA\to I of arrows implementing “weakening” at each object. However, such an interpretation is in general badly behaved, unless we additionally require the natural transformation given by the maps AIA\to I to be monoidal, and it can be shown that this additional requirement already forces the tensorial unit to be terminal (specifically, this follows from the component at II being the identity).

An example of the badly behaved case – where the transformation is not monoidal, and the tensorial unit is not terminal – is given by the category Rel of relations, with cartesian product as tensor product (i.e., with RelRel as cartesian bicategory). Here a natural family of relations AIA\to I is given by picking empty relations everywhere. In the corresponding interpretation of affine logic, any weakening yields an empty relation, which contradicts intuitive principles like for example that “adding a dummy variable to a proof and then substituting a closed term” should not change the semantics.

Last revised on August 18, 2016 at 14:39:59. See the history of this page for a list of all contributions to it.