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.
Definitions
A formula is a (well-formed) string of logical symbols. For example, <math>((a \and b ) \and \neg c) \or d</math> 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, <math>
A \and -
</math> is a context, where the <math>
-
</math> denotes a removed sub-structure. Contexts are written as <math>S\{-\}</math>, so for example, if <math>S\{-\} := A \and -</math>, then <math>S\{B\}</math> is defined as <math>A \and B</math>.
An inference rule is of form <math>\frac{S\{A\{S\{B\</math>, where <math>A, B</math> are substructures, and <math>S\{\}</math> is not any particular formula, but rather an indication that "any context can go here". We can present it in a simplified form as <math>\frac{A}{B}</math>, leaving <math>S\{\}</math> 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, <math>A \or -</math> is a positive context, but <math>A \or \neg -</math> is a negative context, but <math>(A \or \neg -) \to C</math> is once again a positive context. The positivity or negativity of a context is called its polarity. For example, we say "<math>A \or -</math> has positive polarity", and "<math>A \or \neg -</math> has negative polarity".
Two structures may be duals to each other. Similarly, two inference rules <math>\frac{S\{A\{S\{B\, \; \frac{S\{B'\{S\{A'\</math> can also be duals to each other, if it is possible to write <math>A'</math> as a dual to <math>A</math>, and <math>B'</math> as a dual to <math>B</math>. The classical contraposition is an example of this duality.
A convention is to write <math>()</math> for a conjunction, and <math>[]</math> for a disjunction. For example, in linear logic, one writes <math>(A_1, \dots, A_n)</math> for <math>A_1 \otimes \dots \otimes A_n</math>, and <math>[A_1, \dots, A_n]</math> for <math>A_1 \mathbin{\mbox{⅋ \dots \mathbin{\mbox{⅋ A_n</math>.
Ideas
Deep inference
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<math display="block">\frac{\Gamma, A , B\vdash \Delta}{\Gamma, A \and B\vdash \Delta}</math>leaves <math>A, B</math> and all their subformulas unchanged. Only the outermost logical connective of <math>A \and B</math> 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 <math>A \and B</math>, an inference rule can only manipulate the outermost node. Deep inference allows a rule to manipulate arbitrary node within the syntax tree.
Top-down symmetry
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 <math>\frac{\Gamma \vdash A \quad \Gamma \vdash B}{\Gamma \vdash A\& B}(\vdash \&)</math> to produce a proof of <math>\Gamma \vdash A \& B</math>, then one can also produce a proof of <math>\Gamma \vdash A</math>, and a proof of <math>\Gamma \vdash B</math>. In this way, the inference rule <math>\vdash \&</math> has a top-down symmetry.
The formalism of sequent calculus makes this top-down symmetry implicit, since the juxtaposition of a sequent <math>\Gamma \vdash A</math> and another sequent <math> \Gamma \vdash B</math> 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
Definition
SKSg is a CoS for classical propositional logic.
The symbols of SKSg consists of:
- The atoms <math>a_0, \bar a_0, a_1, \bar a_1, \dots</math>. We say that <math>a_i, \bar a_i</math> are atoms that are dual to each other.
- The connectives <math>\or, \and</math>.
- The units <math>\top, \bot</math>.
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:<math display="block">F ::= a | \bar a | \top | \bot | F \or F | F \and F</math>Without negation, all contexts are positive.
Duality for structures is defined by:<math display="block">\begin{aligned}
\overline{a} = \bar a, &\quad \overline{\bar a} = a \\
\overline{A \and B} = \overline{A} \or \overline{B}, & \quad
\overline{A \or B} = \overline{A} \and \overline{B}
\end{aligned}</math>The structural inference rules come in 3 dual pairs:
{| class="wikitable" style="margin:auto; text-align:center;"
|-
| <math>\frac{\top}{a\lor\bar{a\;(\mathrm{i}\downarrow)</math>
| <math>\frac{\bot}{a}\;(\mathrm{w}\downarrow)</math>
| <math>\frac{a\lor a}{a}\;(\mathrm{c}\downarrow)</math>
|-
| identity
| weakening
| contraction
|-
| <math>\frac{a\land\bar{a{\bot}\;(\mathrm{i}\uparrow)</math>
| <math>\frac{a}{\top}\;(\mathrm{w}\uparrow)</math>
| <math>\frac{a}{a\land a}\;(\mathrm{c}\uparrow)</math>
|-
| cut
| coweakening
| cocontraction
|}
The 2 logical inference rules are self-dual:
{| class="wikitable" style="margin:auto; text-align:center;"
|-
| <math>\frac{A\land(B\lor C)}{(A\land B)\lor C}\;(\mathrm{s})</math>
| <math>\frac{(A\land B)\lor(C\land D)}{(A\lor C)\land(B\lor D)}\;(\mathrm{m})</math>
|-
| switch
| medial
|}
In addition to these rules, there are the following equations:<math display="block">
\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
</math>All equations of the SKSg system can be replaced by inference rules. The resulting equation-less system is SKS.
Properties
This is a valid derivation:
<math display="block">
\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.
</math>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 <math>\mathrm{i}\uparrow</math> is not used. One can eliminate cuts by a technique called splitting.
MLL⁻
Define MLL⁻ to be the proof system of multiplicative linear logic without units.
A formula consists of <math>F ::= a | \bar a | F \mathbin{\mbox{⅋ F | F \times F</math>. Here, <math>a</math> and <math>\bar{a}</math> are dual atoms. The equations of duality are <math display="block">(A \otimes B)^\bot = A^\bot \mathbin{\mbox{⅋ B^\bot, \quad
(A \mathbin{\mbox{⅋ B)^\bot = A^\bot \otimes B^\bot</math>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, <math>\bar{\bar a} = a</math>.
The system has the following CoS:<math display="block">
\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}
</math>
<math display="block">
\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}
</math>
BV
The BV system (Basic System V) can be produced by this CoS:<math display="block">
\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}
</math>
<math display="block">
\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}
</math>
References
Further reading
- Kai Brünnler (2004). Deep Inference and Symmetry in Classical Proofs. Logos Verlag.
External links
- Calculus of structures homepage
- CoS in Maude: page documenting implementations of logical systems in the calculus of structures, using the Maude system.