### (no subject)

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.

◇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.