# nLab linear-non-linear logic

Contents

foundations

## Removing axioms

#### Monoidal categories

monoidal categories

# Contents

## Idea

Linear-non-linear logic is a presentation of intuitionistic linear logic that decomposes the $!$ modality into an adjunction of between a syntax for a cartesian logic and a linear logic with cartesian variables.

The semantics of linear-non-linear logic is more direct than that of intuitionistic linear logic: it is based on a symmetric monoidal adjunction where the source of the left adjoint is a cartesian monoidal category.

• If the linear context is restricted to having at most one variable, the judgmental structure of linear-non-linear logic coincides with call-by-push-value with stacks.

## References

Created on April 20, 2018 at 14:00:38. See the history of this page for a list of all contributions to it.