# How to develop an effective notation for a partially ordered logic?

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, 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?

• 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 May 19 '14 at 13:31
• @MartinBerger: The ultimate goal is using this logic as the basis for a type system for a functional language for systems programming. – pyon May 19 '14 at 15:34
• Typing systems are often easily seen as logics presented in natural deduction style. – Martin Berger May 19 '14 at 15:39
• Maybe the sequent calculus for multiplicative noncommutative logic by Abrusci and Ruet may be an inspiration? – Damiano Mazza May 20 '14 at 7:42
• @DamianoMazza: Thanks, I am going to have a look. – pyon May 20 '14 at 8:16