Editing Bunched logic (section)

===Truth-functional semantics (resource semantics)===
The easiest way to understand these formulae is in terms of its truth-functional semantics. In this semantics a formula is true or false with respect to given resources. 
<math>A*B </math> asserts that the resource at hand can be decomposed into resources that satisfy <math>A</math> and <math>B</math>. 
<math> B {-\!\!*} C </math> says that if we compose the resource at hand with additional resource that satisfies <math>B</math>, then the combined resource satisfies <math>C</math>. <math> \wedge </math> and <math> \Rightarrow </math> have their familiar meanings.

The foundation for this reading of formulae was provided by
a forcing semantics <math> r \models A </math> advanced by Pym, where the forcing relation means {{'}}''A'' holds of resource ''r''{{'}}. The semantics is analogous to  Kripke's semantics of [[intuitionistic logic|intuitionistic]] or [[modal logic]], but where the elements of the model are regarded as resources that can be composed and decomposed, rather than as possible worlds that are accessible from one another. For example, the forcing semantics for the conjunction is of the form
::<math>r \models A * B \quad \mbox{iff} \quad \exists r_Ar_B.\,r_A \models A,\, r_B \models B,\,\mbox{and}\,r_A \bullet r_B \leq r </math>
where <math> r_A \bullet r_B </math> is a way of combining resources and <math> \leq </math> is a relation of approximation.

This semantics of bunched logic draws on prior work in [[relevance logic]] (especially the [[operational semantics]] of Routley–Meyer), but differs from it by not requiring  <math> r \bullet r  \leq r </math> and by accepting the semantics of standard intuitionistic or classical versions of <math> \wedge </math> and <math> \Rightarrow </math>. The property <math> r \bullet r  \leq r </math>  is justified when thinking about relevance but denied by considerations of resource; having two copies of a resource is not the same as having one, and in some models (e.g. [[memory heap|heap]] models) <math> r \bullet r </math> might not even be defined. The standard semantics of  <math> \Rightarrow </math> (or of negation) is often rejected by relevantists in their bid to escape the `paradoxes of material implication', which are not a problem from the perspective of modelling resources and so not rejected by bunched logic. The semantics is also related to the 'phase semantics' of [[linear logic]], but again is differentiated by accepting the standard (even boolean) semantics of <math> \wedge </math> and <math> \Rightarrow </math>, which in linear logic is rejected in a bid to be constructive. These considerations are discussed in detail in an article on resource semantics by Pym, O'Hearn and Yang.<ref name=POY04>{{cite journal|last1=Pym|first1=David|last2=O'Hearn|first2=Peter|last3=Yang|first3=Hongseok|title=Possible worlds and resources: The semantics of BI|journal=[[Theoretical Computer Science (journal)|Theoretical Computer Science]]|date=2004|volume=315|issue=1|pages=257–305|doi=10.1016/j.tcs.2003.11.020|url=http://www.cs.ucl.ac.uk/staff/p.ohearn/papers/resource.ps|doi-access=free|url-access=subscription}}</ref>