Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
  
  
• Remember me

• Forgot your password?
• Apply for membership

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-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite 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 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

1. • CommentRowNumber1.
   • CommentAuthorMike Shulman
   • CommentTimeOct 11th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThe [linear logic wiki](http://llwiki.ens-lyon.fr/mediawiki/index.php/Translations_of_classical_logic) describes several translations of classical logic into linear logic, which translate the classical implication $A\to B$ as the linear $!? A' \multimap ?B'$ or $?(!A' \multimap B')$ or $!(A' \multimap ?B')$, or $!A' \multimap ?!B'$ (where $A'$ and $B'$ translate $A$ and $B$ respectively). But [wikipedia](https://en.wikipedia.org/wiki/Linear_logic#Encoding_classical.2Fintuitionistic_logic_in_linear_logic) claims that it can be translated as $!A' \multimap ?B'$, which is none of these. Is wikipedia wrong?

   The linear logic wiki describes several translations of classical logic into linear logic, which translate the classical implication as the linear or or , or (where and translate and respectively). But wikipedia claims that it can be translated as , which is none of these. Is wikipedia wrong?

2. • CommentRowNumber2.
   • CommentAuthorNoam_Zeilberger
   • CommentTimeOct 11th 2017
   • PermaLink
   Author: Noam_Zeilberger
   Format: MarkdownItexI'm pretty sure that the translation $!A' \multimap ?B'$ is correct, from the intuition that classical sequent calculus allows weakening/contraction both on the left and on the right. As a sanity check, here is [a derivation of Peirce's law](http://bach.istc.kobe-u.ac.jp/cgi-bin/llprover.cgi?system=cll&sysopt=full&formula=%5B%5D+--%3E+%21%28%21%28%21p+-%3E+%3Fq%29+-%3E+%3Fp%29+-%3E+%3Fp&formula1=&style=twosided&output=pretty&threshold=3) found by [llprover](http://bach.istc.kobe-u.ac.jp/llprover/): <pre> ------- Ax p --> p -------- R? p --> ?p ----------- W? p --> ?q,?p ------------ L! !p --> ?q,?p --------------- R-> --> !p-> ?q,?p ------------------- R! --------- Ax --> ! (!p-> ?q),?p ?p --> ?p --------------------------------- L-> ! (!p-> ?q)-> ?p --> ?p,?p -------------------------- C? ! (!p-> ?q)-> ?p --> ?p --------------------------- L! ! (! (!p-> ?q)-> ?p) --> ?p ------------------------------ R-> --> ! (! (!p-> ?q)-> ?p)-> ?p </pre> The "T" and "Q" translations on the linear logic wiki are references to an old paper by Danos, Joinet and Schellinx, [LKQ and LKT: sequent calculi for second order logic based upon dual linear decompositions of classical implication](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.127.4245).

   I’m pretty sure that the translation is correct, from the intuition that classical sequent calculus allows weakening/contraction both on the left and on the right. As a sanity check, here is a derivation of Peirce’s law found by llprover:

   ------- Ax
   p --> p
   -------- R?
   p --> ?p
   ----------- W?
   p --> ?q,?p
   ------------ L!
   !p --> ?q,?p
   --------------- R->
    --> !p-> ?q,?p
   ------------------- R!  --------- Ax
    --> ! (!p-> ?q),?p     ?p --> ?p
   --------------------------------- L->
      ! (!p-> ?q)-> ?p --> ?p,?p
      -------------------------- C?
       ! (!p-> ?q)-> ?p --> ?p
       --------------------------- L!
       ! (! (!p-> ?q)-> ?p) --> ?p
       ------------------------------ R->
        --> ! (! (!p-> ?q)-> ?p)-> ?p
   

   The “T” and “Q” translations on the linear logic wiki are references to an old paper by Danos, Joinet and Schellinx, LKQ and LKT: sequent calculi for second order logic based upon dual linear decompositions of classical implication.

3. • CommentRowNumber3.
   • CommentAuthorNoam_Zeilberger
   • CommentTimeOct 11th 2017
   • (edited Oct 11th 2017)
   • PermaLink
   Author: Noam_Zeilberger
   Format: MarkdownItexBy the way, part of the background/motivation for these less "economical" translations T and Q was to obtain non-degenerate semantics of _proofs_ in classical sequent calculus (rather than just classical provabiliy), where "non-degenerate" means "not all proofs are equated under cut-elimination". The naive interpretation of classical sequent calculus runs into the problem of "Lafont's critical pair": given any pair of proofs $\alpha_1,\alpha_2$ of $\Gamma \vdash \Delta$, we right-weaken $\alpha_1$ to a proof of $\Gamma\vdash \Delta,A$, left-weaken $\alpha_2$ to a proof of $A,\Gamma\vdash \Delta$, cut the two resulting proofs together to get a proof of $\Gamma,\Gamma \vdash \Delta,\Delta$, and apply repeated contraction to get a new proof $\beta$ of $\Gamma \vdash \Delta$. Under cut-elimination, $\beta$ can reduce to either $\alpha_1$ or $\alpha_2$, so we must have $[[ \alpha_1 ]] \equiv [[ \alpha_2 ]]$ (at least under a naive semantics of proofs). I think of the DJS paper as an attempt at giving more constructive semantics to classical logic via translation to linear logic, and as a precursor to better ways of understanding such translations via polarities and focusing and all that jazz.

   By the way, part of the background/motivation for these less “economical” translations T and Q was to obtain non-degenerate semantics of proofs in classical sequent calculus (rather than just classical provabiliy), where “non-degenerate” means “not all proofs are equated under cut-elimination”. The naive interpretation of classical sequent calculus runs into the problem of “Lafont’s critical pair”: given any pair of proofs of , we right-weaken to a proof of , left-weaken to a proof of , cut the two resulting proofs together to get a proof of , and apply repeated contraction to get a new proof of . Under cut-elimination, can reduce to either or , so we must have (at least under a naive semantics of proofs).

   I think of the DJS paper as an attempt at giving more constructive semantics to classical logic via translation to linear logic, and as a precursor to better ways of understanding such translations via polarities and focusing and all that jazz.

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeOct 11th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexAh, interesting, thanks. Do you know a citation for the $!A' \multimap ?B'$ translation?

   Ah, interesting, thanks. Do you know a citation for the translation?

5. • CommentRowNumber5.
   • CommentAuthorNoam_Zeilberger
   • CommentTimeOct 11th 2017
   • (edited Oct 11th 2017)
   • PermaLink
   Author: Noam_Zeilberger
   Format: MarkdownItex> Do you know a citation for the $!A' \multimap ?B'$ translation? Actually I'm not sure, I was wondering about that... It doesn't seem to be in Girard's [original linear logic paper](http://www.sciencedirect.com/science/article/pii/0304397587900454) (see Sections 5.4 and 5.5 for different translations of classical logic), or in [linear logic: its syntax and semantics](http://iml.univ-mrs.fr/~girard/Synsem.pdf). And I just saw in some [notes by Emmanuel Beffara](https://hal.archives-ouvertes.fr/cel-01144229/document) it says that "translating $A \Rightarrow B$ into $!A \multimap ?B$ does not work", so I might be missing something.

   Do you know a citation for the translation?

   Actually I’m not sure, I was wondering about that…

   It doesn’t seem to be in Girard’s original linear logic paper (see Sections 5.4 and 5.5 for different translations of classical logic), or in linear logic: its syntax and semantics. And I just saw in some notes by Emmanuel Beffara it says that “translating into does not work”, so I might be missing something.

6. • CommentRowNumber6.
   • CommentAuthorNoam_Zeilberger
   • CommentTimeOct 11th 2017
   • PermaLink
   Author: Noam_Zeilberger
   Format: MarkdownItexOkay, here is a counterexample: $\vdash^{CL} (q \supset r) \supset ((p \supset q) \supset (p \supset r))$ but not $\vdash^{LL} !(! q \multimap ? r) \multimap ?(!(! p \multimap ? q) \multimap ? (! p \multimap ? r) ) )$. So in #2 I was thinking about weakening and contraction, but the counterexample is just composition! Whoops!

   Okay, here is a counterexample: but not .

   So in #2 I was thinking about weakening and contraction, but the counterexample is just composition! Whoops!

7. • CommentRowNumber7.
   • CommentAuthorNoam_Zeilberger
   • CommentTimeOct 11th 2017
   • (edited Oct 11th 2017)
   • PermaLink
   Author: Noam_Zeilberger
   Format: MarkdownItexOne way to see the reason for the failure is to consider a classical cut: $$ \frac{\Gamma_1 \vdash A,\Delta_1 \quad \Gamma_2, A \vdash \Delta_2}{\Gamma_1,\Gamma_2 \vdash \Delta_1,\Delta_2} $$ If we translate classical sequents $\Gamma \vdash \Delta$ by linear sequents $! \Gamma^* \vdash ? \Delta^*$, then we get stuck trying to compose a proof of $!\Gamma_1^* \vdash ?A^*,?\Delta_1^*$ with a proof of $!\Gamma_2^*, !A^* \vdash ?\Delta_2^*$. On the other hand, if we use the translation $! \Gamma^* \vdash ?! \Delta^*$, then we get a proof of $!\Gamma_1^* \vdash ?!A^*,?!\Delta_1^*$ and a proof of $!\Gamma_2^*, !A^* \vdash ?!\Delta_2^*$, and we can apply left-promotion on the right premise to get $!\Gamma_2^*, ?!A^* \vdash ?!\Delta_2^*$, and then cut. Dually, if we use the translation $!? \Gamma^* \vdash ? \Delta^*$ then we can apply right-promotion on the left premise and then cut.

   One way to see the reason for the failure is to consider a classical cut:

   If we translate classical sequents by linear sequents , then we get stuck trying to compose a proof of with a proof of . On the other hand, if we use the translation , then we get a proof of and a proof of , and we can apply left-promotion on the right premise to get , and then cut. Dually, if we use the translation then we can apply right-promotion on the left premise and then cut.

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeOct 11th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexInteresting! How can you be sure that not $\vdash^{LL} !(! q \multimap ? r) \multimap ?(!(! p \multimap ? q) \multimap ? (! p \multimap ? r) ) )$? Someone should fix wikipedia, and we should also record this at [[linear logic]]. The reason I ask is that I'm looking at a particular model in which $!A \multimap ?B$ is an interesting thing, and unless I'm mistaken, in this model such things *do* compose. I wonder what extra structure this model has that makes that work.

   Interesting! How can you be sure that not ?

   Someone should fix wikipedia, and we should also record this at linear logic.

   The reason I ask is that I’m looking at a particular model in which is an interesting thing, and unless I’m mistaken, in this model such things do compose. I wonder what extra structure this model has that makes that work.

9. • CommentRowNumber9.
   • CommentAuthorNoam_Zeilberger
   • CommentTimeOct 11th 2017
   • (edited Oct 11th 2017)
   • PermaLink
   Author: Noam_Zeilberger
   Format: MarkdownItex> How can you be sure that not $\vdash^{LL} !(! q \multimap ? r) \multimap ?(!(! p \multimap ? q) \multimap ? (! p \multimap ? r) ) )$? Good question. I'm reasoning backwards about all possible cut-free proofs in the sequent calculus. Some of the !s and ?s are useless, so this goal reduces to proving $!q \multimap ?r, !p \multimap ?q, !p \vdash ?r$, which further reduces to proving $!q \multimap ?r, ?q \vdash ?r$ after applying the $\multimap$-left rule, then $!q \multimap ?r, q \vdash ?r$ after a left-promotion, and finally $q \vdash !q$ after another $\multimap$-left rule. But there is no way to prove the goal $q \vdash !q$ in general, so there is no proof of our original sequent. > The reason I ask is that I'm looking at a particular model in which $!A \multimap ?B$ is an interesting thing, and unless I'm mistaken, in this model such things *do* compose. I wonder what extra structure this model has that makes that work. Yeah, that's interesting. Does the model let you define morphisms of type $!q \multimap ?r, !p \multimap ?q \vdash !p \multimap ?r$, or does composition work in a different way?

   How can you be sure that not ?

   Good question. I’m reasoning backwards about all possible cut-free proofs in the sequent calculus. Some of the !s and ?s are useless, so this goal reduces to proving , which further reduces to proving after applying the -left rule, then after a left-promotion, and finally after another -left rule. But there is no way to prove the goal in general, so there is no proof of our original sequent.

   The reason I ask is that I’m looking at a particular model in which is an interesting thing, and unless I’m mistaken, in this model such things do compose. I wonder what extra structure this model has that makes that work.

   Yeah, that’s interesting. Does the model let you define morphisms of type , or does composition work in a different way?

10. • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeOct 12th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexUnless I got a dual misplaced (which is entirely possible), I think the model doesn't have $!q \multimap ?r, !p \multimap ?q \vdash !p \multimap ?r$, but instead something like $!(!q \multimap ?r), !(!p \multimap ?q) \vdash !p \multimap ?r$. The model is the $\ast$-autonomous category [[Sup]], with $!A = D A$ the suplattice of downsets in $A$ ordered by containment. This is the comonad induced on $Sup$ by the adjunction exhibiting it as monadic over $Pos$, i.e. $D A$ is the free suplattice on the poset $A$. Then $? A = (D A^*)^* = (D A^{op})^{op}$, which is the suplattice of upsets in $A$ ordered by reverse containment. I haven't checked all the details to be sure this acts like $!$, but I think this satisfies at least the law $!(A\times B) \cong !A \otimes !B$, since maps out of both of them classify arbitrary poset-maps out of $A\times B$. Note that the embedding of intuitionistic logic taking $A\to B$ to $!A \multimap B$ corresponds to building the Kleisli category of $D$, which is the category of suplattices and arbitrary poset-maps between them. To see what happens with composition, write $A \multimap B = (A \otimes B^*)^*$, so that $$!A \multimap ?B = (!A \otimes (?B)^*)^* = (!A \otimes !(B^*))^* = (!(A\times B^*))^* = ?(A^* \times B),$$ the suplattice of upsets in $A^* \times B$ ordered by reverse containment. This is also known as the opposite of the poset of $\mathbf{2}$-enriched profunctors $A^{op} \times B \to \mathbf{2}$. Since profunctors can be composed, taking the opposite of this composition map we get a map of posets $(!A \multimap ?B) \times (!B \multimap ?C) \to (!A \multimap ?C)$. Composition of profunctors is cocontinuous in each variable, but this is no longer the case when we take opposites, so this doesn't extend to a suplattice map on $(!A \multimap ?B) \otimes (!B \multimap ?C)$. But it does of course induce a suplattice map on $!((!A \multimap ?B) \times (!B \multimap ?C))$, which as noted above is equivalent to $!(!A \multimap ?B) \otimes !(!B \multimap ?C)$. This model also has other very special features not present in syntactic linear logic, such as $A\& B = A\oplus B$ and $(!A\multimap B)^* = (!(A^*) \multimap B^*)$, so it's not too surprising if this is another one of them. But I would like to understand it better. In particular, can the existence of this composition be expressed as a property (or property-like structure) of $D$ among comonads on $\ast$-autonomous categories?

    Unless I got a dual misplaced (which is entirely possible), I think the model doesn’t have , but instead something like .

    The model is the -autonomous category Sup, with the suplattice of downsets in ordered by containment. This is the comonad induced on by the adjunction exhibiting it as monadic over , i.e. is the free suplattice on the poset . Then , which is the suplattice of upsets in ordered by reverse containment. I haven’t checked all the details to be sure this acts like , but I think this satisfies at least the law , since maps out of both of them classify arbitrary poset-maps out of .

    Note that the embedding of intuitionistic logic taking to corresponds to building the Kleisli category of , which is the category of suplattices and arbitrary poset-maps between them.

    To see what happens with composition, write , so that

    the suplattice of upsets in ordered by reverse containment. This is also known as the opposite of the poset of -enriched profunctors . Since profunctors can be composed, taking the opposite of this composition map we get a map of posets . Composition of profunctors is cocontinuous in each variable, but this is no longer the case when we take opposites, so this doesn’t extend to a suplattice map on . But it does of course induce a suplattice map on , which as noted above is equivalent to .

    This model also has other very special features not present in syntactic linear logic, such as and , so it’s not too surprising if this is another one of them. But I would like to understand it better. In particular, can the existence of this composition be expressed as a property (or property-like structure) of among comonads on -autonomous categories?

11. • CommentRowNumber11.
    • CommentAuthorNoam_Zeilberger
    • CommentTimeOct 18th 2017
    • PermaLink
    Author: Noam_Zeilberger
    Format: MarkdownItexRe #8, I went ahead and fixed the Wikipedia article, and then looking back through the history realized that I was the one who originally introduced this mistake, way back in June 2009! That adds some (painful) irony to my being "pretty sure" the article's claim was correct... :-o So thanks, Mike, for bringing this issue up and helping me to correct the errors of my youth!

    Re #8, I went ahead and fixed the Wikipedia article, and then looking back through the history realized that I was the one who originally introduced this mistake, way back in June 2009! That adds some (painful) irony to my being “pretty sure” the article’s claim was correct… :-o So thanks, Mike, for bringing this issue up and helping me to correct the errors of my youth!

12. • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeOct 18th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexHaha! Thanks.

    Haha! Thanks.