Notations

Logical systems

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

Notation	Meaning	Connectives
MLL	propositional without units	$X,{\tens},{\parr}$
MLLu	propositional with units only	$\one,\bot,{\tens},{\parr}$
MLL0	propositional with units and variables	$X,\one,\bot,{\tens},{\parr}$
MLL1	first-order without units	$X\vec{t},{\tens},{\parr},\forall x A,\exists x A$
MLL01	first-order with units	$X\vec{t},\one,\bot,{\tens},{\parr},\forall x A,\exists x A$
MLL2	second-order propositional without units	$X,{\tens},{\parr},\forall X A,\exists X A$
MLL02	second-order propositional with units	$X,\one,\bot,{\tens},{\parr},\forall X A,\exists X A$
MLL12	first-order and second-order without units	$X\vec{t},{\tens},{\parr},\forall x A,\exists x A,\forall X A,\exists X A$
MLL012	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}}$).