nLab linear implication

Idea

Linear implication $D \multimap E$ is the most common version of implication/function type in linear logic/linear type theory.

The categorical semantics of linear implication is as the internal hom in the non-cartesian closed monoidal category of types whose tensor product $\otimes$ corresponds to multiplicative conjunction.

Closely related is the multiplicative implication of bunched implication logic, though they behave somewhat differently.

Related concepts

• exponential conjunction

• function type

• hypothetical judgement

Logical operations and notation in linear logic

$\phantom{-}$symbol$\phantom{-}$	$\phantom{-}$in linear logic$\phantom{-}$
$\phantom{A}$$\top$	$\phantom{A}$additive truth
$\phantom{A}$$\bot$	$\phantom{A}$additive falsehood
$\phantom{A}$$0$	$\phantom{A}$multiplicative falsehood
$\phantom{A}$$1$	$\phantom{A}$multiplicative truth
$\phantom{A}$$\multimap$$\phantom{A}$	$\phantom{A}$linear implication$\phantom{A}$
$\phantom{A}$$\otimes$$\phantom{A}$	$\phantom{A}$multiplicative conjunction$\phantom{A}$
$\phantom{A}$$\oplus$$\phantom{A}$	$\phantom{A}$additive disjunction$\phantom{A}$
$\phantom{A}$$\&$$\phantom{A}$	$\phantom{A}$additive conjunction$\phantom{A}$
$\phantom{A}$$\invamp$$\phantom{A}$	$\phantom{A}$multiplicative disjunction$\phantom{A}$
$\phantom{A}$$\;!$$\phantom{A}$	$\phantom{A}$exponential conjunction$\phantom{A}$
$\phantom{A}$$\;?$$\phantom{A}$	$\phantom{A}$exponential disjunction$\phantom{A}$
$\phantom{A}$$^\bot$$\phantom{A}$	$\phantom{A}$negation$\phantom{A}$

References

E.g.

• Daniel Mihályi, Valerie Novitzká, p. 2, 5 of: What about Linear Logic in Computer Science?, Acta Polytechnica Hungarica 10 4 (2013) 147-160 [pdf, pdf]

For more see the references at linear logic.