?

Log in

No account? Create an account
I think I got around the need for corecursion by just using One More… - Notes from a Medium-Sized Island [entries|archive|friends|userinfo]
Jason

[ website | My Website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

[Jan. 22nd, 2016|08:45 pm]
Jason
[Tags|, , ]

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