Why is it called linear logic?

Why is it called "Linear" Logic? What's linear about it?

Solution 1:

Girard himself, in his native language (cf. Girard, Cours de Logique I, Hermann, 2006, Section 1.B.2), writes:

"La logique linéaire est issue d'une prise en compte systématique de l'interprétation catégorique. En particulier, les espaces cohérents [...], proches des espaces vectoriels [...] font apparaître des structures logiques familières en algèbre linéaires [...]"

Translation: "Linear logic developed from systematically taking into consideration the categorical interpretation. In particular, coherent spaces [...], similar to vector spaces [...] give rise to logical structures which are familiar from linear algebra."

So, in one sentence, it is called linear logic because it involves semantics which resemble structures from linear algebra.