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.
Tags:
• #### (no subject)

Something that's bugged me for a long time is this: How many paths, starting at the origin, taking N steps either up, down, left or right, end up at…

• #### (no subject)

Still sad that SAC seems to end up being as complicated as it is. Surely there's some deeper duality between…

• #### (no subject)

I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic