Jason (jcreed) wrote,

summary for QC readers: Hey I'm a logician! omg, you are too? Sweet, let's make some babies!

Having a very mathy few days.

Today I mostly spent writing up results about this idea I had yesterday. I am coming to the belief, thanks to discussion with Frank, that it is essentially about understanding focussing via an "active truth" judgment, written "A act" for some proposition A instead of the usual judgment "A true" or perhaps in the case of linear logic "A res". Its meaning is handwavily given by saying the way you prove A act is (think of uniform proofs) by decomposing eagerly on the right. The way you prove some other judgment using active truth hypotheses is by eagerly decomposing them in the context from right to left. But you always start out with truth judgments — it's some structural rules that let you "activate" propositions whenever you like, but the rules defining connectives say you have to keep working on them until you come to an explicit deactivation.

If you think this sounds a heck of a lot like just doing focussing with pointlessly different terminology, you're very close to right. The difference is that the focussing system says you have to do asynchronous things eagerly, and you have to do all synchronous things all the way until you get to some asynchronous connectives again. This other system I'm trying to hack up just says you have to do designated chunks of work all at once, but it lets you say where they start and end. You don't have to work on asynchronous connectives right away, but if you start working on one, you have to finish it.

The advantage of this is that proving cut elimination for the "active truth" system seems to completely bypass all the weird lemmas about shuffling around the ordered context present in Kaustuv's last proof; I think it's because I only have one thing active at once, and not a huge pile of asynchronous connectives that leap into Ω and demand attention. And then by easy invertibility properties it's very easy to show at the very end that it's sound and complete with respect to focussing.
Tags: focussing, math, work

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded