Yeah, Michael Arntzenius was telling me all about this! Sounds awesome. I was trying to work out for myself what the 'judgmental' story is for that diamond, and my best guess so far is

I think I managed to convince myself that cut-elim holds for that, too. I always hate doing these one-off messy cut proofs, and prefer to get it for free out of encoding the exotic connective out of familiar bits, but this one is a tough nut to crack. Something like the recursive definition

◇A = all a . q(a) -o exists b . q(b) -o !s(a) -o s(b) * ((y(a,b) * A) + (n(a, b) * ◇A))

looks like it is a good step in the right direction (where q and s are arbitrary positive atoms with no axioms, and you axiomatize y and n by

y(a, b) * y(b, c) -o 0

y(a, b) * n(b, c) -o y(a, c)

n(a, b) * y(b, c) -o y(a, c)

n(a, b) * n(b, c) -o n(a, c)

(the absence of n(a, a) is necessary to prevent ◇0)

so that when you try to prove ◇A1, ... ◇An |- ◇C, your premises end up being

A1, ◇A2... ◇An |- C

◇A1, A2... ◇An |- C

...

◇A1, ◇A2... An |- C

and (unfortunately) also

◇A1, ... ◇An |- ◇C

so maybe with some coinduction magic you can let a proof "spin" in the loop at ◇A1, ... ◇An |- ◇C waiting for one of the events to fire. And then figure out how to force C |- ◇C and ◇◇C |- ◇C to hold.

*Edited at 2016-01-21 03:34 pm (UTC)*