(no subject)

[jcreed]

I think I got around the need for corecursion by just using One More Linear Token: defining

◇A = ∃x.z(x) ⊗ □!(z(x) ⊸ ∀a.q(a) ⊸ ∃b.q(b) ⊗ □!(ℓ(a) ⊸ ℓ(b) ⊗ ((A ⊗ y(a,b)) ⊕ (z(x) ⊗ n (a, b)))

and axiomatizing

z(x) ⊢ 1
1 ⊢ z(*) (for some arbitrarily chosen first-order constant term *)
n(a,b), n(b,c) ⊢ n(a,c)
y(a,b), y(b,c) ⊢ y(a,c)
y(a,b), y(b,c) ⊢ y(a,c)
y(a,b), y(b,c) ⊢ 0
⊢ y(a,a)

lets me prove
◇A, ◇B ⊢ ◇((A ∧ ◇B) ∨ (B ∧ ◇A))
and even
A ⊢ ◇A
without I hope too much collateral damage. Still no ◇◇A ⊢ ◇A, but maybe I can be clever and figure that out somehow.