April 24th, 2012

beartato phd

(no subject)

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 #.