## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorMike Shulman
• CommentTimeJun 8th 2017
• (edited Jun 8th 2017)

The cut rule for linear logic used to be stated as

If $\Gamma \vdash A$ and $A \vdash \Delta$, then $\Gamma \vdash \Delta$.

I don’t think this is general enough, so I corrected it to

If $\Gamma \vdash A, \Phi$ and $\Psi,A \vdash \Delta$, then $\Psi,\Gamma \vdash \Delta,\Phi$.

• CommentRowNumber2.
• CommentAuthorTodd_Trimble
• CommentTimeJun 8th 2017

No objection, but I guess it would depend on the precise rules. In MLL which has duals, if we have rules which allow us to derive

$\frac{\Gamma \vdash \Sigma,\Phi}{\Gamma, \Phi^\ast \vdash \Sigma}, \qquad \frac{\Psi, \Sigma \vdash \Delta}{\Psi \vdash \Delta, \Sigma^\ast}$

where $\Phi^\ast$ is the list of duals of formulas of $\Phi$, and $A^{\ast\ast} = A$, I thought we would be able to derive your more general cut rule from the more specific cut rule:

$\array{ \arrayopts{\rowlines{solid}} \Gamma \vdash A, \Phi\;\;\;\;\;\;\;\;\; \Psi, A \vdash \Delta \\ \Gamma, \Phi^\ast \vdash A \;\;\;\;\;\;\;\;\; A \vdash \Psi^\ast, \Delta \\ \Gamma, \Phi^\ast \vdash \Psi^\ast, \Delta \\ \Psi, \Gamma \vdash \Delta, \Phi }$
• CommentRowNumber3.
• CommentAuthorMike Shulman
• CommentTimeJun 8th 2017

Yes, you’re right. But I think it’s better to formulate the rule in a way that remains correct in fragments without involutive negation.

• CommentRowNumber4.
• CommentAuthorTodd_Trimble
• CommentTimeJun 8th 2017

Understood (and agreed); I was just explaining the likely reason the original form was the way it was (I’m guessing I wrote that).

• CommentRowNumber5.
• CommentAuthorTobyBartels
• CommentTimeSep 10th 2018

Confirm that the game semantics presented here is the same as Blass's. (I still haven't actually read Blass 1992, yet, but I read a 1994 paper by Blass that summarizes the 1992 semantics.)

• CommentRowNumber6.
• CommentTimeMar 24th 2019

Added differential linear logic to variants, included a reference to the paper introducing differential categories.

1. Link to game semantics article

Ammar Husain

2. Copycat example.

Ammar Husain

3. Caires, Pfenning

Ammar Husain

• CommentRowNumber10.
• CommentAuthorMike Shulman
• CommentTimeNov 12th 2019

• CommentRowNumber11.
• CommentTimeFeb 16th 2020

• CommentRowNumber12.
• CommentAuthorTobyBartels
• CommentTimeFeb 17th 2020

Mention Mike's antithesis interpretation.

• CommentRowNumber13.
• CommentAuthorMike Shulman
• CommentTimeMar 12th 2020

Thanks for adding that, Toby! I added a redirect for “antithesis interpretation” to this page, since you created a link to that from join. We could eventually have a separate page about it, but for now this is the best target of such a link.

4. I think the use of ’categorial semantics’, when the section talks about a ’categorical semantics’ was a typo. If it isn’t, it might be good to explain that there are schools of thought that prefer the adjective ’categorial’ to ’categorical’, and strongly so. Personally, I prefer ’categorical’, but some of my best friends insist on ’categorial’.

Valeria de Paiva

• CommentRowNumber15.
• CommentAuthorUrs
• CommentTimeJan 19th 2021
• (edited Jan 19th 2021)

I do expect it was a typo. But it might still be good to explain issues with the terminology, either on this page or on a dedicated page!

I feel that most usage of “categorical” in mathematics is, or originates in, a careless search for terminology that is really looking for “category theoretic”. Compare the analogous clear difference between “numerical” and “number theoretic”.

• CommentRowNumber16.
• CommentAuthorTodd_Trimble
• CommentTimeJan 25th 2021

It almost surely is not a typo – it’s Toby’s preferred word.

• CommentRowNumber17.
• CommentAuthorDmitri Pavlov
• CommentTimeJan 26th 2021
• (edited Jan 26th 2021)

Searching MathSciNet, “categorical” is more popular than “categorial” by an order of 20 (11822 vs 591 matches).

Furthermore, “categorial” matches mostly philosophy, logic, and computer science, with almost no actual category theory papers.

• CommentRowNumber18.
• CommentAuthorUrs
• CommentTimeJan 26th 2021
• (edited Jan 26th 2021)

Somebody please just add a discussion of terminology, conventions and issues to this entry – or better to categorical logic and then link to it from here.

It sure must look like typos to any outside reader: There was 16 “categorical” vs 4 “categorial” before Valeria’s latest edit, some next to each other, notably there was

1. Categorial semantics. We discuss the categorical semantics…

I see from the edit history that the “categorial”s are Toby’s intentional ideosyncrasy. As per #15 I probably agree with the logic behind this, but if mathematical terminology were a matter of logic, most of it would be much different. The goal of an entry must be to communicate with the reader, not to irritate them.

But if we had a decent section “On terminology” at categorical logic we could link to this from the very top of all relevant pages – say: “On the terminology of ’categori(c)al’ in the following see at categorical logic. ” – and then the issue would be dealt with.

• CommentRowNumber19.
• CommentAuthorUrs
• CommentTimeJan 27th 2021

So I went ahead and wrote a comment on terminology myself: here (in a new section of the entry categorical semantics).

Maybe best to have any further discussion of this point there, in the thread for the entry on categorical semantics.

• CommentRowNumber20.
• CommentAuthorDmitri Pavlov
• CommentTimeJan 27th 2021
• (edited Jan 27th 2021)

Re #15: dictionaries list two different meanings for “categorical”, for example, Wiktionary says

1. Absolute; having no exception.

2. Of, pertaining to, or using a category or categories.

Clearly, the second meaning makes “categorical” perfectly appropriate here. I do not understand how or why the interpretation that “categorical” necessarily refers to 1 above, whereas “categorial” means 2, came to be.

• CommentRowNumber21.
• CommentAuthorTodd_Trimble
• CommentTimeJan 28th 2021

Re #20: I don’t think it’s that. I think Toby wants “categorial” to avoid a conflict with the model theorists’ usage of the word “categorical”. My own opinion is that we don’t need such deferment.

Anonymous

6. Noted that the reason the symbols matched the positive/negative grouping is because that’s how they were chosen

Anonymous

• CommentRowNumber24.
• CommentAuthorDavid_Corfield
• CommentTimeAug 21st 2022

• Paul-André Melliès, A Functorial Excursion Between Algebraic Geometry and Linear Logic, in 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (LICS ’22), August 2–5, 2022, Haifa, Israel. ACM, New York, (doi:10.1145/3531130.3532488, pdf)
• CommentRowNumber25.
• CommentAuthorDavid_Corfield
• CommentTimeAug 21st 2022

So what’s going on in that reference in #24?

Our main technical contribution in this work is to resolve an old open question in the field of mathematical logic, which is to construct a model of linear logic — including the exponential modality — in the functorial language of Algebraic Geometry. By performing this construction in the present paper, we hope to integrate linear logic as a basic and very natural component in the current process of geometrization of type theory. The guiding idea here is that linear logic should be seen as the logic of generalised vector bundles, in the same way as Martin-Löf type theory with identity is seen today as the logic of spaces up to homotopy, formulated in the language of ∞-topos theory.

The idea of relating linear types and vector bundles already appears in the early work by Schreiber [Schreiber 2014] on quantization of pre-quantum field theory. The approach to linear homotopy types and stable ∞-categories of bundles developed there is quite different in style and spirit however, and it will be thus instructive to clarify the connection with the constructions of the present paper.

(This second paragraph in the printed version, rather than the preprint.)

Hmm,

Our main purpose in the paper is to associate to every scheme $X$ a specific model of intuitionistic linear logic, where formulas are interpreted as generalised vector bundles, and where proofs are interpreted as suitable vector fields.

• CommentRowNumber26.
• CommentAuthorUrs
• CommentTimeAug 21st 2022

Thanks for the pointer. I don’t have much time to spare, lagging behind with preparing slides for upcoming talks (broadly on this topic, though), but I’ll try to take a look.

• CommentRowNumber27.
• CommentAuthorUrs
• CommentTimeAug 21st 2022

Have had a glance over the article in #24.

My impression is that at least the broad conceptual nature of the “linear/non-linear adjunction” there – i.e. (31) in the preprint, (30) in the published version (p. 10), realized in terms of coalgebras – coincides with that discussed in Sec. 4.2 of “Quantization via Linear Homotopy Types” (i.e. p. 47-48, esp. the canonical Exp. 4.1 given by forming suspension spectra), observing that suspension spectra canonically inherit comonoid structure (here: coring spectrum-structure) from the fact that forming suspension spectra is strong monoidal.

In fact, as recalled on that p. 47, there is a canonical linear/non-linear adjunction induced as soon as the linear type system in question is the global value of a dependent linear type system, and that then goes through comonoids in this sense as soon as the functor forming the dependent sum of the tensor unit ($X \mapsto \underset{X}{\sum} \mathbf{1}_X$) is strong monoidal.

Since the linear types in #24 do form a dependent system (not sure if this is made fully explicit there, at least in the final dictionary the adjective “dependent” seems to be missing on the left of the second row – and the word “bundle” might usefully complete the first row on the right), this canonical linear/non-linear adjunction should exist in that context, too, and probably coincides with the one that is given, up to unwinding of notation (I wonder if there is room to connect more to standard notation: after all, the yoga of six operations that provides models of dependent linear type theory originates in the example of quasi-coherent modules over schemes).

• CommentRowNumber28.
• CommentAuthorDavid_Corfield
• CommentTimeAug 21st 2022

Interesting! Especially for me since my own small contribution to your paper (as you note in footnote 13) concerns Exp. 4.1, suggested in a comment here. I’ll see if I can make any further sense later.

• CommentRowNumber29.
• CommentAuthorUrs
• CommentTimeAug 21st 2022
• (edited Aug 23rd 2022)

Thanks for digging out this old thread.

It’s good to come back to this topic after a long detour, now with a better idea of what the interesting base spaces are over which to parameterize linear types in view of quantum systems. The neeext step (at CQTS) will to actually program and then “run” (simulate) topological quantum gates as described here. Let’s see how that will work out…

• CommentRowNumber30.
• CommentAuthorDavid_Corfield
• CommentTimeAug 26th 2022

Another thread to dig out is this one unstable K(n)-homotopy theory.

Thoughts on $\Sigma^\infty \Omega^\infty$ as the comonad associated to the co-operad of co-commutative co-algebras.

• CommentRowNumber31.
• CommentAuthorDavid_Corfield
• CommentTimeAug 26th 2022

So won’t Synthetic Spectra via a Monadic and Comonadic Modality with its synthetic definitions of $\Sigma^\infty$ and $\Omega^\infty$ (Def. 3.14 and 3.17) be relevant to linear HoTT, and yet just a couple of references to linear logic.

• CommentRowNumber32.
• CommentAuthorDavid_Corfield
• CommentTimeAug 28th 2022
• (edited Sep 15th 2022)

Seeing that they have $\Omega^{\infty} E := \natural (\mathbb{S} \to E)$ and $\Sigma^{\infty} E := E \wedge \mathbb{S}$, then $! = \Sigma^\infty \Omega^\infty$ is like a variation on the store comonad,

$D X : X \rightarrow W \times [W,X].$
• CommentRowNumber33.
• CommentAuthorDavid_Corfield
• CommentTimeSep 3rd 2022

So is there some kind of base change adjoint triple between $Spectra/\mathbb{S}$ and $Spectra$?

All $E_{\infty}$-rings are $\mathbb{S}$-graded.

• CommentRowNumber34.
• CommentAuthorUrs
• CommentTimeDec 31st 2022

• CommentRowNumber35.
• CommentAuthorUrs
• CommentTimeMar 30th 2023
• (edited Mar 30th 2023)

I have expanded the Idea section:

In a new subsection “Absence of weakening and contraction” (here) I have added actual discussion of these inference rules and what it means when they are absent.

Then in “As a quantum logic” (here) I have used this to amplify the natural relation to quantum logic, in particular making explicit that

no contraction $\leftrightarrow$ no cloning

no weakening $\leftrightarrow$ no deleting

Ended this section with a comment highlighting the remarkable fact that the perspective on resource-availability has meanwhile been independently noted in quantum information theory (by people who mostly will have never heard of linear logic).

This then naturally leads over to the sub-section on resource availability (here). But I haven’t worked on that section yet. I find it needs a complete rewrite (because that whimsical example, which is its sole content, of “have cake $\vdash$ eat cake “, is of dubious value, at least as long as there is no serious example accompanying it.)

• CommentRowNumber36.
• CommentAuthorUrs
• CommentTimeMar 30th 2023

fixed numerous occurrences of “relevant logic” to “relevance logic”

• CommentRowNumber37.
• CommentAuthorDavid_Corfield
• CommentTimeMar 30th 2023

In the box at the start of ’Absence of weakening and contraction’ (here), the top right entry for semantics of cloning should have the arrow $\Gamma \times P \times P \to T$.

• CommentRowNumber38.
• CommentAuthorUrs
• CommentTimeMar 30th 2023

Thanks. I have fixed that typo and also beautified the alignments a little (here)

• CommentRowNumber39.
• CommentAuthorUrs
• CommentTimeApr 8th 2023
• (edited Apr 8th 2023)