Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes science set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: linear logic

Bottom of Page

1 to 43 of 43

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

    The cut rule for linear logic used to be stated as

    If Γ⊢A\Gamma \vdash A and A⊢ΔA \vdash \Delta, then Γ⊢Δ\Gamma \vdash \Delta.

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

    If Γ⊢A,Φ\Gamma \vdash A, \Phi and Ψ,A⊢Δ\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 **=AA^{\ast\ast} = A, I thought we would be able to derive your more general cut rule from the more specific cut rule:

    Γ⊢A,ΦΨ,A⊢Δ Γ,Φ *⊢AA⊢Ψ *,Δ Γ,Φ *⊢Ψ *,Δ Ψ,Γ⊢Δ,Φ \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.)

    diff, v80, current

    • CommentRowNumber6.
    • CommentAuthorBenMacAdam
    • CommentTimeMar 24th 2019

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

    diff, v82, current

  7. Link to game semantics article

    Ammar Husain

    diff, v84, current

  8. Copycat example.

    Ammar Husain

    diff, v84, current

  9. Caires, Pfenning

    Ammar Husain

    diff, v85, current

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeNov 12th 2019

    Added some redirects

    diff, v87, current

    • CommentRowNumber11.
    • CommentAuthorAdeleLopez
    • CommentTimeFeb 16th 2020

    fixing dead link

    diff, v89, current

    • CommentRowNumber12.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 17th 2020

    Mention Mike's antithesis interpretation.

    diff, v90, current

    • 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.

    diff, v92, current

  14. 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

    diff, v94, current

    • 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.

  22. Fix Bierman thesis link

    Anonymous

    diff, v100, current

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

    Anonymous

    diff, v101, current

    • CommentRowNumber24.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 21st 2022

    Added to references

    • 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)

    diff, v103, current

    • 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 XX 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↦∑X1 XX \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 Ω ∞E:=♮(𝕊→E)\Omega^{\infty} E := \natural (\mathbb{S} \to E) and Σ ∞E:=E∧𝕊\Sigma^{\infty} E := E \wedge \mathbb{S}, then !=Σ ∞Ω ∞! = \Sigma^\infty \Omega^\infty is like a variation on the store comonad,

    DX:X→W×[W,X]. 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/𝕊Spectra/\mathbb{S} and SpectraSpectra?

    All E ∞E_{\infty}-rings are 𝕊\mathbb{S}-graded.

    • CommentRowNumber34.
    • CommentAuthorUrs
    • CommentTimeDec 31st 2022

    added pointer to:

    diff, v107, current

    • 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.)

    diff, v111, current

    • CommentRowNumber36.
    • CommentAuthorUrs
    • CommentTimeMar 30th 2023

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

    diff, v111, current

    • 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 Γ×P×P→T\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)

    diff, v113, current

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

    added pointer to:

    diff, v116, current

    • CommentRowNumber40.
    • CommentAuthorUrs
    • CommentTimeSep 4th 2023

    added pointer to:

    here and elsewhere

    diff, v124, current

    • CommentRowNumber41.
    • CommentAuthorUrs
    • CommentTimeSep 4th 2023

    added pointer to:

    diff, v125, current

    • CommentRowNumber42.
    • CommentAuthorUrs
    • CommentTimeMay 31st 2024

    added pointer to:

    also re-shuffled the list of references, given the quantum-applications its own subsection, for better discernability

    diff, v129, current

  43. moving section on the antithesis interpretation in linear logic to its own page at antithesis interpretation

    Anonymouse

    diff, v133, current

1 to 43 of 43

  1.