Editing Bunched logic (section)

===Categorical semantics (doubly closed categories)===
The double version of the deduction theorem of bunched logic has a corresponding category-theoretic structure. Proofs in intuitionistic logic can be interpreted in 
[[cartesian closed]]  categories, that is, categories with finite products satisfying the ([[natural transformation|natural]] in ''A'' and ''C'') [[Adjoint functors|adjunction]] correspondence relating hom sets:
::<math>Hom(A \wedge B, C) \quad \mbox{is isomorphic to} \quad Hom(A, B \Rightarrow C)  </math>
Bunched logic can be interpreted in categories possessing two such structures
::a categorical model of bunched logic is a single category possessing two closed structures, one symmetric monoidal closed the other cartesian closed.
A host of categorial models can be given using Day's [[tensor product]] construction.<ref>{{cite book|last1=Day|first1=Brian|chapter=On closed categories of functors|title=Reports of the Midwest Category Seminar IV |series=Lecture Notes in Mathematics |volume=137|publisher=Springer|date=1970|pages=1–38|chapter-url=https://www.math.rochester.edu/people/faculty/doug/otherpapers/DayReport.pdf}}</ref>
Additionally, the implicational fragment of bunched logic has been given a [[game semantics]].<ref>{{cite book|last1=McCusker|first1=Guy|last2=Pym|first2=David|chapter=A Games Model of Bunched Implications|title=Computer Science Logic |series=Lecture Notes in Computer Science |volume=4646 |publisher=Springer|date=2007|chapter-url=http://www.cs.bath.ac.uk/~gam23/papers/innocentBI.pdf}}</ref>