Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: logic

Topic: Girard algebras?

James Wood (Apr 11 2020 at 12:38):

As Boolean algebras are to classical logic and Heyting algebras are to intuitionistic logic, is there such a thing as “Girard algebras” for (fragments of) (classical or intuitionistic) linear logic? And is there a version of Stone duality for them?

Eduardo Ochs (Apr 11 2020 at 13:22):

James Wood said:

As Boolean algebras are to classical logic and Heyting algebras are to intuitionistic logic, is there such a thing as “Girard algebras” for (fragments of) (classical or intuitionistic) linear logic? And is there a version of Stone duality for them?

Can you tell us more about what you know about models for fragments of Linear Logic?
If you know very little, a good place to start is section 1.7.2 of Abramsky/Tzevelekos: https://arxiv.org/pdf/1102.1313.pdf
This is a great resource too, but it's more advanced: https://www.irif.fr/~mellies/papers/panorama.pdf

James Wood (Apr 11 2020 at 14:11):

Everything in that section 1.7 is familiar to me. Most of the Melliès survey looks at least approachable, and I'm least familiar with the specifics of the concrete models from chapter 8.

James Wood (Apr 11 2020 at 14:18):

I know a little bit about Chu spaces as well.

Amar Hadzihasanovic (Apr 11 2020 at 14:55):

If I understand correctly that you are looking for the “provability semantics” of linear logic, I think the most common answer would be a commutative quantale with a dualising element.

Amar Hadzihasanovic (Apr 11 2020 at 14:57):

This has the slightly annoying feature that both the tensor and the dualiser are structure on a poset, unlike the case of Heyting and Boolean algebras which are posets with properties.

Amar Hadzihasanovic (Apr 11 2020 at 14:59):

If you want “everything to be a property”, you would need to consider something like “posetal polycategories” with a number of properties (existence of “absolute” finite meets and joins, representability on both sides, existence of dualities). I don't know if this is written down anywhere.

Mike Shulman (Apr 11 2020 at 14:59):

A quantale is a non-elementary structure since it has all small meets and joins, unlike a Boolean or Heyting algebra. I think the better structure to talk about for classical linear logic is a star-autonomous poset.

Amar Hadzihasanovic (Apr 11 2020 at 15:01):

Oh, for some reason I remembered that quantales only had finite meets and joins. Thanks.

Robin Piedeleu (Apr 11 2020 at 15:04):

What then is the right provability semantics that also includes exponentials? A star-autonomous poset with a Galois connection to a Heyting algebra, mimicking the linear-nonlinear adjunction for the categorical semantics?

Amar Hadzihasanovic (Apr 11 2020 at 15:09):

Well, I think you can do it “more internally” because you have fewer choices. To model !, first you need a comonad. In a poset, that's just an interior operator.

Amar Hadzihasanovic (Apr 11 2020 at 15:11):

And for each element $x$, you have a comonoid on $!x$. That's just a tensor-idempotent.

Amar Hadzihasanovic (Apr 11 2020 at 15:13):

You have a sort-of canonical choice (which I think would correspond to the linear-non linear adjunction with the category of internal cocommutative comonoids) by taking $!x$ to be the greatest tensor-idempotent below $x$.

Mike Shulman (Apr 11 2020 at 15:14):

cf https://ncatlab.org/nlab/show/%21-modality

James Wood (Apr 11 2020 at 15:23):

So a *-autonomous poset is to a *-autonomous category as a Heyting algebra is to a CCC with sums? That seems satisfying. I just wanted to check that there weren't any unexpected problems with the definition. So how about Stone duality?

Valeria de Paiva (Apr 17 2020 at 19:00):

James Wood said:

As Boolean algebras are to classical logic and Heyting algebras are to intuitionistic logic, is there such a thing as “Girard algebras” for (fragments of) (classical or intuitionistic) linear logic? And is there a version of Stone duality for them?

yes, there are several versions of this. (none that I particularly like thugh) I think the most recent ones are by Mai Gherke (Relational semantics for full linear logic, with Dion Coumans and Lorijn van Rooijen. Journal of Applied Logic 12 (1) (2014), 50–66.) and Alessandra Palmigiano (e.g Sahlqvist correspondence via duality and its applications, A Palmigiano
23rd International Workshop on Logic, Language, Information, and Computation 2016)

Valeria de Paiva (Apr 17 2020 at 19:05):

Mike Shulman said:

A quantale is a non-elementary structure since it has all small meets and joins, unlike a Boolean or Heyting algebra. I think the better structure to talk about for classical linear logic is a star-autonomous poset.

beg to differ, Mike! lineales are about getting the posetal intuitionistic version of linear logic and the involution of the star-autonomous poset is best considered an after-thought, imho. but I would say that, of course.

Valeria de Paiva (Apr 17 2020 at 19:08):

Amar Hadzihasanovic said:

You have a sort-of canonical choice (which I think would correspond to the linear-non linear adjunction with the category of internal cocommutative comonoids) by taking $!x$ to be the greatest tensor-idempotent below $x$.

hmm clearly I'm in a minority here, but the greatest tensor-idempotent below $x$ is only the syntactic description of what's needed for a !-modality, it does not produce a mathematical modality.

Mike Shulman (Apr 17 2020 at 19:23):

Valeria de Paiva said:

beg to differ, Mike! lineales are about getting the posetal intuitionistic version of linear logic and the involution of the star-autonomous poset is best considered an after-thought, imho. but I would say that, of course.

Well of course there's a continuum. If you have only the judgmental structure with no connectives, then you have a poly-poset. If you have all the connectives, you have a *-autonomous poset. If you leave out the involution but have all the other connectives, you have a linearly distributive poset (I assume that's what a lineale is). Conversely, if you keep the involution but leave out all the other connectives, you have a *-poly-poset. And there are lots of other things in between. I don't see any reason to privilege the case of "all connectives except the involution", so I would say that either *-autonomous posets or poly-posets (the two extremes) are the most natural thing to tell newcomers about if they know about classical linear logic and are wondering about its posetal semantics.

Gershom (Apr 17 2020 at 19:37):

James Wood said:

So a *-autonomous poset is to a *-autonomous category as a Heyting algebra is to a CCC with sums? That seems satisfying. I just wanted to check that there weren't any unexpected problems with the definition. So how about Stone duality?

There are a lot of easy ways to generate and think about simple heyting algebras. Are there similar ways to get our hands on simple examples of *-autonomous posets? Do they have characterizations we can think of in terms of purely order-theoretic properties?

Valeria de Paiva (Apr 17 2020 at 20:59):

Mike Shulman said:

Valeria de Paiva said:

beg to differ, Mike! lineales are about getting the posetal intuitionistic version of linear logic and the involution of the star-autonomous poset is best considered an after-thought, imho. but I would say that, of course.

Well of course there's a continuum. If you have only the judgmental structure with no connectives, then you have a poly-poset. If you have all the connectives, you have a *-autonomous poset. If you leave out the involution but have all the other connectives, you have a linearly distributive poset (I assume that's what a lineale is). Conversely, if you keep the involution but leave out all the other connectives, you have a *-poly-poset. And there are lots of other things in between. I don't see any reason to privilege the case of "all connectives except the involution", so I would say that either *-autonomous posets or poly-posets (the two extremes) are the most natural thing to tell newcomers about if they know about classical linear logic and are wondering about its posetal semantics.

there's a continuum, but we're disagreeing on the important places to stop. a lineale is a monoidal closed poset (so it has tensor and implication), multiplicative disjunction which you can add (defined via implication or not) will give you the poly-structure. the important point is that from the logic/lambda-calculus perspective you can reasonably stay on the intuitionistic universe and have Curry-Howard working as it should. when you bite into the polycategory stuff/classical logic you lose the perfect correspondence and you need to start making trade-offs.

Amar Hadzihasanovic (Apr 17 2020 at 21:11):

hmm clearly I'm in a minority here, but the greatest tensor-idempotent below $x$ is only the syntactic description of what's needed for a !-modality, it does not produce a mathematical modality.

What would you say "produces a mathematical modality"?

(Btw, for ! I should have also said: "...and which is below the tensor unit", I guess)

sarahzrf (Apr 17 2020 at 23:25):

hmm, so a lineale is basically for intuitionistic linear logic?

sarahzrf (Apr 17 2020 at 23:25):

whereas *-autonomous is for classical linear logic?

sarahzrf (Apr 17 2020 at 23:26):

oh wait i guess ILL also has finite meets & joins

Mike Shulman (Apr 17 2020 at 23:31):

@Valeria de Paiva But the post I was replying to was about classical linear logic (quantales with a dualizing element), not intuitionistic linear logic. For ILL, a symmetric monoidal closed poset is definitely the natural "endpoint" on one side (the one on the left being a multi-poset).

Mike Shulman (Apr 17 2020 at 23:31):

Oh, and yes if you want the additive connectives too, then you want finite meets and joins, in all cases.

sarahzrf (Apr 17 2020 at 23:32):

i should probably study ILL some more, my perception of it is still vaguely "but dont you lose most of the stuff that makes linear logic cool"

Valeria de Paiva (Apr 18 2020 at 00:46):

sarahzrf said:

hmm, so a lineale is basically for intuitionistic linear logic?

@sarahzrf|276072 lineales have meets and joints, if you want them to.
and @Mike given a model of ILL you can always get a model of CLL by taking the double negated elements, as usual. do you can add that to you continuum, even more to the right.

@Amar Hadzihasanovic in Dialectica categories you have a mathematical modality which comes about from taking free monoids in the underlying category, in coherence spaces you have two versions of ! modality, one of them using multisets. these mathematical constructions exist independently from their use to model Linear Logic.
In my paper with Andrea Schalk, http://www.cs.man.ac.uk/~schalk/publ/pvsets.pdf we also resort to using the syntactic construction (which you still need to prove is non-empty) but it's always less satisfying than finding models in "the wild of mathematics".

sarahzrf (Apr 18 2020 at 00:51):

anyway my impression was that classical linear logic largely had pretty good computational behavior?

Valeria de Paiva (Apr 18 2020 at 01:00):

sarahzrf said:

anyway my impression was that classical linear logic largely had pretty good computational behavior?

well, it really depends on what you call "good computational behavior", doesn't it?

Valeria de Paiva (Apr 18 2020 at 01:16):

Gershom said:

There are a lot of easy ways to generate and think about simple heyting algebras.
````
which easy ways are you thinking of, please?

sarahzrf (Apr 18 2020 at 01:19):

any bounded toset is [classically] a heyting algebra, right?

sarahzrf (Apr 18 2020 at 01:20):

the collection of monotone functions from any proset into a complete heyting algebra forms a complete heyting algebra

sarahzrf (Apr 18 2020 at 01:21):

the opens of a topological space form a complete heyting algebra

sarahzrf (Apr 18 2020 at 01:21):

any boolean algebra is a heyting algebra

sarahzrf (Apr 18 2020 at 01:22):

as a special case of the "monotone functions" one, you can pick the codomain to be the set of truth values, so that the functions correspond to upward-closed sets of the domain, and this gets a heyting algebra out of any proset (equivalent to kripke semantics)

Valeria de Paiva (Apr 18 2020 at 01:27):

yes, any boolean algebra is a heyting algebra, but you do want to deal with heyting algebras that are not boolean, if you want to discuss the truly intuitionistic features of your system. similarly, any heyting algebra is a degenerate lineale, one where the tensor is a meet and par is a join, but you don't want to dwell on the degenerate cases, I think.

sarahzrf (Apr 18 2020 at 01:28):

alright, so leave that one out :)

sarahzrf (Apr 18 2020 at 01:29):

well, actually it can be useful

sarahzrf (Apr 18 2020 at 01:29):

if you have a complete boolean algebra, you can get a complete heyting algebra that isnt necessarily boolean by taking the monotone functions into it from some other proset

sarahzrf (Apr 18 2020 at 01:29):

that's exactly what you're doing in kripke semantics, if your metatheory is classical

Gershom (Apr 18 2020 at 01:46):

Valeria de Paiva said:

which easy ways are you thinking of, please?

Well in the (not so special?) case of complete Heyting Algebras you have the nice purely order-theoretic characterization which is somewhat local of it just being a complete lattice with finite meets distributing over arbitrary joins. And since we have lots of order-theoretic results on distributive lattices going back to Birkhoff, those are easy to generate and get your hands on (and as noted above come with a nice Stone-representation story, etc). Some of the niceness (and locality) there being reflected in the fact that we have "forbidden sublattice" characterizations, etc.

Meanwhile *-autonomous stuff (which I don't understand well, hence my question), like boolean lattice stuff, feels like it has a "global character" to its definition, in that the dualizing operation relates elements that can be fairly distant in the poset structure. But nonetheless, I'm wondering how much of a nice characterization of *-autonomous poset stuff we can give in terms of that same classic order-theoretic technology. Perhaps there's something like the "complete" condition for Heyting Algebras that carves out a large subclass where such techniques are more tractable?

One route there might be the "depleted" posetal version of the chu construction, I suppose?

sarahzrf (Apr 18 2020 at 01:48):

oh have you not seen mike's paper about that exact thing?

Gershom (Apr 18 2020 at 01:54):

I assume you mean "linear logic for constructive mathematics"? I'm aware of it. If my question is answered there, its buried in all the other nice stuff such that I didn't recognize it.

sarahzrf (Apr 18 2020 at 02:10):

well, it does do a posetal chu construction

sarahzrf (Apr 18 2020 at 02:11):

gets models of affine logic by taking pairs (P⁺, P⁻) from a Heyting algebra, such that P⁺ ∧ P⁻ ⊢ ⊥

Valeria de Paiva (Apr 18 2020 at 06:04):

sarahzrf said:

if you have a complete boolean algebra, you can get a complete heyting algebra that isnt necessarily boolean by taking the monotone functions into it from some other proset

this is not a case that you can learn much from, I fear.
Kripke semantics is an useful semantics, but its usefulness is limited, if your goal is category theory

sarahzrf (Apr 18 2020 at 06:10):

i mean, taking the monotone functions into 2 is the same thing, in a classical metatheory, to taking the monotone functions into truth values

sarahzrf (Apr 18 2020 at 06:11):

and that is taking (0, 1)-copresheaves :-)

sarahzrf (Apr 18 2020 at 06:13):

perhaps you wouldve liked it better if i'd said something like... "if you have a boolean grothendieck topos, you can get a grothendieck topos that isn't necessarily boolean by taking the category of functors into it from some other category"—well, i'm not sure whether that's true, tho i wouldnt be surprised, but it's for sure true if the boolean grothendieck topos in question is a classical metatheory's Set

Valeria de Paiva (Apr 18 2020 at 06:20):

Gershom said:

I assume you mean "linear logic for constructive mathematics"? I'm aware of it. If my question is answered there, its buried in all the other nice stuff such that I didn't recognize it.

I'm just thinking that there isn't an awful lot of information on Heyting algebras around, actually. it would be nice to know more about them. My friend Jean Pretorius wrote a phd thesis in Cambridge about them in the 90's. I looked around to see new stuff, but didn't find much.

and no, I don't thin the involution of *-autonomous posets is that interesting. It has been investigated by lots of people since the early 90's and as far as I know has not produced any goods. but maybe this is just my biased view.

sarahzrf (Apr 18 2020 at 06:22):

well, i don't have that much knowledge of *-autonomous stuff, so maybe that's part of it

sarahzrf (Apr 18 2020 at 06:23):

mostly i'm coming at it from a syntactic point of view, some game semantics, & actually yes *-autonomous stuff but mostly just in the specific and pretty concrete form ive seen in "linear logic for constructive mathematics"

sarahzrf (Apr 18 2020 at 06:25):

but to me, a ton of what ive found interesting about the linear logic stuff ive learned has been related to ⅋ and ┴

sarahzrf (Apr 18 2020 at 06:26):

or more abstractly and handwavily, dualities, i guess

Valeria de Paiva (Apr 18 2020 at 06:26):

sarahzrf said:

and that is taking (0, 1)-copresheaves :-)

no, it isn't. and no, I wouldn't like " it better if i'd said something like... "if you have a boolean grothendieck topos, you can get a grothendieck topos that isn't necessarily boolean by taking the category of functors into it from some other category".
Dialectica categories do not give you toposes, Grothendick or otherwise. I would like to get a topos construction, if this was truly what the construction produced. if it is, I have problems seeing it..

topos theory models more that we see here.

sarahzrf (Apr 18 2020 at 06:28):

what do you mean by "no, it isn't"? the poset of truth values generally plays the same role among (0, 1)-categories that Set does among (1, 1)-categories, so you should get "(0, 1)-copresheaves" by taking the internal hom into it

sarahzrf (Apr 18 2020 at 06:28):

do you have a specific objection?

Valeria de Paiva (Apr 18 2020 at 06:38):

sarahzrf said:

do you have a specific objection?

yes, I do have a specific objection. when I construct dialectica categories I'm not pretending to build presheaves or sheaves at all. topos theory requires much more structure than I can build up.

sarahzrf (Apr 18 2020 at 06:39):

i wasn't talking about dialectica categories, though...

sarahzrf (Apr 18 2020 at 06:45):

never mind, sorry—i'm about to go to sleep anyway

sarahzrf (Apr 18 2020 at 06:45):

good night

Gershom (Apr 18 2020 at 06:50):

Valeria de Paiva said:

I'm just thinking that there isn't an awful lot of information on Heyting algebras around, actually. it would be nice to know more about them. My friend Jean Pretorius wrote a phd thesis in Cambridge about them in the 90's. I looked around to see new stuff, but didn't find much.

Well in the finite case it's exactly the theory of finite distributive lattices (right?), which is very rich. I agree that there's a lot more going on in the general case, but there's certainly a lot of "hands on" stuff to get a handle on with small examples. Maybe I should just start playing around with some small finite *-autonomous posets and see where it goes... I was just hoping someone had gone there first :-)

Amar Hadzihasanovic (Apr 18 2020 at 10:14):

Valeria de Paiva said:

@Amar Hadzihasanovic in Dialectica categories you have a mathematical modality which comes about from taking free monoids in the underlying category, in coherence spaces you have two versions of ! modality, one of them using multisets. these mathematical constructions exist independently from their use to model Linear Logic.
In my paper with Andrea Schalk, http://www.cs.man.ac.uk/~schalk/publ/pvsets.pdf we also resort to using the syntactic construction (which you still need to prove is non-empty) but it's always less satisfying than finding models in "the wild of mathematics".

Oh, I absolutely agree. But I would say that the same is true of “Heyting algebras in general” as opposed to, say, particular CCCs that are found in the wild. I think the topic was specifically about what (algebraic or order-theoretic) structures or properties are needed to give a provability semantics of linear logic, which is what you would call “syntactic constructions”.

Amar Hadzihasanovic (Apr 18 2020 at 10:18):

Of course the case of the exponentials is special because they are not uniquely fixed by their logical behaviour, not even up to logical equivalence, but I think that if there is one exponential that 'feels more canonical' than others, it is the (Lafont?) one arising from a left adjoint to the forgetful functor from the cartesian category of commutative comonoids inside a SMC. Which in the poset case would be the “greatest tensor-idempotent” one.

James Wood (Apr 18 2020 at 12:31):

Amar Hadzihasanovic said:

[exponentials] are not uniquely fixed by their logical behaviour, not even up to logical equivalence

Can you expand on this a bit? It seems like an interesting property, which would maybe explain why the exponentials have typically been harder to pin down.

Amar Hadzihasanovic (Apr 18 2020 at 13:26):

Well, you can take any sequent calculus or natural deduction calculus with implication $\rightarrow$, and try “duplicating” some connectives together with their rules. Same rules, different symbol only. Say they're n-ary, call the two “copies” of the connective $c$ and $c'$. Then you ask: is it always provable, for all formulas $A_1, ..., A_n$ that $c(A_1, \ldots, A_n) \rightarrow c'(A_1, \ldots, A_n)$ and $c'(A_1, \ldots, A_n) \rightarrow c(A_1, \ldots, A_n)$.

(Maybe there are meaningful version of the problem without implication)

Amar Hadzihasanovic (Apr 18 2020 at 13:27):

At least in the standard calculi for linear logic, this is true (wrt linear implication) for all the multiplicatives and the additives. So two copies of the same connectives are “internally interchangeable”.

Amar Hadzihasanovic (Apr 18 2020 at 13:29):

But it is not true for the exponentials. In fact you can have several copies of ! and ?, with the same rules, and consistently extend the calculus with rules that make it provable that they are inequivalent.

Amar Hadzihasanovic (Apr 18 2020 at 13:31):

I think this is the classical reference for such a system (unfortunately under a Springer paywall...)

Amar Hadzihasanovic (Apr 18 2020 at 13:35):

In terms of categorical models, this is reflected by the fact that the logical rules for, say, $!$ are modelled by any monoidal comonad such that for all objects $A$, $!A$ has the structure of a commutative comonoid (wrt tensor), and there can be many of those on the same monoidal category.

James Wood (Apr 18 2020 at 13:47):

For the additives, I guess this property is obvious because they satisfy a universal property. For tensor, is it again because of a universal property... how it represents multi-/polycategory morphisms? But for exponentials, there is no such thing.

Amar Hadzihasanovic (Apr 18 2020 at 13:48):

(I guess without implication you need to differentiate between (two-sided) sequent calculi and natural deduction. In the first case you ask if you can always derive $c(A_1, \ldots, A_n) \vdash c'(A_1, \ldots, A_n)$ and the other way around. In the second case you ask whether you can always derive $c'(A_1, \ldots, A_n)$ from $c(A_1, \ldots, A_n)$ and the other way around.)

James Wood (Apr 18 2020 at 13:49):

(Though in the system I've been working on, a graded ! is supposed to be used in representing “weighted multicategory” morphisms, so this question would be interesting to investigate there.)

Amar Hadzihasanovic (Apr 18 2020 at 13:53):

James Wood said:

For the additives, I guess this property is obvious because they satisfy a universal property. For tensor, is it again because of a universal property... how it represents multi-/polycategory morphisms? But for exponentials, there is no such thing.

To be fair, from the “model” side I think it's quite subtle, and it all depends on what we consider to be the “bare-bones” model of a logic.

Amar Hadzihasanovic (Apr 18 2020 at 13:53):

It's related to what @Mike Shulman and @Valeria de Paiva were discussing about on the “continuum” of models.

Amar Hadzihasanovic (Apr 18 2020 at 13:56):

If the bare-bones model structures are categories, there can be only one interpretation of the additives, and you can ask “is this category a model of the additive fragment of LL”, but there can be different SMC structures, so it does not make sense to ask “is this a model of the multiplicative fragment”.

Amar Hadzihasanovic (Apr 18 2020 at 13:57):

But if the bare-bones model is multi or polycategories, then it does make sense.

James Wood (Apr 18 2020 at 14:00):

If we're just talking about a syntactic property, doesn't the fact that I can find a model factored in the way I needed it to be (e.g, representable multi-/polycategories) suffice?

Amar Hadzihasanovic (Apr 18 2020 at 14:00):

If your bare-bones model is a symmetric monoidal category, agreed, there can be many exponentials.

But say your bare-bones model, for whatever reason, is a monoidal functor from a cartesian category to an SMC. Then it makes sense to ask “does this have a left adjoint?”, and in that case say that your model has the property of being a model of multiplicative-exponential linear logic.

Amar Hadzihasanovic (Apr 18 2020 at 14:03):

(Btw if you designed your sequent calculus or whatever in such a way that its “natural” model is such a functor, then I believe you would have a unique, logically fixed exponential.)

James Wood (Apr 18 2020 at 14:07):

Aah, that makes sense. And something like that may indeed be the case in what I'm working on. At least, I'm pretty sure that ! is unique, and I get syntactically why it's not unique in standard linear logic now.

Amar Hadzihasanovic (Apr 18 2020 at 14:07):

Something like a dual-context sequent calculus with the interpretation that one part of the context is to be read “through a functor”. I hadn't thought of the connection with “uniqueness of exponentials” before but I'm sure this has been done, probably Mike or Valeria would know.

Amar Hadzihasanovic (Apr 18 2020 at 14:10):

In fact I vaguely remember having convinced myself a few years ago that dual context was a better way of doing the LL sequent calculus precisely for this reason.

sarahzrf (Apr 18 2020 at 14:11):

man i should try to finish the logic of unity paper sometime

James Wood (Apr 18 2020 at 14:11):

I forget: how well does dual context stuff handle classical linear logic?

Mike Shulman (Apr 18 2020 at 14:14):

Yes, in general multiple-context versions of modal logics are the best way to give modal operators a universal property (and thereby make them unique). I think we understand the "intuitionistic" version of this pretty well both syntactically and semantically in general, e.g. my paper with Dan and Mitchell. But the "classical" version, with multiple types on both sides of the turnstile, is not as well understood semantically, although I've done some playing around with it.

Amar Hadzihasanovic (Apr 18 2020 at 14:16):

Do you remember what the main challenges were?

James Wood (Apr 18 2020 at 14:16):

Right, I guess I can make the claim, then, that this is a good motivation for studying intuitionistic linear logic.

Amar Hadzihasanovic (Apr 18 2020 at 14:17):

sarahzrf said:

man i should try to finish the logic of unity paper sometime

Is that the dual of Girard's “unity of logic” paper? :)

sarahzrf (Apr 18 2020 at 14:43):

oops!

Mike Shulman (Apr 18 2020 at 15:57):

@Amar Hadzihasanovic I don't know that there were particular challenges; it's just that no one has sat down and worked it out yet. But one thing that's potentially tricky is the interaction between ? and ! along with duality.

Valeria de Paiva (Apr 18 2020 at 17:22):

sarahzrf said:

what do you mean by "no, it isn't"? the poset of truth values generally plays the same role among (0, 1)-categories that Set does among (1, 1)-categories, so you should get "(0, 1)-copresheaves" by taking the internal hom into it

oh sorry for the talking across purposes here. I wasn't referring to the fact that " taking the monotone functions into 2 is the same thing, in a classical metatheory, to taking the monotone functions into truth values". I sure agree with this.

when I said "no, it isn't" I meant that the construction you proposed (taking the monotone functions into 2) is not the same as
"taking (0, 1)-copresheaves" because the first is something that you can talk to highschool students about, while for the second you need all the background of category theory that comes from sheaves and notions of 2 and higher order categories. I was reacting to the suggestion that I wanted to complicate things more than they need to be complicated, as exemplified in the next sentence. so my objection was that I don't want to bring heavy machinery if I don't need it for the modeling task at hand. But I think the misunderstanding boils down to me not being familiar with the medium, really. I needed to be more careful with a sentence like "no, it isn't".

and sure "11:39 PM i wasn't talking about dialectica categories, though...", sorry, I was!

Valeria de Paiva (Apr 18 2020 at 17:33):

Amar Hadzihasanovic said:

I think this is the classical reference for such a system (unfortunately under a Springer paywall...)

Jean-Baptiste has the free version here http://www-philo.univ-paris1.fr/Joinet/NEW/PDF/PublicationsVersionOK/1-ok-structexp.pdf
but
"!A has the structure of a commutative comonoid (wrt tensor)" is not enough (the comonoid structure has to interact well with the coalgebra structure induced by the monoidal comonad), as discussed in
Relating Categorical Semantics for Intuitionistic Linear Logic with P. Maneggia, V. de Paiva and E. Ritter
in Applied Categorical Structures, volume 13(1):1--36, 2005 https://www.math.unipd.it/~maietti/pubb.html

but sure there are many ways of defining exponentials.

Valeria de Paiva (Apr 18 2020 at 17:36):

Amar Hadzihasanovic said:

If the bare-bones model structures are categories, there can be only one interpretation of the additives, and you can ask “is this category a model of the additive fragment of LL”, but there can be different SMC structures, so it does not make sense to ask “is this a model of the multiplicative fragment”.

Yes!!
Amar Hadzihasanovic said:

To be fair, from the “model” side I think it's quite subtle, and it all depends on what we consider to be the “bare-bones” model of a logic.

totally agreeing!!!

Valeria de Paiva (Apr 18 2020 at 17:39):

Amar Hadzihasanovic said:

In fact I vaguely remember having convinced myself a few years ago that dual context was a better way of doing the LL sequent calculus precisely for this reason.

hmm, I had reached the same conclusion for a totally different reason: because I wanted to re-use the libraries already written for simply typed calculus, on the intuitionistic side of the model.

Amar Hadzihasanovic (Apr 18 2020 at 18:08):

"!A has the structure of a commutative comonoid (wrt tensor)" is not enough (the comonoid structure has to interact well with the coalgebra structure induced by the monoidal comonad), as discussed in

Thanks for the reference! :) I didn't remember the details.

Valeria de Paiva (Apr 18 2020 at 19:40):

Amar Hadzihasanovic said:

"!A has the structure of a commutative comonoid (wrt tensor)" is not enough (the comonoid structure has to interact well with the coalgebra structure induced by the monoidal comonad), as discussed in

Thanks for the reference! :) I didn't remember the details.

Thanks for the conversation! I feel a bit obsessive about those particular details, which are not important for most people. because they have an impact on the previous conversation on the continuum of models.

sarahzrf (Apr 19 2020 at 00:58):

Valeria de Paiva said:

sarahzrf said:

what do you mean by "no, it isn't"? the poset of truth values generally plays the same role among (0, 1)-categories that Set does among (1, 1)-categories, so you should get "(0, 1)-copresheaves" by taking the internal hom into it

oh sorry for the talking across purposes here. I wasn't referring to the fact that " taking the monotone functions into 2 is the same thing, in a classical metatheory, to taking the monotone functions into truth values". I sure agree with this.

when I said "no, it isn't" I meant that the construction you proposed (taking the monotone functions into 2) is not the same as
"taking (0, 1)-copresheaves" because the first is something that you can talk to highschool students about, while for the second you need all the background of category theory that comes from sheaves and notions of 2 and higher order categories. I was reacting to the suggestion that I wanted to complicate things more than they need to be complicated, as exemplified in the next sentence. so my objection was that I don't want to bring heavy machinery if I don't need it for the modeling task at hand. But I think the misunderstanding boils down to me not being familiar with the medium, really. I needed to be more careful with a sentence like "no, it isn't".

and sure "11:39 PM i wasn't talking about dialectica categories, though...", sorry, I was!

oh—the point i was trying to make was that homming into a complete boolean algebra in order to get a heyting algebra, and/or doing kripke semantics, actually is ubiquitous, because one of its cases is the (0, 1)-truncated version of taking copresheaves, and that's a pretty fundamental construction

sarahzrf (Apr 19 2020 at 00:59):

for example, it's the free completion of a preordered set to an inflattice

Valeria de Paiva (Apr 20 2020 at 21:26):

sarahzrf said:

oh—the point i was trying to make was that homming into a complete boolean algebra in order to get a heyting algebra, and/or doing kripke semantics, actually is ubiquitous, because one of its cases is the (0, 1)-truncated version of taking copresheaves, and that's a pretty fundamental construction

not disagreeing that "homming into a(n) algebra" is a pretty fundamental construction, it is. still disagreeing that it is ubiquitous and still disagreeing that thinking of it as the "(0, 1)-truncated version of taking copresheaves" is helpful. but sure, different people different notions of what's helpful, of what's easy or not.

But I came back to this thread because of
Amar Hadzihasanovic said:

Something like a dual-context sequent calculus with the interpretation that one part of the context is to be read “through a functor”. I hadn't thought of the connection with “uniqueness of exponentials” before but I'm sure this has been done, probably Mike or Valeria would know.

I don't think I know any of this. But I was thinking and it seems to me that you don't get uniqueness of exponentials this way. maybe I am wrong, but I think you get one amonoidal comonad that can be "resolved" into a infinity of adjoint pairs, the full spectrum from Eilenberg-Moore coalgebras to co-Klesili categories, passing through products of exponentiable objects, etc. with several possible levels of "strictification" of morphisms. So Milly Maeitti (my co-author) wanted very strict morphisms of models of LL(mirroring the type theory), while Andrea Schalk and Martin Hyland wanted morphisms that are better for category theory, less so for the syntax. Either way, I don't think you get uniqueness of exponentials, but it has been a long time since I thought about this.

Valeria de Paiva (Apr 20 2020 at 21:33):

Gershom said:

Valeria de Paiva said:

I'm just thinking that there isn't an awful lot of information on Heyting algebras around, actually. it would be nice to know more about them. My friend Jean Pretorius wrote a phd thesis in Cambridge about them in the 90's. I looked around to see new stuff, but didn't find much.

Well in the finite case it's exactly the theory of finite distributive lattices (right?), which is very rich. I agree that there's a lot more going on in the general case, but there's certainly a lot of "hands on" stuff to get a handle on with small examples. Maybe I should just start playing around with some small finite *-autonomous posets and see where it goes... I was just hoping someone had gone there first :-)

Sure, playing around with small finite *-autonomous posets is a good idea. Vaughan Pratt had some student of his program a Chu calculator for that http://chu.stanford.edu/live/ I think it's still working. but I confess that it hasn't helped me very much.

Amar Hadzihasanovic (Apr 21 2020 at 14:19):

@Valeria de Paiva I am thinking of the following setting: you have a dual-context intuitionistic sequent calculus, with sequents of the form $A_1, \ldots, A_n ; B_1, \ldots, B_m \vdash C$, and the “bare-bones” semantics are monoidal functors (or morphisms of multicategories) $F: \mathcal{C} \to \mathcal{D}$, so that the $A_i$ are interpreted in $\mathcal{C}$, the $B_j$ and $C$ in $\mathcal{D}$, and the sequent is interpreted as a morphism $\bigotimes F(\llbracket A_i \rrbracket) \otimes \bigotimes \llbracket B_j \rrbracket \to \llbracket C \rrbracket$ in $\mathcal{D}$.

Amar Hadzihasanovic (Apr 21 2020 at 14:23):

Then you can interpret a modality $\square$ with left rule $\Gamma ; A, \Delta \vdash B$ leads to $\square A, \Gamma ; \Delta \vdash B$ and right rule $\Gamma ; \vdash A$ leads to $\Gamma ; \vdash \square A$ if and only if $F$ has a left adjoint. Also the rules specify the modality up to logical equivalence.

Amar Hadzihasanovic (Apr 21 2020 at 14:25):

In brief the specific splitting of the comonad as an adjunction is given as part of the “bare-bones” semantics, and that's what makes it unique...

Amar Hadzihasanovic (Apr 21 2020 at 14:29):

(There's a little of imprecision in what I wrote in that the interpretation of $\square A$ changes depending on where it is in the context, but it's not hard to fix)

Valeria de Paiva (Apr 21 2020 at 14:40):

Amar Hadzihasanovic said:

Valeria de Paiva I am thinking of the following setting: you have a dual-context intuitionistic sequent calculus, with sequents of the form $A_1, \ldots, A_n ; B_1, \ldots, B_m \vdash C$, and the “bare-bones” semantics are monoidal functors (or morphisms of multicategories) $F: \mathcal{C} \to \mathcal{D}$, so that the $A_i$ are interpreted in $\mathcal{C}$, the $B_j$ and $C$ in $\mathcal{D}$, and the sequent is interpreted as a morphism $\bigotimes F(\llbracket A_i \rrbracket) \otimes \bigotimes \llbracket B_j \rrbracket \to \llbracket C \rrbracket$ in $\mathcal{D}$.

yes, we've done this in ICALP1998. Explicit Substitutions for Constructive Necessity (with Neil Ghani and Eike Ritter), presented at 25th International Colloquium on Automata, Languages and Programming (ICALP'98). Lecture Notes in Computer Science LNCS 1443, eds. Larsen, Skyum and Winskel.

more recently Eike Ritter and I did a fibrational version of this dual-context modal logic Valeria de Paiva, Eike Ritter. Fibrational Modal Type Theory. Electronic Notes in Theoretical Computer Science, 01 June 2016. Proceedings of the Tenth Workshop on Logical and Semantic Frameworks with Applications (LSFA 2015). [PDF]