Editing Bunched logic (section)

===Proof theory and type theory (bunches)===

The [[proof calculus]] of bunched logic
differs from usual [[sequent calculus|sequent calculi]] in having a tree-like context of [[hypothesis|hypotheses]] instead of a flat list-like structure.  In its sequent-based proof theories, the 
context <math>\Delta </math> in an entailment judgement <math>\Delta \vdash A </math>
is a [[tree (graph theory)|finite rooted tree]] whose leaves are propositions and whose internal nodes are labelled with modes of composition corresponding to the two conjunctions. 
The two combining operators, comma and semicolon, are used (for instance) in the introduction rules for the two implications. 
:<math>\frac{\Gamma,A \vdash B}{\Gamma \vdash A{-\!\!*} B}  \qquad \qquad \frac{\Gamma;A \vdash B}{\Gamma \vdash A{\Rightarrow} B} </math>
The difference between the two composition rules comes from additional rules that apply to them.
* Multiplicative composition <math> \Delta , \Gamma </math> denies the [[structural rule]]s of weakening and contraction.
* Additive composition <math> \Delta ; \Gamma </math> admits weakening and contraction of entire bunches.
The structural rules and other operations on bunches are often applied deep within a tree-context, and not only at the top level: it is thus in a sense a calculus of [[deep inference]].

Corresponding to bunched logic is a type theory having two kinds of function type. Following the [[Curry–Howard correspondence]], introduction rules for implications correspond to introduction rules for function types.
:<math>\frac{\Gamma,x:A \vdash M:B}{\Gamma \vdash \lambda x.M: A{-\!\!*} B}  \qquad \qquad \frac{\Gamma;x:A \vdash M: B}{\Gamma \vdash \alpha x.M:A{\Rightarrow} B} </math>
Here, there are two distinct binders, <math>\lambda</math> and <math>\alpha</math>, one for each kind of function type.

The proof theory of bunched logic has an historical debt to the use of bunches in relevance logic.<ref>{{cite book|last1=Read|first1=Stephen|title=Relevant Logic: A Philosophical Examination of Inference|date=1989|publisher=Wiley-Blackwell}}</ref> But the bunched structure can in a sense be derived from the categorical and algebraic semantics:
to formulate an introduction rule for <math> {-\!\!*} </math> we should mimick <math> * </math> on the left in sequents, and to introduce <math> \Rightarrow</math> we should mimick <math> \wedge </math>. This consideration leads to the use of two combining operators.

James Brotherston has done further significant work on a unified proof theory for bunched logic and variants,<ref>{{cite journal|last1=Brotherston|first1=James|title=Bunched logics displayed|journal=[[Studia Logica]]|date=2012|volume=100|issue=6|pages=1223–1254|url=http://www0.cs.ucl.ac.uk/staff/J.Brotherston/StudiaLogica12/BL_display_SL_final.pdf|doi=10.1007/s11225-012-9449-0|citeseerx=10.1.1.174.8777|s2cid=13634990}}</ref> employing [[Nuel Belnap|Belnap]]'s notion of [[structural proof theory|display logic]].<ref>{{cite journal|last1=Belnap|first1=Nuel|title=Display logic|journal=[[Journal of Philosophical Logic]]|date=1982|volume=11|issue=4|pages=375–417|doi=10.1007/BF00284976|s2cid=41451176}}</ref>

Galmiche, Méry, and Pym have provided a comprehensive treatment of bunched logic, including [[Completeness (logic)|completeness]] and other meta-theory, based on labelled [[Method of analytic tableaux|tableaux]].<ref>{{Cite journal|title = The Semantics of BI and Resource Tableaux|last1 = Galmiche|first1 = Didier|date = 2005|journal = Mathematical Structures in Computer Science|doi = 10.1017/S0960129505004858|last2 = Méry|first2 = Daniel|last3 = Pym|first3 = David|volume = 15|issue = 6|pages = 1033–1088| doi-broken-date=1 November 2024 |citeseerx = 10.1.1.144.1421|s2cid = 1700033}}</ref>