April 10th, 2012

beartato phd

(no subject)

Long but reasonably productive day at work.

I've gotten re-obsessed with some of the ideas in this paper I worked on with Frank a while ago, which shows how to very precisely embed a variety of substructural logics down into a very ordinary nonsubstructural logic, but which has a focusing discipline. What "very precisely" means is that the correctness theorems you prove aren't just an ordinary soundness-completeness pair that show "it's provable here iff it's provable over yonder" --- but also there's an isomorphism between (the choices you make during) the proof search processes before and after embedding.

A new result I managed to sketch over lunch yesterday and today is that you don't even need focusing* in the target language, and you can get focusing in the source language! You can squeeze a crazy big focused substructural logic with multiple adjoint-logicky judgments down into plain ol' unfocused intuitionistic first-order logic. What's that asterisk on "don't even need focusing"? Weeelll you need to let me add a single "jumbo" connective to first-order logic, which I will call [t]x.A(x), which features a term argument t and a proposition argument A, and binds a term variable x. It is morally equivalent to a proposition built out of first-order forall and implication and an atomic proposition:
[t]x.A(x) "=" ∀x.A(x) → a(t,x)
and its inference rules are just the derived rules for that big blob of connectives on the right of the "=". Although I personally used focusing reasoning to come up with that connective, you don't really need to think about focusing to prove harmony for it ~ you just treat it like any other connective and go through the motions of cut and identity.

Anyway, this is the same deal as the F_x and U_x in my Focusing as Token-Passing, which provides much of the proof structure for showing my new idea works.