Calculus of structures

In mathematical logic, the calculus of structures (CoS) is a proof calculus with deep inference for studying the structural proof theory of noncommutative logic. The calculus has since been applied to study linear logic, classical logic, modal logic, and process calculi, and many benefits are claimed to follow in these investigations from the way in which deep inference is made available in the calculus.

It was first introduced in 2001 in the paper A System of Interaction and Structure by Alessio Guglielmo of the University of Bath.¹²

A formula is a (well-formed) string of logical symbols. For example, ${\displaystyle ((a\land b)\land \neg c)\lor d}$ is a formula.

An equational theory is a list of equations that describe an equivalence relation on the set of all formulas. The usual equations are associativity, commutativity, and equations for logical constants.

A structure is an equivalence class of formulas. The name "structure" emphasizes that CoS does not distinguish sequents and formulas, but uses a single object to do the job of both in a sequent calculus. Specifically, a structure can be regarded as an equivalence class of formulas.

A context is a structure with a sub-structure removed. For example, ${\displaystyle A\land -}$ is a context, where the ${\displaystyle -}$ denotes a removed sub-structure. Contexts are written as ${\displaystyle S\{-\}}$, so for example, if ${\displaystyle S\{-\}:=A\land -}$, then ${\displaystyle S\{B\}}$ is defined as ${\displaystyle A\land B}$.

An inference rule is of form ${\displaystyle {\frac {S\{A\}}{S\{B\}}}}$, where ${\displaystyle A,B}$ are substructures, and ${\displaystyle S\{\}}$ is not any particular formula, but rather an indication that "any context can go here". We can present it in a simplified form as ${\displaystyle {\frac {A}{B}}}$, leaving ${\displaystyle S\{\}}$ implicit. By default, contexts appearing in inference rules must have positive polarity.

A context has a polarity. The polarity of a context is either positive or negative. For example, ${\displaystyle A\lor -}$ is a positive context, but ${\displaystyle A\lor \neg -}$ is a negative context, but ${\displaystyle (A\lor \neg -)\to C}$ is once again a positive context. The positivity or negativity of a context is called its polarity. For example, we say "${\displaystyle A\lor -}$ has positive polarity", and "${\displaystyle A\lor \neg -}$ has negative polarity".

Two structures may be duals to each other. Similarly, two inference rules ${\displaystyle {\frac {S\{A\}}{S\{B\}}},\;{\frac {S\{B'\}}{S\{A'\}}}}$ can also be duals to each other, if it is possible to write ${\displaystyle A'}$ as a dual to ${\displaystyle A}$, and ${\displaystyle B'}$ as a dual to ${\displaystyle B}$. The classical contraposition is an example of this duality.

A convention is to write ${\displaystyle ()}$ for a conjunction, and ${\displaystyle []}$ for a disjunction. For example, in linear logic, one writes ${\displaystyle (A_{1},\dots ,A_{n})}$ for ${\displaystyle A_{1}\otimes \dots \otimes A_{n}}$, and ${\displaystyle [A_{1},\dots ,A_{n}]}$ for ${\displaystyle A_{1}\mathbin {\mbox{⅋}} \dots \mathbin {\mbox{⅋}} A_{n}}$.

In sequent calculus, each inference rule can only produce/eliminate logical connectives on the outermost level of a formula. In particular, this means that most subformulas remain unchanged. In deep inference, each inference rule can rewrite subformulas on any level.

For example, in the sequent calculus for classical logic, the rule$${\displaystyle {\frac {\Gamma ,A,B\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}}$$leaves ${\displaystyle A,B}$ and all their subformulas unchanged. Only the outermost logical connective of ${\displaystyle A\land B}$ is produced.

For deep inference, inference rules may apply to any subformula, arbitrarily deep within the syntax tree. In other words, out of all the nodes in the syntax tree of ${\displaystyle A\land B}$, an inference rule can only manipulate the outermost node. Deep inference allows a rule to manipulate arbitrary node within the syntax tree.

In sequent calculus and natural deduction, a proof is a tree of inference rules. This then produces a fundamental asymmetry: The top of a proof tree are made of many leaf-sequents, but the bottom of a proof tree is a single endsequent. However, many inference rules are symmetric: The top half and the bottom half are mutually derivable.

For example, if one can apply a rule ${\displaystyle {\frac {\Gamma \vdash A\quad \Gamma \vdash B}{\Gamma \vdash A\&B}}(\vdash \&)}$ to produce a proof of ${\displaystyle \Gamma \vdash A\&B}$, then one can also produce a proof of ${\displaystyle \Gamma \vdash A}$, and a proof of ${\displaystyle \Gamma \vdash B}$. In this way, the inference rule ${\displaystyle \vdash \&}$ has a top-down symmetry.

The formalism of sequent calculus makes this top-down symmetry implicit, since the juxtaposition of a sequent ${\displaystyle \Gamma \vdash A}$ and another sequent ${\displaystyle \Gamma \vdash B}$ is not itself a sequent. This means this top-down symmetry is not on the object-level of the proof calculus.

In the calculus of sequents, a proof is a line of inference rules. This places the top-down symmetry in the object level.

SKSg is a CoS for classical propositional logic.

The symbols of SKSg consists of:

• The atoms ${\displaystyle a_{0},{\bar {a}}_{0},a_{1},{\bar {a}}_{1},\dots }$. We say that ${\displaystyle a_{i},{\bar {a}}_{i}}$ are atoms that are dual to each other.
• The connectives ${\displaystyle \lor ,\land }$.
• The units ${\displaystyle \top ,\bot }$.

Negation does not exist in SKSg, since we have demoted negation from a logical connective to merely a pairing between logical atoms.

A structure of SKSg has the following syntax in Backus–Naur form:$${\displaystyle F::=a|{\bar {a}}|\top |\bot |F\lor F|F\land F}$$Without negation, all contexts are positive.

Duality for structures is defined by:$${\displaystyle {\begin{aligned}{\overline {a}}={\bar {a}},&\quad {\overline {\bar {a}}}=a\\{\overline {A\land B}}={\overline {A}}\lor {\overline {B}},&\quad {\overline {A\lor B}}={\overline {A}}\land {\overline {B}}\end{aligned}}}$$The structural inference rules come in 3 dual pairs:

${\displaystyle {\frac {\top }{a\lor {\bar {a}}}}\;(\mathrm {i} \downarrow )}$	${\displaystyle {\frac {\bot }{a}}\;(\mathrm {w} \downarrow )}$	${\displaystyle {\frac {a\lor a}{a}}\;(\mathrm {c} \downarrow )}$
identity	weakening	contraction
${\displaystyle {\frac {a\land {\bar {a}}}{\bot }}\;(\mathrm {i} \uparrow )}$	${\displaystyle {\frac {a}{\top }}\;(\mathrm {w} \uparrow )}$	${\displaystyle {\frac {a}{a\land a}}\;(\mathrm {c} \uparrow )}$
cut	coweakening	cocontraction

The 2 logical inference rules are self-dual:

${\displaystyle {\frac {A\land (B\lor C)}{(A\land B)\lor C}}\;(\mathrm {s} )}$	${\displaystyle {\frac {(A\land B)\lor (C\land D)}{(A\lor C)\land (B\lor D)}}\;(\mathrm {m} )}$
switch	medial

In addition to these rules, there are the following equations:$${\displaystyle {\begin{array}{rcl}A\lor B&=&B\lor A\\A\land B&=&B\land A\\(A\lor B)\lor C&=&A\lor (B\lor C)\\(A\land B)\land C&=&A\land (B\land C)\end{array}}\qquad {\begin{array}{rcl}A\lor \bot &=&A\\A\land \top &=&A\\\top \lor \top &=&\top \\\bot \land \bot &=&\bot \end{array}}\quad }$$All equations of the SKSg system can be replaced by inference rules. The resulting equation-less system is SKS.

This is a valid derivation: $${\displaystyle {\begin{array}{c}(a\lor b)\land a\\\Vert \\((a\lor b)\land a)\land ((a\lor b)\land a)\end{array}}\equiv \left({\frac {\left({\frac {a}{a\land a}}\;(\mathrm {c} \uparrow )\right)\lor \left({\frac {b}{b\land b}}\;(\mathrm {c} \uparrow )\right)}{(a\lor b)\land (a\lor b)}}\;(\mathrm {m} )\right)\land \left({\frac {a}{a\land a}}\;(\mathrm {c} \uparrow )\right)\quad .}$$This is a general principle in deep inference: structural rules on generic formulas can be replaced by the same structural rule on atoms. In this case, cocontraction.

A cut-free derivation is a derivation where ${\displaystyle \mathrm {i} \uparrow }$ is not used. One can eliminate cuts by a technique called splitting.³⁴

Define MLL⁻ to be the proof system of multiplicative linear logic without units.

A formula consists of ${\displaystyle F::=a|{\bar {a}}|F\mathbin {\mbox{⅋}} F|F\times F}$. Here, ${\displaystyle a}$ and ${\displaystyle {\bar {a}}}$ are dual atoms. The equations of duality are $${\displaystyle (A\otimes B)^{\bot }=A^{\bot }\mathbin {\mbox{⅋}} B^{\bot },\quad (A\mathbin {\mbox{⅋}} B)^{\bot }=A^{\bot }\otimes B^{\bot }}$$In particular, negation does not exist anymore, since we have demoted negation from a logical connective to merely a duality between pairs of logical atoms. By definition, ${\displaystyle {\bar {\bar {a}}}=a}$.

The system has the following CoS:⁴$${\displaystyle {\begin{aligned}&\mathrm {i} \downarrow \;{\frac {}{A^{\perp }\mathbin {\mbox{⅋}} A}}&&\mathrm {i} \uparrow \;{\frac {A\otimes A^{\perp }}{}}\\&\mathrm {i} \downarrow \;{\frac {S\{B\}}{S\{(A^{\perp }\mathbin {\mbox{⅋}} A)\otimes B\}}}&&\mathrm {i} \uparrow \;{\frac {S\{B\mathbin {\mbox{⅋}} (A\otimes A^{\perp })\}}{S\{B\}}}\\&\sigma \downarrow \;{\frac {S\{A\mathbin {\mbox{⅋}} B\}}{S\{B\mathbin {\mbox{⅋}} A\}}}&&\sigma \uparrow \;{\frac {S\{A\otimes B\}}{S\{B\otimes A\}}}\\&\alpha \downarrow \;{\frac {S\{A\mathbin {\mbox{⅋}} (B\mathbin {\mbox{⅋}} C)\}}{S\{(A\mathbin {\mbox{⅋}} B)\mathbin {\mbox{⅋}} C\}}}&&\alpha \uparrow \;{\frac {S\{A\otimes (B\otimes C)\}}{S\{(A\otimes B)\otimes C\}}}\\&\mathrm {s} \;{\frac {S\{A\otimes (B\mathbin {\mbox{⅋}} C)\}}{S\{(A\otimes B)\mathbin {\mbox{⅋}} C\}}}\end{aligned}}}$$Each row is a pair of dual rules. The switch rule is dual to itself.

There are 4 initiation rules, two for i↑, and two for i↓. The reason there are two instead of one is that the system has no units ${\displaystyle 1,\bot }$. With the unit ${\displaystyle 1}$ for ${\displaystyle \otimes }$, one can simply subsume ${\displaystyle {\frac {}{A^{\perp }\mathbin {\mbox{⅋}} A}}}$ as a special case of ${\displaystyle {\frac {S\{B\}}{S\{(A^{\perp }\mathbin {\mbox{⅋}} A)\otimes B\}}}}$, where ${\displaystyle S\{-\}}$ is the empty context, and ${\displaystyle B=1}$. Similarly, with the unit ${\displaystyle \bot }$ for ${\displaystyle \mathbin {\mbox{⅋}} }$, one can subsume ${\displaystyle {\frac {A\otimes A^{\bot }}{}}}$ under ${\displaystyle {\frac {S\{B\mathbin {\mbox{⅋}} (A\otimes A^{\perp })\}}{S\{B\}}}}$.

The rules for association ${\displaystyle \alpha }$ and commutation ${\displaystyle \sigma }$ mean that both connectives are associative and commutative. These rules can be replaced with the equations ${\displaystyle (A\otimes B)\otimes C=A\otimes (B\otimes C)}$, etc.

i↑ corresponds to the identity axiom in sequent calculus: ${\displaystyle A\vdash A}$, or equivalently, ${\displaystyle \vdash A^{\bot },A}$.

i↓ corresponds to the cut rule: ${\displaystyle {\frac {\Gamma \vdash \Delta ,A\quad A,\Gamma '\vdash \Delta '}{\Gamma ,\Gamma '\vdash \Delta ,\Delta '}}}$.

The switch rule ${\displaystyle {\frac {S\{A\otimes (B\mathbin {\mbox{⅋}} C)\}}{S\{(A\otimes B)\mathbin {\mbox{⅋}} C\}}}}$ is more subtle. It corresponds to ${\displaystyle S\{A\otimes (B\mathbin {\mbox{⅋}} C)\}\vdash S\{(A\otimes B)\mathbin {\mbox{⅋}} C\}}$. In general, an inference rule of a CoS can be read as a provable sequent in a sequent calculus, by "rotating it 90 degrees".

In MLL⁻, the symbols ${\displaystyle \otimes ,\mathbin {\mbox{⅋}} }$ are logical connectives (conjunction, disjunction), and can only appear on the level of formulas. On the level of sequents, the comma behaves essentially the same as ${\displaystyle \mathbin {\mbox{⅋}} }$, since we have the following inference rule$${\displaystyle {\frac {\vdash \Gamma ,A,B,\Delta }{\vdash \Gamma ,A\mathbin {\mbox{⅋}} B,\Delta }}}$$but it appears on the level of sequents. Similarly, writing two sequents side-by-side within a proof tree has essentially the same behavior as ${\displaystyle \otimes }$, since we have the following inference rule$${\displaystyle {\frac {\vdash \Gamma ,A\quad \vdash B,\Delta }{\vdash \Gamma ,A\otimes B,\Delta }}}$$but it appears on the level of proofs.

In the CoS for MLL⁻, the symbol ${\displaystyle \otimes }$ are manipulated according to rules such that it can do the job of both the logical connective ${\displaystyle \otimes }$ and the side-by-side placement of sequents. Similarly for ${\displaystyle \mathbin {\mbox{⅋}} }$.

In particular, given a proof tree in MLL⁻ sequent calculus, one can convert it to a proof in MLL⁻ CoS if one convert each sequent ${\displaystyle \vdash A_{1},\dots ,A_{n}}$ into ${\displaystyle A_{1}\mathbin {\mbox{⅋}} \dots \mathbin {\mbox{⅋}} A_{n}}$, then convert each side-by-side placement of sequents ${\displaystyle \vdash \Gamma _{1}\quad \dots \quad \vdash \Gamma _{n}}$ with ${\displaystyle \Gamma _{1}\otimes \dots \otimes \Gamma _{n}}$. Then replace each use of inference rule in the sequent calculus with a use of several inference rules in the CoS. This shows that structures are not a mere replication of formulas or sequents, since it has features of both.

Cut elimination corresponds to i↓-elimination.

The SLLS system is the CoS version of the full linear logic. It is much larger than the CoS for MLL⁻.⁵$${\displaystyle {\begin{aligned}&\mathrm {ai} \downarrow \;{\frac {1}{a\mathbin {\mbox{⅋}} {\bar {a}}}}&&\mathrm {ai} \uparrow \;{\frac {a\otimes {\bar {a}}}{\bot }}\\&\mathrm {d} \downarrow \;{\frac {(A\mathbin {\mbox{⅋}} B)\mathbin {\&} (C\mathbin {\mbox{⅋}} D)}{(A\mathbin {\&} C)\mathbin {\mbox{⅋}} (B\oplus D)}}&&\mathrm {d} \uparrow \;{\frac {(A\oplus B)\otimes (C\mathbin {\&} D)}{(A\otimes C)\oplus (B\otimes D)}}\\&\mathrm {p} \downarrow \;{\frac {!(R\mathbin {\mbox{⅋}} T)}{!R\mathbin {\mbox{⅋}} ?T}}&&\mathrm {p} \uparrow \;{\frac {!R\otimes ?T}{?(R\otimes T)}}\\&\mathrm {aw} \downarrow \;{\frac {0}{a}}&&\mathrm {ac} \downarrow \;{\frac {a\oplus a}{a}}&&\mathrm {ac} \uparrow \;{\frac {a}{a\mathbin {\&} a}}&&\mathrm {aw} \uparrow \;{\frac {a}{\top }}\\&\mathrm {nm} \downarrow \;{\frac {0}{0\mathbin {\&} 0}}&&\mathrm {s} \;{\frac {(A\mathbin {\mbox{⅋}} B)\otimes C}{(A\otimes C)\mathbin {\mbox{⅋}} B}}&&\mathrm {m} \;{\frac {(A\mathbin {\&} B)\oplus (C\mathbin {\&} D)}{(A\oplus C)\mathbin {\&} (B\oplus D)}}&&\mathrm {nm} \uparrow \;{\frac {\top \oplus \top }{\top }}\\&\mathrm {nm} _{1}\downarrow \;{\frac {0}{0\mathbin {\mbox{⅋}} 0}}&&\mathrm {m} _{1}\downarrow \;{\frac {(A\mathbin {\mbox{⅋}} B)\oplus (C\mathbin {\mbox{⅋}} D)}{(A\oplus C)\mathbin {\mbox{⅋}} (B\oplus D)}}&&\mathrm {m} _{1}\uparrow \;{\frac {(A\mathbin {\&} B)\otimes (C\mathbin {\&} D)}{(A\otimes C)\mathbin {\&} (B\otimes D)}}&&\mathrm {nm} _{1}\uparrow \;{\frac {\top \otimes \top }{\top }}\\&\mathrm {nm} _{2}\downarrow \;{\frac {0}{0\otimes 0}}&&\mathrm {m} _{2}\downarrow \;{\frac {(A\otimes B)\oplus (C\otimes D)}{(A\oplus C)\otimes (B\oplus D)}}&&\mathrm {m} _{2}\uparrow \;{\frac {(A\mathbin {\&} B)\mathbin {\mbox{⅋}} (C\mathbin {\&} D)}{(A\mathbin {\mbox{⅋}} C)\mathbin {\&} (B\mathbin {\mbox{⅋}} D)}}&&\mathrm {nm} _{2}\uparrow \;{\frac {\top \mathbin {\mbox{⅋}} \top }{\top }}\\&\mathrm {nl} _{1}\downarrow \;{\frac {0}{?0}}&&\mathrm {l} _{1}\downarrow \;{\frac {?R\oplus ?T}{?(R\oplus T)}}&&\mathrm {l} _{1}\uparrow \;{\frac {!(R\mathbin {\&} T)}{!R\mathbin {\&} !T}}&&\mathrm {nl} _{1}\uparrow \;{\frac {!\top }{\top }}\\&\mathrm {nl} _{2}\downarrow \;{\frac {0}{!0}}&&\mathrm {l} _{2}\downarrow \;{\frac {!R\oplus !T}{!(R\oplus T)}}&&\mathrm {l} _{2}\uparrow \;{\frac {?(R\mathbin {\&} T)}{?R\mathbin {\&} ?T}}&&\mathrm {nl} _{2}\uparrow \;{\frac {?\top }{\top }}\\&\mathrm {nz} \downarrow \;{\frac {\bot }{?0}}&&\mathrm {z} \downarrow \;{\frac {?R\mathbin {\mbox{⅋}} T}{?(R\oplus T)}}&&\mathrm {z} \uparrow \;{\frac {!(R\mathbin {\&} T)}{!R\otimes T}}&&\mathrm {nz} \uparrow \;{\frac {!\top }{1}}\end{aligned}}}$$

$${\displaystyle {\begin{aligned}A\otimes B&=B\otimes A&\qquad (A\otimes B)\otimes C&=A\otimes (B\otimes C)&\qquad A\otimes 1&=A\\A\mathbin {\&} B&=B\mathbin {\&} A&(A\mathbin {\&} B)\mathbin {\&} C&=A\mathbin {\&} (B\mathbin {\&} C)&A\mathbin {\&} \top &=A\\A\oplus B&=B\oplus A&(A\oplus B)\oplus C&=A\oplus (B\oplus C)&A\oplus 0&=A\\A\mathbin {\mbox{⅋}} B&=B\mathbin {\mbox{⅋}} A&(A\mathbin {\mbox{⅋}} B)\mathbin {\mbox{⅋}} C&=A\mathbin {\mbox{⅋}} (B\mathbin {\mbox{⅋}} C)&A\mathbin {\mbox{⅋}} 1&=\bot \\??R&=?R&!!R&=!R\\\bot \oplus \bot &=\bot =?\bot &1\mathbin {\&} 1&=1=!1\end{aligned}}}$$

The BV system (Basic System V) can be produced by this CoS:⁶$${\displaystyle {\begin{aligned}&\mathrm {ai} \downarrow \;{\frac {\circ }{a\mathbin {\mbox{⅋}} {\bar {a}}}}&&\mathrm {ai} \uparrow \;{\frac {a\otimes {\bar {a}}}{\circ }}\\&\mathrm {s} \;{\frac {(A\mathbin {\mbox{⅋}} B)\otimes C}{(A\otimes C)\mathbin {\mbox{⅋}} B}}\\&\mathrm {q} \downarrow \;{\frac {(A\mathbin {\mbox{⅋}} B)\triangleleft (C\mathbin {\mbox{⅋}} D)}{(A\triangleleft C)\mathbin {\mbox{⅋}} (B\triangleleft D)}}&&\mathrm {q} \uparrow \;{\frac {(A\triangleleft B)\otimes (C\triangleleft D)}{(A\otimes C)\triangleleft (B\otimes D)}}\end{aligned}}}$$

$${\displaystyle {\begin{aligned}A\otimes B&=B\otimes A&\qquad (A\otimes B)\otimes C&=A\otimes (B\otimes C)&\qquad A\otimes \circ &=A\\A\mathbin {\mbox{⅋}} B&=B\mathbin {\mbox{⅋}} A&(A\mathbin {\mbox{⅋}} B)\mathbin {\mbox{⅋}} C&=A\mathbin {\mbox{⅋}} (B\mathbin {\mbox{⅋}} C)&A\mathbin {\mbox{⅋}} \circ &=A\\&&(A\triangleleft B)\triangleleft C&=A\triangleleft (B\triangleleft C)&A\triangleleft \circ &=A=\circ \triangleleft A\end{aligned}}}$$