Jason (jcreed) wrote,

So although I'd already worked out the full translation of Liang's LUF straight down into first-order logic, I notice it also has a straightforward double-negation translation into the kind of two-level linear logic that, thanks to neelk, dates all the way back to the mid-90s. Much simpler that way.

This is the thing that always confuses me about classical logic: that it seems to have basically the same number of inference rules but twice as many symbols as the corresponding intuitionistic logic, and you gotta remember which are dual to which. Not a big deal when there's like six of 'em, but more of a big deal with there's 28. Why not just have the 14 and allow them to behave differently on different sides of the turnstile?
Tags: focusing, logic

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded