Thought a little about the 'contingent access problem' that was interested in since it came up on twitter.

As far as I got was the following paging-back-in of what I remembered of it: (which may be redundant with stuff you already know, chris?)

If we want to have a three-way connective A -[c]o B pronounced "A linearly implies B contingent on positive atom c being in the context right now", then a candidate shibboleth sequent for whether we've done it right is the nonprovability of

a -[c]o 0, c, c -o a |- 0

where a is also a positive atom. The sequent is attainable (by focusing on a -[c]o n) if at the same time we can (1) consume a and (2) non-destructively observe c. But we can only continue observing c if we don't depend on consuming it in the process of using c -o a.

This sequent suffices to tell us that the "consume c and give it back immediately" strategy

A -[c]o B = c -o c * (A -o B)

is no good, since

c -o c * (a -o 0), c, c -o a |- 0

is easily provable. But also we can see even the "consume c and give it back at the next focusing blur" strategy I tried to propose here is not right. For in that case we get something like

a -[c]o 0 = [c](a -o 0)
= c -o {c}(a -o 0)
= c -o ({c}a -o 0 & a -o {c}0)
= c -o ((c -o a) -o 0 & a -o (c * 0))

and it is possible to prove

c -o ((c -o a) -o 0 & a -o (c * 0)), c, c -o a |- 0
(c -o a) -o 0 & a -o (c * 0), c -o a |- 0
(c -o a) -o 0, c -o a |- 0

Except come to think of it I may have done the translation wrong, because a is a positive atom and shouldn't actually be the locus of a "give-c-back" action. Hmmm.

---

Actually, the left rule I imagine for A -[c]o B is

```Δ |- A   Γ, B |- D  c ∈ Δ, Γ
-------------------------------------------
Δ, Γ, A -[c]o |- D
```

which doesn't preclude

```c, c -o a |- a     0 |- 0
-------------------------
a -[c]o 0, c, c -o a |- 0
```

at all, unless we imagine a focusing discipline where we keep focus on a:
```c, c -o a |- [a]     0 |- 0
-------------------------
[a -[c]o 0], c, c -o a |- 0
```

but then this would mean a failure of completeness of focusing; a sequent that's provable if we don't do focusing, but isn't if we do. This seems to imply that A -[c]o B can't be a negative proposition that allows focusing to flow through to a positive first argument A.
Tags:
• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic