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
  • 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