Jason (jcreed) wrote,
Jason
jcreed

Here's a bit of math that I kind of expect only the people who read my ill-fated paper with Frank will care about, but here's the deal with it anyway:

The paper-with-Frank is about how a variety of (substructural, and also secretly some modal) logics can be very well-simulated (meaning: preserving the reduced nondeterminism imposed by focusing) by a fragment of first-order focused logic (with no fancy substructural stuff!) with just the negative connectives.

These notes are about how you can take the target language of that translation, and go even farther, still preserving the restrictions of the focusing discipline, down to a logic that isn't focused! The price you pay is just that you have to throw back in the positive connectives, and one funny "jumbo connective" Ux.A(x) that binds a first-order variable, and is equivalent to ∀x.A(x) ⇒ #(x), for a distinguished atomic proposition #.
Tags: focusing, math
Subscribe

  • (no subject)

    Something that's bugged me for a long time is this: How many paths, starting at the origin, taking N steps either up, down, left or right, end up at…

  • (no subject)

    Still sad that SAC seems to end up being as complicated as it is. Surely there's some deeper duality between…

  • (no subject)

    I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 13 comments

  • (no subject)

    Something that's bugged me for a long time is this: How many paths, starting at the origin, taking N steps either up, down, left or right, end up at…

  • (no subject)

    Still sad that SAC seems to end up being as complicated as it is. Surely there's some deeper duality between…

  • (no subject)

    I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…