Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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$.
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 }$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.
Understood (and agreed); I was just explaining the likely reason the original form was the way it was (I’m guessing I wrote that).
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
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”.
It almost surely is not a typo – it’s Toby’s preferred word.
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.
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
- 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.
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.
Re #15: dictionaries list two different meanings for “categorical”, for example, Wiktionary says
Absolute; having no exception.
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.
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.
Added to references
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.
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.
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).
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.
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…
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.
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.
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].$So is there some kind of base change adjoint triple between $Spectra/\mathbb{S}$ and $Spectra$?
All $E_{\infty}$-rings are $\mathbb{S}$-graded.
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.)
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$.
added pointer to:
1 to 39 of 39