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

  • (no subject)

    Walked around UW-madison campus yesterday. It was almost entirely deserted, peaceful, cold. The passageways between buildings were as often as…

  • (no subject)

    Today I saw a really aesthetically great scene: there was a guy shuffling along the sidewalk, and the wind picked up and the rainwater falling from…

  • (no subject)

    About ten years ago, in the beginning of the calendar year 2000, 19-year-old me took some classes including "15-312" * and "Category Theory", and…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded