<p>I am developing a logic for reasoning about programs in a resource-constrained environment. My starting point is intuitionistic linear logic, but I made the following changes:</p>

<ol>
<li><p>In intuitionistic linear logic, environments are sets of available resources. In my logic, environments are partially ordered sets: some resources have to be consumed before others.</p>

<ul>
<li><p>Multiplicative conjunction splits into two connectives: parallel conjunction and sequential conjunction.</p></li>
<li><p>Linear implication can only consume a resource X, if there is no other resource Y that must be consumed before X.</p></li>
</ul></li>
<li><p>Logical connectives are usually defined in terms of introduction and elimination rules. In my logic, I need a new kind of rule: <em>usage rules</em>, which describe how a resource can be used in a computation without destroying it.</p>

<ul>
<li><p>I add a new unary operator, called <a href="http://static.rust-lang.org/doc/master/guide-lifetimes.html" rel="nofollow">borrowed pointer</a>, which denotes a non-owning reference to an existing resource.</p></li>
<li><p>Creating a borrowed pointer <em>uses</em> but does not consume the resource being pointed. In particular, one may always create a borrowed pointer to an existing resource X, even if there is some resource Y that must be consumed before X.</p></li>
<li><p>No resource may be consumed until all borrowed pointers to it have been consumed. This is my main motivation for introducing the notion of sequential conjunction in the first place.</p></li>
</ul></li>
</ol>

<p>I want to give a formal presentation of the rules of inference of this logic using natural deduction and sequent calculus. However, I am having trouble coming up with a good notation that succinctly conveys ideas like:</p>

<ol>
<li><p>The environment $\Gamma$ can be split into sub-environments $\Delta, \Sigma$, where there is no resource in $\Sigma$ that must be consumed before any resource in $\Delta$.</p></li>
<li><p>Given the environment $\Gamma$ and a resource $A \in \Gamma$, the result of adding a resource ${\rm ref} A$ to $\Gamma$, in such a way that ${\rm ref} A$ must be consumed before $A$.</p></li>
<li><p>The sequential conjunction of $A$ and $B$.</p></li>
<li><p>etc.</p></li>
</ol>

<p>What guidelines should I follow in order to design a good notation for this logic?</p>

CC BY-SA 3.0
2014-05-19T13:31:32.293Z
There is no absolute notion of good presentation. It all depends on what you want to do with it. For proving meta-theorems like cut-elimination, a sequent style presentation might be suitable. For actual reasoning maybe natural deduction is more appropriate. Etc.
Martin Berger
CC BY-SA 3.0
2014-05-19T15:34:10.880Z
@MartinBerger: The ultimate goal is using this logic as the basis for a type system for a functional language for systems programming.
isekaijin
CC BY-SA 3.0
2014-05-19T15:39:36.400Z
Typing systems are often easily seen as logics presented in natural deduction style.
Martin Berger
CC BY-SA 3.0
2014-05-20T07:42:52.617Z
Maybe the sequent calculus for multiplicative [noncommutative logic](http://en.wikipedia.org/wiki/Noncommutative_logic) by [Abrusci and Ruet](http://dx.doi.org/10.1016/S0168-0072(99)00014-7) may be an inspiration?
Damiano Mazza
CC BY-SA 3.0
2014-05-20T08:16:13.200Z
@DamianoMazza: Thanks, I am going to have a look.
isekaijin
<lo.logic><notation><sequent-calculus><natural-deduction>
How to develop an effective notation for a partially ordered logic?
isekaijin
# How to develop an effective notation for a partially ordered logic?

(Asked by: username_0 on 2014-05-19)

I am developing a logic for reasoning about programs in a resource-constrained environment. My starting point is intuitionistic linear logic, but I made the following changes:

1. In intuitionistic linear logic, environments are sets of available resources. In my logic, environments are partially ordered sets: some resources have to be consumed before others.

   * Multiplicative conjunction splits into two connectives: parallel conjunction and sequential conjunction.
   * Linear implication can only consume a resource X, if there is no other resource Y that must be consumed before X.
2. Logical connectives are usually defined in terms of introduction and elimination rules. In my logic, I need a new kind of rule: *usage rules*, which describe how a resource can be used in a computation without destroying it.

   * I add a new unary operator, called [borrowed pointer](http://static.rust-lang.org/doc/master/guide-lifetimes.html), which denotes a non-owning reference to an existing resource.
   * Creating a borrowed pointer *uses* but does not consume the resource being pointed. In particular, one may always create a borrowed pointer to an existing resource X, even if there is some resource Y that must be consumed before X.
   * No resource may be consumed until all borrowed pointers to it have been consumed. This is my main motivation for introducing the notion of sequential conjunction in the first place.

I want to give a formal presentation of the rules of inference of this logic using natural deduction and sequent calculus. However, I am having trouble coming up with a good notation that succinctly conveys ideas like:

1. The environment $\Gamma$ can be split into sub-environments $\Delta, \Sigma$, where there is no resource in $\Sigma$ that must be consumed before any resource in $\Delta$.
2. Given the environment $\Gamma$ and a resource $A \in \Gamma$, the result of adding a resource ${\rm ref} A$ to $\Gamma$, in such a way that ${\rm ref} A$ must be consumed before $A$.
3. The sequential conjunction of $A$ and $B$.
4. etc.

What guidelines should I follow in order to design a good notation for this logic?

**Tags:** lo.logic, notation, sequent-calculus, natural-deduction

> **Comments:**
> **username_1**: There is no absolute notion of good presentation. It all depends on what you want to do with it. For proving meta-theorems like cut-elimination, a sequent style presentation might be suitable. For actual reasoning maybe natural deduction is more appropriate. Etc.  
> **username_0**: @MartinBerger: The ultimate goal is using this logic as the basis for a type system for a functional language for systems programming.  
> **username_1**: Typing systems are often easily seen as logics presented in natural deduction style.  
> **username_2**: Maybe the sequent calculus for multiplicative [noncommutative logic](http://en.wikipedia.org/wiki/Noncommutative_logic) by [Abrusci and Ruet](http://dx.doi.org/10.1016/S0168-0072(99)00014-7) may be an inspiration?  
> **username_0**: @DamianoMazza: Thanks, I am going to have a look.  

---

## 0 answers

