I left off last time leaving unanswered the question of what sense could be made of the ill-formed but suggestive kind exression \[A \lol \rtype\] that is, the kind of types that depend on an element of type $A$, but which also somehow linearly 'consume' it.
The answer to this question that I had propounded in my thesis was to go back and say that the kind of even the types eligible for participating in linear logical connectives like $\lol$, $\tensor$, etc. was different from the usual 'type' that classifies regular old nonsubstructural types. Before I explain what that kind is, I want to make a more fuzzy and abstract observation:
I think I see more clearly now than I did then that I was following the same guideline that I (not necessarily with any originality) articulated in an unpublished draft:
That is, each judgment in a judgmental logical system applies to only one distinct syntactic class of proposition-like entities, and if you think you want different judgments to apply to the same propositions, then make up some coercions and trivial syntactic classes if you have to.
I'm not actually going to assert that I really believe in this dogmatically as an Important Principle of the Design of Logics or anything. I don't think that it's a guideline that ought to always be followed, on par with say, You Should Have a Cut Elim Theorem, or Focusing Should Work. But for me it's at least been a useful tool in the toolbox to try to separate out different syntactic classes of propositions and see what happens.
The above fuzzy abstract thinking causes me to say more concretely: when you write down the judgments for linear propositions and you say $\Gamma \prov A\ \mathsf{eph}$ for the judgment of the ephemeral truth of $A$ (as Frank does here) you notice that ephemeral truth is not the same thing as ordinary true-ity true truth. According to (*), the kind of thing that is eligible to be ephemerally true is a different kind of thing that is eligible to be ordinarily true. And the kind of thing that is eligible to be ephemerally true, I'm going to say --- essentially defining what I mean by 'ephemerally true' --- is something that has the function kind \[w \to \rtype\] where $w$ is a fresh type that I am postulating exists, thought of as a type of worlds or type of resources or type of situations in a very intentionally Kripke-semantics sort of way.
An ephemeral proposition, a linear proposition, is a thing of kind $w \to \rtype$, a world-indexed proposition. Well, hold on: so far everything I've said doesn't actually seem at all different from possible-world Kripke semantics of a modal logic. You usually don't, in Kripke semantics, make big sober pronouncements about how What A Modal Proposition Is Is a World-Indexed Proposition, but you certainly could without being wrong --- simply take the relation $w \vDash A$ that says whether a proposition holds at a world and repackage it as a partially applied function. What the meaning of $A$ 'is' is the function $\lambda w . w \vDash A$.
So... I'm inclined to confess that this distinction between, on the one hand, having an external relation like $\models$ and, on the other hand, identifying propositions with their meaning as functions over the other data that $\models$ takes, is possibly inessential and just a question of how you curry stuff around. But (*) makes me prefer the latter option, so I'm going with it for now!
But! One thing that's genuinely different here versus modal logic semantics (but similar to resource semantics for bunched logic!) is that we also postulate some structure on the type $w$, specifically a commutative monoid structure: we assert that we have \[1 : w\] \[\tensor : w \to w \to w\] and that $\tensor$ is associative and commutative and satisfies unit laws.
They're translations into fairly small constructive (and in the Ill-Fated paper's case, polarized and focused) logics, which don't just map provability to truth, but map proofs to proofs bijectively. Maybe you could draw some kind of analogy between how people talk about 'transpilers' as distinct from the general class of compilers to which they nonetheless seem to sort of belong? --- transpilers being things whose target language is typically quite close to their source language, and which is itself probably an interpreted language not necessarily close at all in feel to the full unadorned power of machine code.
Anyhow, the bijection between proofs of the syntax and the proofs in the syntax-after-interpretation is genuinely important, I think. That's the thing that actually makes it a potentially meaningful thing to claim, for example, that a proposition literally is a $w \to \rtype$ rather than merely that a linear proposition can be interpreted as as $w \to \rtype$. This is because if you define a proposition that way, you still can recover the entire proof theory.
One quick check we can do to see if this makes sense is try to prove some proposition known to be provable in linear logic, like for example? \[(A \lol B) \lol (B \lol C) \lol (A \lol C)\] Ok, are there any inhabitants of the type that results from expanding the above definition of $\lol$? Trick question! What results from expanding the definition isn't a type, it's a $w \to \rtype$. So we have to modify our question from 'is this type inhabited' to 'is this linear type inhabited at a particular world'. Which world? Well, in this case, we believe $(A \lol B) \lol (B \lol C) \lol (A \lol C)$ is a tautology, so it should be provable in the empty context, so at the world $1$. Let's expand the definition of $((A \lol B) \lol (B \lol C) \lol (A \lol C))(1)$. It's: \[ \Pi y {:} w . (A \lol B)(y) \to (B \lol C) \lol (A \lol C))(1 \tensor y)\] \[= \Pi y {:} w . (A \lol B)(y) \to \Pi z {:} w . (B \lol C)(z) \lol (A \lol C))(1 \tensor y \tensor z)\] \[= \Pi y {:} w . (A \lol B)(y) \to \Pi z {:} w . (B \lol C)(z) \to \Pi x {:} w . A(x) \to C(1 \tensor y \tensor z \tensor x)\] \[= \Pi y {:} w . (A \lol B)(y) \to \Pi z {:} w . (B \lol C)(z) \to \Pi x {:} w . A(x) \to C( y \tensor z \tensor x)\] \[= \Pi y {:} w . (\Pi t{:} w . A(t) \lol B(y \tensor t)) \to \Pi z {:} w . (\Pi t{:} w . B(t) \lol C(z \tensor t)) \to \Pi x {:} w . A(x) \to C( y \tensor z \tensor x)\] and it's completely straightforward to write down a term that inhabits this type: it's \[\lambda y . \lambda F . \lambda z . \lambda G . \lambda x . \lambda a . G\ (y\tensor x)\ (F\ x\ a)\]
Another logical connective we can easily define in the same way is additive conjunction $\&$. We simply say \[(A \& B)(x) = A(x) \x B(x)\] assuming there's some notion of product types in the language we're interpreting into. Exercise for the reader: pick some proposition involving both $\lol$ and $\&$ and try to prove it at world $1$.
Hey, this actually seems to make sense! If we substitute ((conc A $\tensor$ (hyp A $\lol$ conc C)) $\&$ conc C) for $A$, we get cutAdmissible : $\Pi x {:}w.$ ((conc A $\tensor$ (hyp A $\lol$ conc C)) $\&$ conc C)(x) $\to$ type. and unpacking the definition of $\&$ would give us cutAdmissible : $\Pi x {:}w.$ (conc A $\tensor$ (hyp A $\lol$ conc C))(x) $\to$ (conc C)(x) $\to$ type. and doing a little bit of squinting and guessing and hoping --- I haven't yet said what the propositional connective $\tensor$ is, and I'll be saying more about that in a moment --- we can take a leap of faith to cutAdmissible : $\Pi y {:}w.\Pi z {:}w.$ (conc A)(y) $\to$ (hyp A $\lol$ conc C)(z) $\to$ (conc C) (y $\tensor$ z) $\to$ type. This is the statement of cut admissibility that I arrived at in my thesis! I think it's pretty cool in three ways:
But, at least for me and my personal journey of discovery or whatever, trying to incorporate positives both required understanding focusing a bit better, and provided a bunch of interesting information about what is happening in focusing. More on that next time!
(Prev: "Everything I've Learned About Logic in the Last Decade or So, Part 1")
(Next: "Everything I've Learned About Logic in the Last Decade or So, Part 3")