Notations

Logical systems

For a given logical system such as $M L L$ (for multiplicative linear logic), we consider the following variations:

Notation	Meaning	Connectives
$M L L$	propositional without units	$X,{\tens},{\parr}$
$M L L u$	propositional with units only	$\one,\bot,{\tens},{\parr}$
$M L L 0$	propositional with units and variables	$X,\one,\bot,{\tens},{\parr}$
$M L L 1$	first-order without units	$X\vec{t},{\tens},{\parr},\forall x A,\exists x A$
$M L L 01$	first-order with units	$X\vec{t},\one,\bot,{\tens},{\parr},\forall x A,\exists x A$
$M L L 2$	second-order propositional without units	$X,{\tens},{\parr},\forall X A,\exists X A$
$M L L 02$	second-order propositional with units	$X,\one,\bot,{\tens},{\parr},\forall X A,\exists X A$
$M L L 12$	first-order and second-order without units	$X\vec{t},{\tens},{\parr},\forall x A,\exists x A,\forall X A,\exists X A$
$M L L 012$	first-order and second-order with units	$X\vec{t},\one,\bot,{\tens},{\parr},\forall x A,\exists x A,\forall X A,\exists X A$

Formulas and proof trees

Formulas

First order quantification: $\forall x A$ with substitution $A [t / x]$
Second order quantification: $\forall X A$ with substitution $A [B / X]$
Quantification of arbitrary order (mainly first or second): $\forall\xi A$ with substitution $A [τ / ξ]$

Rule names

Name of the connective, followed by some additional information if required, followed by "L" for a left rule or "R" for a right rule. This is for a two-sided system, "R" is implicit for one-sided systems. For example: $\wedge_1 \text{add} L$ .

Semantics

Coherent spaces

Web of the space $X$ : $\web X$
Coherence relation of the space $X$ : large $\coh_X$ and strict $\scoh_X$

Finiteness spaces

Web of the finiteness space $\mathcal A$ : $\web{\mathcal A}$
Finiteness structure of the space $\mathcal A$ : $\mathfrak F(\mathcal A)$ (we use \mathfrak, which is consistent with the fact that $\finpowerset{\web{\mathcal A}}\subseteq \mathfrak F(\mathcal A) \subseteq\powerset{\web{\mathcal A}}$ ).

Nets

The free ports of a net $R$ : $fp(R)$ .
The result of the connection of two nets $R$ and $R'$ , given the partial bijection $f:\mathrm{fp}(R)\pinj \mathrm{fp}(R')$ : $R\bowtie_f R'$ .
The number of loops in the resulting net: $\Inner{R}{R'}_f$ (includes the loops already present in $R$ and $R'$ ).