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}}$).

Nets

• The free ports of a net Rfp(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').

Miscellaneous

• Isomorphism: $A\cong B$
• injection: $A\hookrightarrow B$
• partial injection: $A\pinj B$