So is the point you can do ALL THE LOGICS in FF, and you can do FF in the "Target Language"? "Source" and "Target" aren't quite denoteful enough for me.

Yeah yeah sorry.

"lots of logics" -> FF -> FOL+U

FOL+U is ordinary intuitionistic first-order-logic with the U connective.

Do you think there's value/advantage to skipping the FF step? I kind of expected you to be doing that.

I actually worked that out first, yeah.

It's debatable which way's better. I think the two-translation way is just barely edging out the one-translation in my mind right now, having seen both of them. The reason is that there are two warts of the overall translation, and the two-translation approach confines each wart to one of the two phases. The ALL THE LOGICS -> FF step involves the weird continuation-passing translation that you've already seen in the Ill-Fated paper. The FF -> FOL+U step has a pair of intertwined translation functions that do different things to a proposition depending on which side of the turnstile it's on. If you have One Monolithic Translation from ALL THE LOGICS -> FOL+U, it has continuations *and* intertwining, and it's hard to see what's going on all at once.

I buy it. Especially since I do consider the know-which-side-you're-on to be the larger wart, I guess.

So I guess my current take on the world is that focusing makes sense in itself, especially once you have polarities, so the story of just cut and identitying FF and then using that to prove focalization for FF is the one I'd lean towards to deal with FF. As I put it in the SF paper, "The cut admissibility and identity expansion lemmas for the focused sequent calculus are strong enough for the unfocused sequent calculus to inherit its metatheory from the force of the theorems in the focused setting."

What you're emphasizing here is something different and still-interesting-to-me, and something that goes back to the Focusing Linear Logic In Itself note - you're addressing the question of what's the minimum amount of stuff on top of extra logic you need to get the structure of focusing. Is that a reasonable take?

Yeah, the cut and identity proof for FF is really rather easy, and I buy that there's not a huge market for making it any simpler.

Stilllll I can't help but remain a tiny bit sketched out by the dot-dot-dotness of the identity proof, and it makes me feel nice to know there's another proof.

And yeah, I think I do care about "what's the minimum amount of stuff on top of extra logic you need to get the structure of focusing", and the answer (as far as I care) is essentially nothing. The answer is actually "the connective Ux.A(x)", but I think that is barely anything. If we're willing to not be scared by, say, negation as a first-class connective (despite the fact that it's definable from implication and false) we needn't be scared by this U.

Yeah, but Structural Focalization takes care of dot dot dot perfectly. See 2.3.3 and 2.3.4 of the one existing chapter for the clearest discussion I've written, but don't read past that because it's all wrong and I'm fixing it.

Oh right hm I totally forgot that development. I am super scatterbrained tonight.

That said, the separate observation that you need basically nothing to get focusing is very interesting to me as an independent point.

And yeah, I think I do care about "what's the minimum amount of stuff on top of extra logic you need to get the structure of focusing", and the answer (as far as I care) is essentially nothing.

I find myself somewhat depressed by this answer. Since Noam's thesis, I've been thinking of focusing as a good way to talk about effects intelligently. However, if all that's really going is a cunning quasi-CPS translation, since Ux.A(x) is morally ∀x. A(x) → #(x), then focusing fixes evaluation order and *nothing else* --- which means we are still as far from a type-theoretic account of effects as ever.

I mean, it's still great that we can specify evaluation order without also getting control operators (which is the problem with CPS), but I want more! :)

Hmmm interesting. Can you elaborate on what type of statement you're trying to make about what effects are using focusing? I understood Noam's stuff as far as making certain claims about limiting how effects behave, like, observing what polarities of connectives they can commute with, and I don't think I'm either tearing down or adding anything significant to that observation.

Another thing I wanted to say by what I think the essential moral of my translation here is, is that the "tightness" (be it linearity or modality or whatever) of the intuitionistic conclusion is enough to model focusing.

And both of those arrows are translations that are, for each proposition, isomorphisms of proof-sets. In other words, full and faithful functors on the categories whose objects are propositions and whose arrows are proofs.

Er.... I guess I mean to claim that they are full and faithful, but their functoriality itself (that they commute with morphism composition, which'd be cut, right?) is actually not quite obvious to me. Although I hope it's true.