**meshach**, after plopping myself down in the UC for to read some simplicial geometry stuff when she happened to wander by Si Señor's. I love CMU's persistent random-thoughtful-conversational-people magnet.

In other news, I had this idea yesterday and mumbled to

**aleffert**about it a bit, but now I'm more convinced it's actually sort of correct. Consider the rules for / in Lambek logic:

Ω, B ⊢ A ---------- Ω ⊢ A / B Ω_{*}⊢ B Ω_{L}, A, Ω_{R}⊢ C ------------------------- Ω_{L}, A / B, Ω_{*}, Ω_{R}⊢ C

Notice the left rule lets us decompose A / B somewhere in the middle of the context. Notice also that in the right rule, the proposition is adjoined to the right of the context, and in the left rule, it's the proposition A / B on the left of the associated context Ω

_{*}. Let's write it more like bunched sequent rules, and use the apparently trivial function op(□, □) = □, □ to highlight the associated thingies just mentioned:

op(Ω, B) ⊢ A ---------- Ω ⊢ A / B Ω_{*}⊢ B Δ(A) ⊢ C ------------------------- Δ(op(A / B, Ω_{*})) ⊢ C

But now we're not explicitly referring to any real, structural comma in the context! It's all mediated by op. It's like we've got a prototypical pair of intro/elim rules for an arrow right adjoint to some context-forming operation on the left. So let's try to generalize the hell out of it:

Pick two types, "Prop" for propositions, and "Ctx" for contexts. Suppose there is an injection singleton : Prop → Ctx that creates singleton contexts. Suppose there is a notion of "admissible" function from Ctx

^{n}→ Ctx that is closed up to composition and stuff like that. Suppose ≤ is a relation between Ctx and atomic propositions. Suppose op is some admissible function Ctx

^{2}→ Ctx. Then the following system satisfies cut elimination (in the sense of, if Γ ⊢ A and Δ(A) ⊢ C, then &Delta(Γ) ⊢ C, for any Γ : Ctx and admissible &Delta : Ctx → Ctx) and identity

Γ ≤ p ---------init Γ ⊢ p op(Ω, B) ⊢ A ----------R Ω ⊢ B →_{op}A Ω_{*}⊢ B Δ(A) ⊢ C -------------------------L Δ(op(B →_{op}A, Ω_{*})) ⊢ C

so long as admissible functions satisfy some peculiar axioms that let us tease out dependencies on individual propositions:

- If Γ(Δ) = Ψ(A), then there exist (admissible) Γ' and Δ' such that
- Γ'(Δ'(X), X) = Ψ(X) for all X
- Γ'(Y, A) = Γ(Y) for all Y
- Δ'(A) = Δ

- Γ'(Δ'(X), X) = Ψ(X) for all X
- If f(Δ,Ω) = Ψ(A), then there exist (admissible) &Delta' and Ω' such that
- f(Δ'(X), Ω'(X)) = Ψ(X) for all X
- Δ'(A) = Δ
- Ω'(A) = Ω

- f(Δ'(X), Ω'(X)) = Ψ(X) for all X
- If singleton(B) = Ψ(A), then at least one of the following is true:
- Ψ(X) = singleton(X) for all X (and so A = B)
- Ψ(X) = singleton(B) for all X

- Ψ(X) = singleton(X) for all X (and so A = B)

and ≤ satisfies — and this sort of caught me off guard with how simple it is — identity and cut elimination: we should have singleton(p) ⊢ p, and we should have that Γ ≤ p and Δ(p) ≤ q imply Δ(Γ) ≤ q.

I think this uniformly accounts for cut admissibility theorems for the linear, ordered, and additive and multiplicative bunched function spaces.

And because you can rig up a sensible (i.e. cut-and-identity satisfying) logical system on top of any other sensible system, augmenting it with just one connective, I kind of wonder if this would lead to a nice, general way of modularly adding logical connectives to systems. As it stands, it isn't really that good, since the new connective doesn't "infect" the mutual recursion of proposition syntax the way you want it to... it just floats on top.