Jason (jcreed) wrote,

Went to a talk by Greg Restall on modal logic using hypersequents. Rather interesting, and a very clear and well-delivered talk to be sure. It occurred to me a little afterwards that I don't really see the difference between a hypersequent

G1 |- D1 | G2 |- D2 | ... Gn |- Dn

and just a plain old sequent in a standard hybrid system with a distinct label for each sequent, like

G1[a1], G2[a2] ... Gn[an] |- D1[a1], D2[a2], ... Dn[an]

In which case the sequent rules Restall gave for S5 box seem to be exactly those that I'd expect for ∀a.A @ a, as it shows up in tom7's thesis for example. On the left, you get to pick a label, or equivalently the sequent within the hypersequent that you travel to, and on the right you create a fresh label, which is equivalent to creating a fresh sequent disjunctively adjoined to all the rest.
Tags: math, talks

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded