Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

May 19, 2018

Linear Logic for Constructive Mathematics

Posted by Mike Shulman

Intuitionistic logic, i.e. logic without the principle of excluded middle (P¬PP \vee \neg P), is important for many reasons. One is that it arises naturally as the internal logic of toposes and more general categories. Another is that it is the logic traditionally used by constructive mathematicians — mathematicians following Brouwer, Heyting, and Bishop, who want all proofs to have “computational” or “algorithmic” content. Brouwer observed that excluded middle is the primary origin of nonconstructive proofs; thus using intuitionistic logic yields a mathematics in which all proofs are constructive.

However, there are other logics that constructivists might have chosen for this purpose instead of intuitionistic logic. In particular, Girard’s (classical) linear logic was explicitly introduced as a “constructive” logic that nevertheless retains a form of the law of excluded middle. But so far, essentially no constructive mathematicians have seriously considered replacing intuitionistic logic with any such alternative. I will refrain from speculating on why not. Instead, in a paper appearing on the arXiv today:

I argue that in fact, constructive mathematicians (going all the way back to Brouwer) have already been using linear logic without realizing it!

Let me explain what I mean by this and how it comes about — starting with an explanation, for a category theorist, of what linear logic is in the first place.

When we first learn about logic, we often learn various tautologies such as de Morgan’s laws ¬(PQ)(¬P¬Q)\neg(P \wedge Q ) \equiv (\neg P \vee \neg Q) and the law of excluded middle P¬PP \vee \neg P. (As usual, \wedge denotes “and”, while \vee denotes “or”.) The field of algebraic semantics of logic starts with the observation that these same laws can be regarded as axioms on a poset, with \wedge denoting the binary meet (greatest lower bound) and \vee the join (least upper bound). The laws of classical logic correspond to requiring such a poset to be a Boolean algebra. Thus, a proof in propositional logic actually shows an equation that must hold in all Boolean algebras.

This suggests there should be other “logics” corresponding to other ordered/algebraic structures. For instance, a Heyting algebra is a lattice that, considered as a thin category, is cartesian closed. That is, in addition to the meet \wedge and join \vee, it has an “implication” PQP\to Q satisfying (PQR)(PQR)(P\le Q\to R) \iff (P \wedge Q \le R). Any Boolean algebra is a Heyting algebra (with (PQ)(¬PQ)(P\to Q) \equiv (\neg P \vee Q)), but not conversely. For instance, the open-set lattice of a topological space is a Heyting algebra, but not generally a Boolean one. The logic corresponding to Heyting algebras is usually called intuitionistic logic, and as noted above it is also the traditional logic of constructive mathematics.

(Note: calling this “intuitionistic logic” is unfaithful to Brouwer’s original meaning of “intuitionism”, but unfortunately there seems to be no better name for it.)

Now we can further weaken the notion of Heyting algebra by asking for a closed symmetric monoidal lattice instead of a cartesian closed one. The corresponding logic is called intuitionistic linear logic: in addition to the meet \wedge and join \vee, it has a tensor product \otimes with internal-hom \multimap satisfying an adjunction (PQR)(PQR)(P\le Q\multimap R) \iff (P \otimes Q \le R). Logically, both \wedge and \otimes are versions of “and”; we call \wedge the “additive conjunction” and \otimes the “multiplicative conjunction”.

Note that to get from closed symmetric monoidal lattices to Boolean algebras by way of Heyting algebras, we first make the monoidal structure cartesian and then impose self-duality. (A Boolean algebra is precisely a Heyting algebra such that P(P0)0P \equiv (P\to 0)\to 0, where 00 is the bottom element and P0P\to 0 is the intuitionistic “not PP”.) But we can also impose self-duality first and then make the monoidal structure cartesian, obtaining an intermediate structure called a star-autonomous lattice: a closed symmetric monoidal lattice equipped with an object \bot (not necessarily the bottom element) such that P(P)P \equiv (P\multimap \bot)\multimap \bot. Such a lattice has a contravariant involution defined by P =(P)P^\perp = (P \multimap \bot) and a “cotensor product” (PQ)(P Q ) (P \parr Q) \equiv (P^\perp \otimes Q^\perp)^\perp, and its internal-hom is definable in terms of these: (PQ)(P Q)(P \multimap Q) \equiv (P^\perp \parr Q). Its logic is called (classical) linear logic: in addition to the two conjunctions \wedge and \otimes, it has two disjunctions \vee and \parr, again called “additive” and “multiplicative”.

Star-autonomous lattices are not quite as easy to come by as Heyting algebras, but one general way to produce them is the Chu construction. (I blogged about this last year from a rather different perspective; in this post we’re restricting it to the case of posets.) Suppose CC is a closed symmetric monoidal lattice, and \bot is any element of CC at all. Then there is a star-autonomous lattice Chu(C,)Chu(C,\bot) whose objects are pairs (P +,P )(P^+,P^-) such that P +P P^+ \otimes P^- \le \bot, and whose order is defined by ((P +,P )(Q +,Q ))(P +Q +)and(Q P ).((P^+,P^-) \le (Q^+,Q^-)) \iff (P^+ \le Q^+) \;\text{and}\; (Q^- \le P^-). In other words, Chu(C,)Chu(C,\bot) is a full sub-poset of C×C opC\times C^{op}. Its lattice operations are pointwise: (P +,P )(Q +,Q )(P +Q +,P Q ) (P^+,P^-) \wedge (Q^+,Q^-) \equiv (P^+ \wedge Q^+, P^- \vee Q^-) (P +,P )(Q +,Q )(P +Q +,P Q ) (P^+,P^-) \vee (Q^+,Q^-) \equiv (P^+ \vee Q^+, P^- \wedge Q^-) while the tensor product is more interesting: (P +,P )(Q +,Q )(P +Q +,(P +Q )(Q +P )) (P^+,P^-) \otimes (Q^+,Q^-) \equiv (P^+ \otimes Q^+, (P^+ \multimap Q^-) \wedge (Q^+ \multimap P^-)) The self-duality is (P +,P ) (P ,P +). (P^+,P^-)^\bot \equiv (P^-,P^+). from which we can deduce the definitions of \parr and \multimap: (P +,P )(Q +,Q )((P Q +)(Q P +),P Q ). (P^+,P^-) \parr (Q^+,Q^-) \equiv ((P^- \multimap Q^+) \wedge (Q^- \multimap P^+), P^- \otimes Q^-). (P +,P )(Q +,Q )((P +Q +)(Q P ),P +Q ). (P^+,P^-) \multimap (Q^+,Q^-) \equiv ((P^+ \multimap Q^+) \wedge (Q^- \multimap P^-), P^+ \otimes Q^-).

Where do closed symmetric monoidal lattices come from? Well, they include all Heyting algebras! So if we have any Heyting algebra, all we need to do to get a star-autonomous lattice from the Chu construction is to pick an object \bot. One natural choice is the bottom element 00, since that would be the self-dualizing object if our Heyting algebra were a Boolean algebra. The resulting monoidal structure on Chu(H,0)Chu(H,0) is actually semicartesian: the monoidal unit coincides with the top element (1,0)(1,0).

The point, now, is to look at this Chu construction Chu(H,0)Chu(H,0) from the logical perspective, where elements of HH are regarded as propositions in intuitionistic logic. The elements of Chu(H,0)Chu(H,0) are pairs (P +,P )(P^+, P^-) such that P +P =0P^+ \wedge P^- = 0, i.e. pairs of mutually incompatible propositions. We think of such a pair as a proposition PP together with information P +P^+ about what it means to affirm or prove it and also information P P^- about what it means to refute or disprove it. The condition P +P =0P^+ \wedge P^- = 0 means that PP cannot be both proven and refuted; but we might still have propositions such as (0,0)(0,0) which can be neither proven nor refuted.

The above definitions of the operations in a Chu construction similarly translate into “explanations” of the additive connectives ,\wedge,\vee and the multiplicative connectives ,\otimes,\parr in terms of affirmations and refutations:

  • A proof of PQP\wedge Q is a proof of PP together with a proof of QQ. A refutation of PQP\wedge Q is either a refutation of PP or a refutation of QQ.
  • A proof of PQP\vee Q is either a proof of PP or a proof of QQ. A refutation of PQP\vee Q is a refutation of PP together with a refutation of QQ.
  • A proof of P P^\perp is a refutation of PP. A refutation of P P^\perp is a proof of PP.
  • A proof of PQP\otimes Q is, like for PQP\wedge Q, a proof of PP together with a proof of QQ. But a refutation of PQP\otimes Q consists of both (1) a construction of a refutation of QQ from any proof of PP, and (2) a construction of a refutation of PP from any proof of QQ.
  • A proof of PQP\parr Q consists of both (1) a construction of a proof of QQ from any refutation of PP, and (2) a construction of a proof of PP from any refutation of QQ. A refutation of PQP\parr Q is, like for PQP\vee Q, a refutation of PP together with a refutation of QQ.

These explanations constitute a “meaning explanation” for classical linear logic, parallel to the Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic. In particular, they justify the characteristic features of linear logic. For instance, the “additive law of excluded middle” PP P \vee P^\perp fails for the same reason that it fails under the BHK-interpretation: we cannot decide for an arbitrary PP whether to prove it or refute it. However, the “multiplicative law of excluded middle” PP P \parr P^\perp is a tautology: if we can refute PP, then by definition we can prove P P^\perp, while if we can refute P P^\perp, then again by definition we can prove PP. In general, the multiplicative disjunction \parr often carries the “constructive content” of what the classical mathematician means by “or”, whereas the additive one \vee carries the constructive mathematician’s meaning. (Note also that the “proof” clauses of PQP\parr Q are essentially the disjunctive syllogism.)

I think this is already pretty neat. Linear logic, regarded as a logic, has always been rather mysterious to me, especially the multiplicative disjunction \parr (and I know I’m not alone in that). But this construction explains both of them quite nicely.

However, there’s more. It’s not much good to have a logic if we can’t do mathematics with it, so let’s do some mathematics in linear logic, translate it into intuitionistic logic along this Chu construction, and see what we get. In this post I won’t be precise about the context in which this happens; the paper formalizes it more carefully as a “linear tripos”. Following the paper, I’ll call this the standard interpretation.

To start with, every set should have an equality relation. Thus, a set in linear logic (which I’ll call an “L-set”) will have a relation (x= Ly)(x=^L y) valued in linear propositions. Since each of these is an element of Chu(H,0)Chu(H,0), it is a pair of mutually incompatible intuitionistic relations; we will call these (x= Iy(x=^I y and (x Iy)(x\neq^I y) respectively.

Now we expect equality to be, among other things, a reflexive, symmetric, and transitive relation. Reflexivity means that (x= Ix,x Ix)(1,0)(x=^I x, x\neq^I x) \equiv (1,0), i.e. that x= Ixx =^I x is true (that is, = I=^I is reflexive) and x Ixx \neq^I x is false (that is, I\neq^I is irreflexive). Symmetry means that (x= Iy,x Iy)(y= Ix,y Ix)(x=^I y, x\neq^I y) \equiv (y=^I x, y\neq^I x), i.e. that (x= Iy)(y= Ix)(x=^I y) \equiv (y=^I x) and (x Iy)(y Ix)(x\neq^I y) \equiv (y\neq^I x): that is, = I=^I and I\neq^I are both symmetric.

Of course, transitivity says that if x=yx=y and y=zy=z, then x=zx=z. But in linear logic we have two different “and”s; which do we mean here? Suppose first we use the additive conjunction \wedge, so that transitivity says (x= Ly)(y= Lz)(x= Lz)(x=^L y) \wedge (y=^L z) \vdash (x=^L z) (here \vdash is the logical equivalent of the inequality \le in our lattices). Using the definition of \wedge in Chu(H,0)Chu(H,0), this says that (x= Iy)(y= Iz)(x= Iz)(x=^I y) \wedge (y=^I z) \vdash (x=^I z) (that is, = I=^I is transitive) and (x Iz)(x Iy)(y Iz)(x\neq^I z) \vdash (x\neq^I y) \vee (y\neq^I z) (this is sometimes called comparison).

Put together, the assertions that = L=^L is reflexive, symmetric, and transitive say that (1) = I=^I is reflexive, symmetric, and transitive, and (2) I\neq^I is irreflexive, symmetric, and a comparison. Part (1) says essentially that an L-set has an underlying I-set, while (2) says that this I-set is equipped with an apartness relation.

Apartness relations are a well-known notion in constructive mathematics; if you’ve never encountered them before, here’s the idea. In classical mathematics, if we need to say that two things are “distinct” we just say that they are “not equal”. However, in intuitionistic logic, being “not equal” is not always a very useful thing. For instance, we cannot prove intuitionistically that if a real number is not equal to zero then it is invertible. However, we can prove that every real number that is apart from zero is invertible, where two real numbers are “apart” if there is a positive rational distance between them. This notion of “apart” is an irreflexive symmetric comparison which is stronger than “not equal”, and many other sets in intuitionistic mathematics are similarly equipped with such relations.

The point is that the standard interpretation automatically produces the notion of “apartness relation”, which constructive mathematicians using intuitionistic logic were led to from purely practical considerations. This same sort of thing happens over and over, and is what I mean by “constructive mathematicians have been using linear logic without realizing it”: they invented lots of concepts which are invisible to classical mathematics, and which may seem ad hoc at first, but actually arise automatically if we do mathematics “naturally” in linear logic and then pass across the standard interpretation.

To convince you that this happens all over the place, here are a bunch more examples.

  1. If AA and BB are L-sets, then in the cartesian product L-set A×BA\times B we have (a 1,b 1)= L(a 2,b 2)(a_1,b_1) =^L (a_2,b_2) defined by (a 1= La 2)(b 1= Lb 2)(a_1 =^L a_2) \wedge (b_1 =^L b_2). In the standard interpretation, this corresponds to the usual pairwise equality for ordered pairs and a disjunctive apartness: (a 1,b 1) I(a 2,b 2)(a_1,b_1) \neq^I (a_2,b_2) means (a 1 Ia 2)(b 1 Ib 2)(a_1 \neq^I a_2) \vee (b_1 \neq^I b_2). That is, two ordered pairs differ if they differ in one component.

  2. If AA and BB are sets, the elements of the function L-set ABA\to B are I-functions that are strongly extensional: (f(x) If(y))(x Iy)(f(x) \neq^I f(y)) \vdash (x\neq^I y) (this is called “strong” because the apartness I\neq^I may be stronger than “not equal”). This is a common condition on functions between sets with apartness relations.

  3. Equality between functions (f= Lg)(f =^L g) is defined by x.(f(x)= Lg(x))\forall x. (f(x) =^L g(x)). I didn’t talk about quantifiers /\forall/\exists above, but they act like infinitary versions of /\wedge/\vee. Thus we get (f= Ig)(f=^I g) meaning x.(f(x)= Ig(x))\forall x. (f(x) =^I g(x)), the usual pointwise equality of functions, and (f Ig)(f\neq^I g) meaning x.(f(x) Ig(x))\exists x. (f(x) \neq^I g(x)): two functions differ if they differ on at least one input.

  4. Because linear propositions are pairs of intuitionistic propositions, the elements of the L-powerset P(A)P(A) of an L-set AA are pairs (U +,U )(U^+,U^-) of I-subsets of the underlying I-set of AA, which must additionally be strongly disjoint in that (xU +)(yU )(x Iy)(x\in U^+) \wedge (y\in U^-) \vdash (x\neq^I y). Bishop and Bridges introduced such pairs in their book Constructive analysis under the name “complemented subset”. The substitution law (x= Ly)(xU)(yU)(x=^L y) \wedge (x\in U) \vdash (y\in U) translates to the requirement that U U^- be strongly extensional (also called “ I\neq^I-open”): (yU )(x Iy)(xU )(y\in U^-) \vdash (x\neq^I y) \vee (x\in U^-).

  5. Equality between L-subsets (U= LV)(U=^L V) means x.((xUxV)(xVxU))\forall x. ((x\in U \multimap x\in V) \wedge (x\in V \multimap x\in U)). In the standard interpretation, (U +,U )= I(V +,V )(U^+,U^-) =^I (V^+,V^-) means (U +=V +)(U =V )(U^+=V^+) \wedge (U^- = V^-) as we would expect, while (U +,U ) I(V +,V )(U^+,U^-) \neq^I (V^+,V^-) means (xU +V )(xU V +)(\exists x \in U^+ \cap V^-) \vee (\exists x\in U^- \cap V^+). In particular, we have U LU \neq^L \emptyset (where the empty L-subset is (,A)(\emptyset,A)) just when xU +\exists x\in U^+. So the obvious linear notion of “nonempty” translates to the intuitionistic notion of inhabited that constructive mathematicians have found to be much more useful than the intuitionistic “not empty”.

  6. An L-group is an L-set with a multiplication m:G×GGm:G\times G\to G, unit eGe\in G, and inversion i:GGi:G\to G satisfying the usual axioms. In the standard interpretation, this corresponds to an ordinary I-group equipped with an apartness I\neq^I such that multiplication and inversion are strongly extensional: (x 1 Iy 1)(x Iy)(x^{-1} \neq^I y^{-1}) \vdash (x \neq^I y) and (xu Iyv)(x Iy)(u Iv)(x u \neq^I y v) \vdash (x \neq^I y) \vee (u\neq^I v). Groups with apartness have been studied in intuitionistic algebra going back to Heyting, and similarly for other algebraic structures like rings and modules.

  7. An L-subgroup of an L-group corresponds to a complemented subset (H +,H )(H^+,H^-) as above such that H +H^+ is an ordinary I-subgroup and H H^- is an antisubgroup, meaning a set not containing ee, closed under inversion ((xH )(x 1H )(x\in H^-) \vdash (x^{-1}\in H^-)), and satisfying (xyH )(xH )(yH )(x y \in H^-) \vdash (x\in H^-) \vee (y\in H^-). Antisubgroups have also been studied in constructive algebra; for instance, they enable us to define an apartness on the quotient G/H +G/H^+ by [x] I[y][x]\neq^I [y] if xy 1H x y^{-1} \in H^-.

  8. An L-poset is an L-set with a relation L\le^L that is reflexive, transitive ((x Ly)(y Lz)(x Lz)(x\le^L y) \wedge (y\le^L z) \vdash (x\le^L z)) and antisymmetric ((x Ly)(y Lx)(x= Ly)(x\le^L y) \wedge (y\le^L x) \vdash (x =^L y)). Under the standard interpretation, this corresponds to two binary relations, which it is suggestive to write I\le^I and < I\lt^I: then I\le^I is an ordinary I-partial-order, < I\lt^I is a “bimodule” over it ((x Iy)(y< Iz)(x< Iz)(x\le^I y) \wedge (y \lt^I z) \vdash (x\lt^I z) and dually) which is cotransitive ((x< Iz)(x< Iy)(y< Iz)(x\lt^I z) \vdash (x\lt^I y) \vee (y\lt^I z)) and “anti-antisymmetric” in the sense that (x Iy)((x< Iy)(y< Ix))(x\neq^I y) \equiv ((x\lt^I y) \vee (y\lt^I x)). Such pairs of strict and non-strict relations are quite common in constructive mathematics, for instance on the real numbers.

In the paper there are even more examples of this sort of thing. However, even this is not all! So far, we haven’t made any use of the multiplicative connectives in linear logic. It turns out that often, replacing some or all of the additive connectives in a definition by multiplicative ones yields, under the standard interpretation, a different intuitionistic version of the same classical definition that is also useful.

Here are a few examples. Note that by semicartesianness (or “affineness” of our logic), we have PQPQP \otimes Q \vdash P\wedge Q and PQPQP\vee Q \vdash P \parr Q (in a general star-autonomous lattice, there may be no implication either way).

  1. A “\vee-field” is an L-ring such that (x= L0)y.(xy= L1)(x=^L 0) \vee \exists y. (x y =^L 1). Under the standard interpretation, this corresponds to an I-ring (with apartness) such that (x= I0)y.(xy= I1)(x=^I 0) \vee \exists y. (x y =^I 1), i.e. every element is either zero or invertible. The rational numbers are a field in this sense (sometimes called a geometric field or discrete field), but the real numbers are not. On the other hand, a “\parr-field” is an L-ring such that (x= L0)y.(xy= L1)(x=^L 0) \parr \exists y. (x y =^L 1). Under the standard interpretation, this corresponds to an I-ring (with apartness) such that (x I0)y.(xy= I1)(x \neq^I 0) \to \exists y. (x y =^I 1) and (y.(xy I1))(x= I0)(\forall y. (x y \neq^I 1)) \to (x =^I 0), i.e. every element apart from zero is invertible and every “strongly noninvertible” element is zero. The real numbers are a field in this weaker sense (if the apartness is tight, this is called a Heyting field).

  2. In classical mathematics, xyx\le y means (x<y)(x=y)(x\lt y) \vee (x=y). Constructively, this is (again) true for integers and rationals but not the reals. However, it is true for the reals in linear logic that (x Ly)(x< Ly)(x= Ly)(x\le^L y) \equiv (x\lt^L y) \parr (x=^L y).

  3. If in the definition of an L-set we weaken transitivity to (x= Ly)(y= Lz)(x= Lz)(x=^L y) \otimes (y=^L z) \vdash (x=^L z), then in the standard interpretation the comparison condition disappears, so that I\neq^I need only be irreflexive and symmetric, i.e. an inequality relation. (To be precise, the comparison condition is actually replaced by the weaker statement that I\neq^I satisfies substitution with respect to = I=^I.) This is useful because not every I-set has an apartness relation, but every I-set does have at least one inequality relation, namely “not equal” (the denial inequality). There are also other inequality relations that are not apartnesses. For instance, the inequality defined above on L-powersets is not an apartness but is still stronger than “not equal”, and in the paper there is an example of a very naturally-occurring normal L-subgroup of a very naturally occurring L-group for which the inequality on the quotient is not an apartness.

Again, there are more examples in the paper, including generalized metric spaces and topological/apartness spaces. (I should warn you that the terminology and notation in the paper is somewhat different; in this post I’ve been constrained in the math symbols available, and also omitted some adjectives for simplicity.)

What does this observation mean for constructive mathematics? Well, there are three levels at which it can be applied. Firstly, we can use it as a “machine” for producing constructive versions of classical definitions: write the classical definition in linear logic, making additive or multiplicative choices for the connectives, and then pass across the standard interpretation. The examples in the paper suggest that this is more “automatic” and less error-prone than the usual process of searching for constructive versions of classical notions.

Secondly, we can also use it as a machine for producing theorems about such constructive notions, by writing a proof in linear logic (perhaps by simply translating a classical proof — many classical proofs remain valid without significant changes) and translating across the standard interpretation. This can save effort and prevent mistakes (e.g. we don’t have to manually keep track of all the apartness relations, or worry about forgetting to prove that some function is strongly extensional).

Thirdly, if we start to do that a lot, we may notice that we might as well be doing constructive mathematics directly in linear logic. Linear logic has a “computational” interpretation just like intuitionistic logic does — its proofs satisfy “cut-elimination” and the “disjunction and existence properties” — so it should be just as good at ensuring that mathematics has computational content, with the benefit of not having to deal explicitly with apartness relations and so on. And the “meaning explanation” I described above, in terms of proofs and refutations, could theoretically have been given by Brouwer or Heyting instead of the now-standard BHK-interpretation. So one might argue that the prevalence of the latter is just a historical accident; maybe in the future a linear constructive mathematics will grow up alongside today’s “intuitionistic constructive mathematics”.

Posted at May 19, 2018 4:53 AM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/3040

29 Comments & 0 Trackbacks

Re: Linear Logic for Constructive Mathematics

Hi Michael,

This is really neat! The way you derive apartness is really very slick, and is absolutely going to be how I explain it from now on.

Two remarks about this post:

  1. About a decade ago, Kazushige Terui did quite a bit of work on set theories which used linear logic as their ambient logic – see his Light Affine Set Theory. The inspiration comes from the line of work on using linear logic to characterize complexity classes, and indeed Terui is able to prove that in LAST, a relation between A and B is functional if and only if there is a polynomial time algorithm sending A’s to B’s. (The thing I like about this set theory is that it’s a naive set theory, since the paradoxes of self-reference require contraction.)

    Sociologically, I think this also why constructive logicians have been hesitant to embrace linear logic: they tend to think of it as a logic of feasible computation (as contrasted with intuitionistic logic being a logic of pure computability). So it is seen as something even more subtle in its distinctions than constructive mathematics. When I asked Paul Taylor, he told me:

    The question, however, is I think about the difference between computability and feasibility (say polynomial time). Whilst there are resource logics that can talk about this, they would look very much more different from ordinary mathematics than ASD (abstract Stone duality) does. I think this needs to be sorted out at the computable level first, leaving the feasible version to another generation.

  2. However, there has been quite a bit of work on Chu-like constructions for giving realizability interpretations of classical logic – if you Google for “TT-closure” or “biorthogonality” or “J.L. Krivine”, you’ll find a lot of hits. For the audience here, I’d recommend Thomas Streicher’s Krivine’s Classical Realizability from a Categorical Perspective.

    Perhaps there is some connection between the tripos-like notion in your paper and Streicher’s, but since I haven’t done more than skim your paper yet, I couldn’t say.

Posted by: Neel Krishnaswami on May 22, 2018 5:21 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Thanks, I’m glad you like it.

I’ve read some of the work on linear/affine set theories and the relation between linearity and feasibility. I didn’t realize that it might be connected with the reluctance of constructive mathematicians to embrace linear logic, though. My impression was that in order to actually get a “logic of feasible computations” you have to do tricky things to the exponential modalities. (For the bystander, the “exponential modalities” are an aspect of linear logic that I didn’t discuss at all in the post, but they’re in the paper.)

To wit: if there are no exponential modalities at all then all your computations are linear, whereas with ordinary exponential modalities the logic becomes as expressive as intuitionistic logic and hence can express everything computable. (The latter, by the way, applies in the “standard interpretation” discussed in this post and the paper, so we lose no expressivity over intuitionistic logic.) To restrict to feasible computations you have to change the behavior of the modalities so that, for instance, instead of being able to duplicate a modal type !A!A!A!A \vdash !A \otimes !A you can instead “use it any finite number of times” !AAAA!A \vdash A \otimes A \otimes \cdots \otimes A. Right? So it seems to me that linear logic allows for a feasibility interpretation, but doesn’t require it.

However, I can certainly see that this work could have caused linear logic to be associated in people’s minds with feasibility, even though mathematically it doesn’t have to be so.

I’ll have a look at classical realizability, thanks!

Posted by: Mike Shulman on May 22, 2018 5:35 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

You are correct about exponential to model certain classes of complexity: they need to be weaker than usual. One keyword is light linear logic (which is precisely a linear logic with weaker modalities). More generally implicit complexity is the name given to the quest to capture complexity classes in types. They play all kind of tricks around linear logic.

I am not, however, convinced that we can deduce that linear logic is about feasibility. And I would expect the difficulty in adopting it as a mathematical formalism to lie elsewhere.

Posted by: Arnaud Spiwack on May 23, 2018 7:36 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

I had a look at Streicher’s paper (and nothing else yet), and although I agree that it does look sort of Chu-like, I can’t see any precise relationship yet.

The closest connection I can see would be to take his set Π\Pi of lists of lambda terms, regard it as a monoid under concatenation, then use that to make the powerset 𝒫(Π)\mathcal{P}(\Pi) into a quantale. His relation \bot between terms and lists of terms could then be made into an element of 𝒫(Π)\mathcal{P}(\Pi), namely the lists of the form t.πt.\pi where tpt\star p \in \bot. Then Chu(𝒫(Π),)Chu(\mathcal{P}(\Pi),\bot) is somewhat akin to the propositions in his realizability: its elements are pairs (|A|,A)({|A|},{\Vert A\Vert }) such that |A|.A{|A|}.{\Vert A \Vert} \subseteq \bot, which is exactly the condition on his pairs if we restrict |A|{|A|} to be a set of one-element lists (i.e. terms). His definition of \forall is exactly the Chu one, \bigcup on A{\Vert A\Vert} and \bigcap on |A|{|A|}. And his definition of AB{\Vert A \to B \Vert} is the Chu-like |A|.B{|A|}.{\Vert B\Vert}. He does always require |A|{|A|} to be the orthogonal of A{\Vert A\Vert}, but that sort of feels like inserting ?? modalities in appropriate places, maybe kind of the way you would when translating classical nonlinear logic into classical linear logic; and restricting |A|{|A|} to consist only of one-element lists could be a similar sort of coreflection.

However, the analogy breaks down in lots of other ways. For instance, 𝒫(Π)\mathcal{P}(\Pi) is a noncommutative quantale, whereas the ordinary Chu construction only works on closed symmetric monoidal categories. There is a noncommutative Chu construction, but its objects are not just pairs of objects in the original category, but doubly-infinite sequences of them. His definition of AB{\Vert A \to B\Vert} does, I think, extend to a definition of ABA\to B that is right adjoint to a sort of tensor product, but that tensor product is not associative. He doesn’t say anything about how to define conjunctions, disjunctions, and existentials; I suppose he is getting them in the higher-order way from implication and universals, but he must be using some extra property of his Π\Pi to make the implications behave correctly for this to work. That’s not surprising, of course, since in my sketch above I didn’t actually use any of the structure on the terms! But it makes it seem like all the interesting stuff is happening somewhere that has nothing to do with the Chu-like part.

Posted by: Mike Shulman on May 22, 2018 11:19 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

On |A||A| being the orthogonal of ||A||||A||: it’s not quite a ? modality, it’s a shift modality. That is, if you were to model a polarised logic in Krivine realisability, interpretation |A||A| of positive types would typically not be orthogonal (they contain only values. Give or take: I didn’t work this out precisely). However, the (negatively) shifted version of them would contain all terms which evaluate to these values, hence the double orthogonal of |A||A|.

Something along these lines anyway.

Posted by: Arnaud Spiwack on May 23, 2018 7:45 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Fascinating. So presumably, in an effort to tie together this post with your last, the Chu construction is a map between 2-theories, or a change of doctrine.

Posted by: David Corfield on May 22, 2018 9:05 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Unfortunately, I don’t quite see how to view the Chu construction as a morphism of 2-theories. The first problem is that Heyting algebras and *\ast-autonomous lattices live in different 3-theories: the first lives in intuitionistic logic and the second in classical logic. If we had a good 3-theory for classical logic that included cartesian cases, we could presumably express them both in there, and then ask about the Chu construction as a morphism there. But that 3-theory is still very much in progress, and even then I’m not sure that the Chu construction would behave like a morphism of theories.

Posted by: Mike Shulman on May 24, 2018 4:50 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Let’s see if I have this right. We have on the other thread the following 3-theories mentioned:

unary, simple, first-order, dependent, classical simple.

Then you speak there of 2-theories within 3-theories, such as first-order classical logic within the 3-theory of first-order logic, and

Other 2-theories in that same 3-theory are first-order intuitionistic logic, first-order linear logic, the type theory of indexed monoidal categories, first-order modal logic, etc.

Now you just said above:

…live in different 3-theories: the first lives in intuitionistic logic and the second in classical logic,

which might seem not to fit. But presumably by ‘classical logic’ here you mean that ‘classical simple’ type theory of before.

Is there a better terminological choice? It seems odd to have ‘classical’ play a role of determining a variety of 2-theory in a 3-theory (e.g., classical first-order logic in first-order logic), and then also play a role in describing a kind of 3-theory (classical simple).

(Or is it secretly because there is a 4-theory about, and you want plain ‘simple’ and ‘classical simple’ as 3-theories within it?)

Posted by: David Corfield on May 24, 2018 8:25 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

I am not using “classical” to determine a variety of 2-theory in a 3-theory, I’m only using it to indicate a theory whose “arity” (which is part of the 3-theory) is many-to-many, as opposed to the “intuitionistic” case in which the arity is many-to-one. These are traditional names for that, although I guess we could say “many-to-many” and “many-to-one” instead. When I said “first-order linear logic” as a 2-theory in the 3-theory of first-order logic, I meant first-order intuitionistic (i.e. many-to-one) linear logic, since I was thinking of the 3-theory of first-order logic as many-to-one. There should also be a 3-theory of “classical first-order logic” whose propositions are many-to-many (though whose base type theory is still many-to-one).

One way to renanme the 3-theories would be something like:

  • unary simple
  • many-to-one simple
  • many-to-many simple
  • many-to-one dependent on many-to-one
  • many-to-many dependent on many-to-one
  • many-to-one dependent on itself

So the basic Chu construction takes as input a symmetric monoidal category (or Heyting algebra, etc.), which lives in the 3-theory of “many-to-one simple”, and outputs a *\ast-autonomous category, which lives in the 3-theory of “many-to-many simple”. The “fibered” version takes a tripos, which lives in the 3-theory of “many-to-one dependent on many-to-one”, and outputs a linear tripos, which lives in the 3-theory of “many-to-many dependent on many-to-one”.

Posted by: Mike Shulman on May 24, 2018 2:35 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Mike, thanks for this beautiful post and paper; now I’m inspired to think more about what mathematics can be done with linear logic!

Posted by: Jon Sterling on May 23, 2018 2:03 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

You may find Sparks & Sabry’s Superstructural Reversible Logic to be of interest, which (just as linear logic adds a second version of “and”) adds a second version of “or”.

This, then, is used to ensure the conservation of choice, or - equivalently - the conservation of temporal resources just as linear logic ensures the conservation of spatial resources.

The fact that this then results in proofs/programs that are reversible is quite nice.

Another paper in the same vein is Computing with Semirings and Weak Rig Groupoids, which establishes higher such isomorphisms, allowing isomorphisms between isomorphisms.

There’s also From Reversible Programs to Univalent Universes and Back (based in the same formalism as both of the above papers), the relevance of which should require little further explanation :P

Posted by: Alex Elsayed on May 23, 2018 6:58 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Classical linear logic does, of course, have a second version of “or” as well, the multiplicative disjunction \parr. But I gather this must be different from the new (“third”?) version of “or” introduced in the paper you mention.

Posted by: Mike Shulman on May 23, 2018 7:49 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

This is all really quite interesting. I wanted to ask about exponentials, but you answered to this already. I’ll see the rest in the paper, when I get around to read it.

A small comment: it is really interesting that you get a useful version of transitivity using x=y&y=zx=zx=y\&y=z\multimap x=z as your definition. Because this is a very unnatural type: I don’t expect it to be provable within linear (or affine) logic, on pretty much any relation. Because the deduction rules basically tell you that you are only able to use the proof or x=yx=y or that of y=zy=z (your choice, though)to prove that x=zx=z, which seems unlikely.

So it ends up being quite a curious logic. I think. And there is a lot that I need to understand there (I’m saying all that, again, without reading the paper, so you may have already answered much of my interrogations there).

On the other hand, between this and the fact that your logic is affine rather than truly linear, the phrase « standard interpretation » sounds a bit of an overstatement.

Posted by: Arnaud Spiwack on May 23, 2018 7:56 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

It is, indeed, surprising; however, I believe that you can in fact prove x=yy=xx=zx=y \wedge y=x \multimap x=z in affine logic in many cases. The point is that you don’t have to choose right away whether to use x=yx=y or y=zy=z; you can first break down the structure of x,y,zx,y,z and use the definition of x=zx=z.

For instance, equality of natural numbers is defined by recursion: (0=0)(0=0)\equiv\top, (Sx=Sx)(x=y)(S x = S x) \equiv (x = y), and (0=Sx)(0 = S x) \equiv \bot. So to prove x=zx=z assuming x=yy=zx=y\wedge y=z, we do induction on x,y,zx,y,z. If xz0x\equiv z\equiv 0 we are done. If x0x\equiv 0 and zSzz\equiv S z', then we case on yy: if y0y\equiv 0 then we can use y=zy=z to get a contradiction, while if ySyy\equiv S y' we can use x=yx=y to get a contradiction. The case xSxx\equiv S x' and z0z\equiv 0 is similar. Finally, if xSxx\equiv S x' and zSzz\equiv S z', if y0y\equiv 0 we get a contradiction from either x=yx=y or y=zy=z, while if ySyy\equiv S y' we can apply the induction hypothesis x=yy=zx=zx'=y'\wedge y'=z' \multimap x'=z'. In no case do we actually need to use both x=yx=y and y=zy=z, but we have to “have both of them” (in the additive sense) because each of them is used in at least one case.

Now if AA and BB both satisfy this strong transitivity condition (in the paper I call them “strong sets”), it’s easy to see that so does A×BA\times B, where equality of ordered pairs is also defined using the additive conjunction \wedge. (In fact, even infinite products x:AB(x)\prod_{x:A} B(x) inherit strong equality from all the B(x)B(x)’s: to show f=hf=h means x,f(x)=h(x)\forall x, f(x)=h(x), and once we fix an xx we can get f(x)=h(x)f(x)=h(x) from f(x)=g(x)g(x)=h(x)f(x)=g(x) \wedge g(x)=h(x), which follows from f=gg=hf=g \wedge g=h.) Thus, the rational numbers are also a strong set.

Even the real numbers are a strong set! This is true for both kinds of real numbers, but I’ll sketch only the Dedekind case. Assuming x=yy=zx=y \wedge y=z, to prove x=zx=z means to prove that every rational q<xq\lt x is also <z\lt z and vice versa. Now if q<xq\lt x, since xx is an open section there is a rational rr with q<rq\lt r and r<xr\lt x. Then since yy is located, from q<rq\lt r we have either y<ry\lt r or q<yq\lt y (we define locatedness using the additive disjunction). If q<yq\lt y we can use y=zy=z to get q<zq\lt z. Whereas if y<ry\lt r, then together with r<xr\lt x we can get a contradiction from x=yx=y. Again, in neither case do we have to use both x=yx=y and y=zy=z, but each of them is used in at least one case.

What’s more, by translating this proof across the standard interpretation, we’ve just shown that the real numbers have an apartness relation as well.

I didn’t dwell on this sort of thing much in the paper: I wanted to keep it as concise as possible, and maximize the accessibility for readers who aren’t already familiar with linear logic, so I focused mainly on the semantics rather than on actually doing proofs in linear logic. I didn’t really think about how surprising it might be to a reader who is familiar with linear logic, so maybe it would be helpful for such readers if I include a bit more of this.

On the other hand, between this and the fact that your logic is affine rather than truly linear, the phrase « standard interpretation » sounds a bit of an overstatement.

Hah! Guilty as charged. In fact, because I couldn’t think of a good name, I deliberately chose a bad name, in hopes that someone else would be motivated to think of a good one. (-:O

One might think of calling it “the Chu interpretation”, but I think that would be an even worse idea, because the Chu construction is a very general way to produce models of linear logic and this is very specifically about Chu constructions applied to Heyting algebras with the bottom element as dualizer. There are even other Chu constructions on Heyting algebras, e.g. if you choose the top element as dualizer, instead of affine logic you get linear logic with MIX, a construction which is related to “Nelson’s constructible falsity” logic (Remark 3.9 in the paper).

Posted by: Mike Shulman on May 23, 2018 7:46 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Point taken. So &-transitivity is a thing. And is strongly tied to apartness (I’m guessing is will be provable of semi-decidable \otimes-transitive relation, more or less)

In fact, because I couldn’t think of a good name, I deliberately chose a bad name, in hopes that someone else would be motivated to think of a good one. (-:O

Sounds like something you would do, indeed :-) . I’ll let you know if I think of something. No promise.

Posted by: Arnaud Spiwack on May 23, 2018 8:25 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

And is strongly tied to apartness

Yes — in fact, if you dualize any proof of x=yy=zx=zx=y \wedge y=z \multimap x=z, you get a proof of the apartness property (x=z) (x=y) (y=z) (x=z)^\perp \multimap (x=y)^\perp \vee (y=z)^\perp. The above proofs of strong transitivity that I sketched are essentially the intuitionistic proofs of apartness “turned around”.

Posted by: Mike Shulman on May 23, 2018 10:52 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Hah! Guilty as charged. In fact, because I couldn’t think of a good name, I deliberately chose a bad name, in hopes that someone else would be motivated to think of a good one. (-:O

How about “propositions-as-complimentary-types”? This seems good for the “meaning explanation” at least. It’s motivated by CMOS logic gates. Every proposition gets a type of affirmations (how to pull the output high) and a type of refutations (how to pull the output low) such that no proposition has both an affirmation and a refutation (no short circuit). Propositions-as-types interpretation of intuitionistic logic seems more like PMOS logic.

Though your affine tripos construction is technically more like “propositions-as-complimentary-propositions”, and isn’t constructive in general.

Posted by: Matt Oliveri on May 28, 2018 11:28 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Thanks for trying! But I don’t think I’d want to write “a strong L-set in the propositions-as-complementary-propositions interpretation corresponds to an I-set with apartness”; there are about a dozen too many syllables there.

Posted by: Mike Shulman on May 28, 2018 11:42 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

You could pick an acronym if that’s the only problem. Actually I don’t like PACP as a name, only PACT. PACP sounds approximately as silly as “propositions-as-propositions”.

I think it’s really cool, by the way. I should have said that while I was commenting. If I’m ever in the situation where I need to formalize a serious amount of constructive math, I intend to try your approach. (Or something similar.)

Posted by: Matt Oliveri on May 29, 2018 2:36 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

In case anyone else was wondering about the exponentials but doesn’t (yet) want to spend the time to read the paper, the short answer is that they are !(P +,P )=(P +,¬P +)!(P^+,P^-) = (P^+, \neg P^+) and ?(P +,P )=(¬P ,P )?(P^+,P^-) = (\neg P^-,P^-). In other words, a proof of !P! P is a proof of PP, while a refutation of !P! P is a construction of an absurdity from any putative proof of PP. Interestingly, this is the only place that the intuitionistic negation appears in the Chu construction (the linear negation simply swaps proofs and refutations).

Posted by: Mike Shulman on May 24, 2018 4:51 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

A word about notation, in case any reader who is new to linear logic is confused: Arnaud’s &\& and my \wedge are both the additive conjunction. Girard originally used &\& and \oplus for the additive “and” and “or” respectively, and \otimes and \parr for the multiplicative “and” and “or” respectively. These notations are still fairly common among type theorists.

However, categorically-minded people (including me) seem to find it more intuitive to use parallel symbols for the two additive connectives and for the two multiplicative connectives, since each pair are each other’s categorical duals, analogous to ×/+\times/+ or /\prod/\coprod for product/coproduct. (Girard’s motivation for using parallel symbols for the additive “and” and the multiplicative “or” was probably that both of them are “negative”, while similarly the additive “or” and multiplicative “and” are both “positive”. Maybe to people who think about focusing more than categorical duality this is intuitive — although it’s still a break with an old tradition in logic (not just category theory) of using parallel symbols for dual operations, like \wedge and \vee for “and” and “or”, and Girard himself used \bigwedge and \bigvee for the linear quantifiers.)

Unfortunately there is no uniformity in a proposed alternative, and I have to confess to having found all the proposed alternatives unsatisfactory and invented yet another one myself in the paper. Since the additive conjunction and disjunction are the lattice-theoretic meet and join, it seems clear that something like /\wedge/\vee is appropriate for them (or ×/+\times/+ in a category that isn’t a poset); though in the paper I used /\sqcap/\sqcup to avoid confusion with the intuitionistic connectives. Cockett and Seely used /\otimes/\oplus for the multiplicative conjunction and disjunction, but I don’t like that because \oplus is almost universally used for direct sums (biproducts) in additive categories, which are very unlike the multiplicative disjunction (they are additive, for one thing). Jeff Egger uses \owedge and \ovee, whose only drawback from my perspective is that I have trouble distinguishing them from each other visually. My suggestion is to use \boxtimes for the multiplicative conjunction and a 45^\circ-rotated \boxtimes for the multiplicative disjunction; the latter thus looks like an “addition” but is easy to distingish from everything else and doesn’t clash with direct sums.

However, as long as we get away from &/\&/\oplus for the additive connectives, it’s not so bad to use \otimes and \parr for the multiplicative ones, as I did in this post: they aren’t visually dual to each other, but at least they don’t look visually dual to something that they aren’t (categorically) dual to; they’re available in iTeX; and \parr is (unlike all other notations for the multiplicative disjunction) totally unambiguous, because Girard essentially invented it for the purpose.

I am still trying to figure out the best ways to pronounce all of these connectives in English. Girard used “times”, “with”, “plus”, and “par” for ,,,\otimes,\wedge,\vee,\parr respectively. This may fly when you’re just talking about syntax, but when it comes to actually doing mathematics, the first three of those words are not really available to be given new meanings.

As with \parr, the word “par” is new and hence unproblematic. Moreover, it’s fairly clear to me that (as long as it’s established that the logic being used is linear/affine) we should use “and” and “or” for \otimes and \vee respectively. It seems that without exception it’s the additive \vee that corresponds to what a constructive mathematician is used to meaning by “or”, and probably at least half the time it’s what a classical mathematician means by “or” too (the rest of the time that being \parr). And it’s \otimes that behaves the way we are used to using “and” in hypotheses, namely that if we have PQP\otimes Q then we may as well have both PP and QQ as separate hypotheses; also we have (PQ)RP(QR)(P\otimes Q)\multimap R \equiv P\multimap (Q\multimap R), so this is the “and” that interacts as we expect with implication. So the odd one out that I don’t know how to pronounce is \wedge.

Posted by: Mike Shulman on May 24, 2018 5:36 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Let me offer a few corrections.

\otimes is generally pronounced “tensor”. As it \otimes is the standard notation for non-cartesian monoidal product, I think that it’s a fair notation, but, of course it doesn’t offer a reasonable similar-looking symbol for its dual.

It’s completely unproblematic, in my view, to replace & and \oplus with \wedge and \vee or ×\times and ++, or to pronounce them “and” and “or” for that matter (but I don’t know why you don’t like “with”). But I’m not on a quest to fix the world’s notation :-) .

The polarity story came after the additive/multiplicative terminology, I believe. At any rate the positive are \otimes and \oplus. Positives are basically inductive-limit-like things while negatives are like projective limits. The reason for the additive/multiplicative/exponential terminology is that the exponential act as a morphism between monoidal products of the respective kind, much like the exponential function between ordinary addition and multiplication (Girard seems to have a taste for elaborate punny names like this).

By the way, I really dislike calling the involutive thingy “negation” because it’s… not. So I call it “dualisation”. Call it my little quirk.

Posted by: Arnaud Spiwack on May 24, 2018 6:49 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

The word “correction” implies that you’re fixing something I said that was wrong, but the only thing I see that you said that contradicts anything I said is that I mistakenly wrote “times” instead of “tensor” as the pronunciation of \otimes. Can you explain further? Are you also saying I was wrong in my guess that Girard’s choice to match the notations /\otimes/\oplus and &/\&/\parr was related to polarity?

Regarding “with”, I tried it but couldn’t get used to it, and it clashed with other ways that I use the ordinary English word “with”.

I also find it a little odd to call the involution in an arbitrary *\ast-autonomous category “negation”. However, in linear constructive mathematics as inspired by the standard interpretation, the involution is unquestionably “negation”.

Posted by: Mike Shulman on May 24, 2018 7:01 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

The word “correction” implies that you’re fixing something I said that was wrong

I have to confess of using the opportunity of these correction to ramble opinions of my own, indeed.

Are you also saying I was wrong in my guess that Girard’s choice to match the notations \otimes/\oplus and &\&/\parr was related to polarity?

I did, but that’s only because I misread what you wrote, and understood that you were saying that additive and positive coincided.

However you didn’t.

Fortunately, my son goes to primary school, so I may just tag along tomorrow and learn how to read.

I’m pretty sure the notion of polarity is posterior to the notation, though. But probably some intuition was already there.

Posted by: Arnaud Spiwack on May 24, 2018 5:31 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

This is a really nice paper, and very clarifying. One thing that relates to it (and which it at least starts to clarify) is the lovely result (which I learned about from Greg Restall) from Dosen and Petrić that the logic of equality of deductions in propositional logic corresponds to multiplicative classical linear logic, in their paper Isomorphic formulae in classical propositional logic. Their approach seems to be something that can be understood via a Chu-construction.

Posted by: Gershom B on May 24, 2018 5:31 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

From the paper,

The Chu construction for Heyting algebras gives a precise way to translate between linear and intuitionistic propositional logic. However, to do substantial mathematics we require not just a propositional logic but a first-order and even higher-order logic.

Anyone following the HoTT buzz of the past few years might have come to think you should add

…and even homotopy type theory.

Imagine such a person, converted by the HoTT book to a constructive outlook, now encounters:

…once we have climbed from intuitionistic to linear logic using the Chu construction, we can kick away the ladder.

What to do? Look for the nearest ladder?

Since Heyting algebras are (0,1)(0, 1)-toposes, presumably we have infinity-Chu operating on (,1)(\infty, 1)-toposes to give us some form of *\ast-autonomous (,1)(\infty, 1)-category. Is that a good place to be?

With that intriguing linear logic-quantum physics connection (e.g., here), one might almost imagine we were being told something.

Posted by: David Corfield on May 25, 2018 9:34 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

However, to do substantial mathematics we require not just a propositional logic but a first-order and even higher-order logic.

Anyone following the HoTT buzz of the past few years might have come to think you should add

…and even homotopy type theory.

I suppose they might… but I think they’d be wrong. (-: There’s no sense in which “substantial” mathematics requires homotopy type theory. Most of mathematics works just fine at set-level and is indifferent to whether it’s formalized in ZFC or ETCS or HOL or set-level HoTT. Even homotopy theory and higher category theory can be done perfectly well in these foundations by simply defining higher categories in terms of sets, as is usually done outside of the small HoTT community.

I’m sure you know all this, but I don’t want any bystanders to get the wrong impression. I enjoy HoTT, but sometimes I also enjoy doing math that is unrelated to HoTT. Six years ago Andrej Bauer wrote about HoTT:

Do I think this is an exciting new development? Certainly! Will the Univalent foundations disrupt the monopoly of Set-theoretic foundations? I certainly hope so! Will it become the new monopoly? It must not!

That said, there is a bit of a nod towards dependent type theory in Remark 9.12 of the current paper. However, I’ve been unable to think of any interesting examples of “L-groupoids”. (Maybe some reader will!)

Posted by: Mike Shulman on May 25, 2018 2:51 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Hi Mike, thanks for the very interesting article. I gave a talk here at the Logic Colloquium in Udine this week about Gödel’s Dialectica interpretation and a few people pointed me to your article, mentioning that it seemed similar. Indeed, Valéria de Paiva wrote a few articles about a Dialectica interpretation of linear logic, and it’s indeed very similar to the Chu construction. In 2006 she wrote a note about the relation between these two constructions (http://www.tac.mta.ca/tac/volumes/17/7/17-07abs.html). If you are interested in how this also relates to realizability, see my 2007 paper on the realizability interpretation of classical linear logic (http://www.eecs.qmul.ac.uk/~pbo/papers/paper013.pdf). You will see that it’s essentially the same construction as the Dialectica (and Chu), only differing on the interpretation of the modalities (!A and ?A). I found this fascinating that realizability and Dialectica coincide on the pure fragment of linear logic, and only differ on the treatment of the exponentials.

Posted by: Paulo Oliva on July 28, 2018 9:57 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Yes, the Chu and Dialectica interpretations are indeed very similar; I myself recently wrote another paper exhibiting them both as a special case of a general polycategorical construction. However, as far as I can tell, the Dialectica construction is almost never semicartesian/affine, which seems to be a very important property of the specific Chu construction that I’m using for this application. There are some remarks about the Dialectica construction in 3.9 and 9.12 of the paper however.

Posted by: Mike Shulman on August 2, 2018 6:52 PM | Permalink | Reply to this

Post a New Comment