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

66 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

I wrote

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

I’m happy to report that this questionably-advised strategy has borne some fruit: an anonymous referee suggests (among other possibilities) “antithesis interpretation”. I like this: it doesn’t have any wrong connotations to me, and it incorporates the important idea that the linear negation (formal De Morgan dual, refutation) is the “direct opposite” of a statement, in contrast to the intuitionistic negation which is just a negative impossibility of proof. So unless I hear something much better before I finish revising the paper for publication, I’ll probably go with that.

Posted by: Mike Shulman on October 18, 2019 11:15 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Ah, so for example, if I'm discussing the convergence of an infinite series xx of real numbers, where the statement that xx converges (by the Cauchy criterion) is ϵ>0,N,m,nn,|x nx m|<ϵ, \forall\, \epsilon \gt 0,\; \exists\, N,\; \forall\, m, n \geq n,\; {|{x_n - x_m}|} \lt \epsilon , then the negation of this statement is ¬ϵ>0,N,m,nn,|x nx m|<ϵ, \neg \forall\, \epsilon \gt 0,\; \exists\, N,\; \forall\, m, n \geq n,\; {|{x_n - x_m}|} \lt \epsilon , which can't be simplified further; but the antithesis of the original statement is ϵ>0,N,m,nn,|x nx m|ϵ, \exists\, \epsilon \gt 0,\; \forall\, N,\; \exists\, m, n \geq n,\; {|{x_n - x_m}|} \geq \epsilon , which is what I really want.

Posted by: Toby Bartels on January 11, 2020 3:37 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Oh, and the pair of statements may be called a synthesis, to bring Hegel into it.

(By the way, some of the nns in my previous comment should be NNs, of course.)

Posted by: Toby Bartels on February 16, 2020 8:58 PM | 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

Re: Linear Logic for Constructive Mathematics

I'm kind of late here, but I want to record this for when I look back here later:

A classical sentence of the form Cx:A,P[x]\forall^C\, x\colon A,\; P[x] is naturally interpreted linearly (or affinely) as Lx:A,P[x]\forall^L\, x\colon A,\; P[x], which is proved intuitionistically as Ix:A,P +[x]\forall^I\, x\colon A,\; P^+[x] and refuted intuitionistically as Ix:A,P [x]\exists^I\, x\colon A,\; P^-[x]. Similarly, Cx:A,P[x]\exists^C\, x\colon A,\; P[x] is interpreted as Lx:A,P[x]\exists^L\, x\colon A,\; P[x], which is proved as Ix:A,P +[x]\exists^I\, x\colon A,\; P^+[x] and refuted as Ix:A,P [x]\forall^I\, x\colon A,\; P^-[x]. But in practice, a lot of types (like AA here) are really subtypes, and we're looking at classical statements like Cx:B,Q[x] CP[x]\forall^C\, x\colon B,\; Q[x] \rightarrow^C P[x] or Cx:B,Q[x] CP[x]\exists^C\, x\colon B,\; Q[x] \wedge^C P[x].

These each have two linear interpretations. The simpler is as Lx:B,Q[x] LP[x]\forall^L\, x\colon B,\; Q[x]^{\bot} \vee^L P[x], which is proved as Ix:B,Q [x] IP +[x]\forall^I\, x\colon B,\; Q^-[x] \vee^I P^+[x] and refuted as Ix:B,Q +[x]P [x]\exists^I\, x\colon B,\; Q^+[x] \wedge P^-[x]. This seems like an unreasonably strong thing to have to prove, but it might work well if QQ is a closed statement (like a weak inequality) and PP is open (like a strict inequality), so that there's likely a bit of overlap between Q Q^- (which is open) and P +P^+ (also open). Similarly, Lx:B,Q[x] LP[x]\exists^L\, x\colon B,\; Q[x] \wedge^L P[x] is proved as Ix:B,Q +[x] IP +[x]\exists^I\, x\colon B,\; Q^+[x] \wedge^I P^+[x] and refuted as Ix:B,Q [x] IP [x]\forall^I\, x\colon B,\; Q^-[x] \vee^I P^-[x]. Now it's the refutation that might be too strong to go through, and it's most likely to work if QQ and PP are both closed.

But there's another linear interpretation, which is Lx:B,Q[x] P[x]\forall^L\, x\colon B,\; Q[x]^\bot \parr P[x] (or Lx:B,Q[x]P[x]\forall^L\, x\colon B,\; Q[x] \multimap P[x]), which is proved as Ix:B,(Q +[x] IP +[x]) IQ [x] IP [x]\forall^I\, x\colon B,\; (Q^+[x] \rightarrow^I P^+[x]) \wedge^I Q^-[x] \rightarrow^I P^-[x] and refuted as Ix:B,Q +[x] IP [x]\exists^I\, x\colon B,\; Q^+[x] \wedge^I P^-[x]. Similarly, Lx:B,Q[x]P[x]\exists^L\, x\colon B,\; Q[x] \otimes P[x] is proved as Ix:B,Q +[x] IP +[x]\exists^I\, x\colon B,\; Q^+[x] \wedge^I P^+[x] and refuted as Ix:B,(Q +[x] IP [x]) IP +[x] IQ [x]\forall^I\, x\colon B,\; (Q^+[x] \rightarrow^I P^-[x]) \wedge^I P^+[x] \rightarrow^I Q^-[x]. In both cases, instead of having to prove an intuitionistic disjunction, this has been replaced by an easier (but more complicated) goal.

So if AA is classically defined as {x:B|Q[x]}\{x\colon B \;|\; Q[x]\}, then there's actually two things that quantification over AA could mean, just as a statement with C\wedge^C or C\vee^C in it could mean two different things. And that's assuming that BB was straightforward. Mike said above (and the full paper seems to agree) that the quantifiers are straightforward, acting like L\wedge^L and L\vee^L (the simple ones), but it seems to me that at best this depends on the nature of the domain of quantification.

This reminds me of Abstract Stone Duality, Paul Taylor's logic for doing topology (at least in locally compact spaces). This allows universal quantification only over a compact domain and existential quantification only over an overt domain. If we assume that BB is already compact, then AA is compact if QQ is closed, and then AA can use the simple interpretation of universal quantification. On the other hand, if BB is already overt, then AA is overt if QQ is open, and this never appeared above. But actually that fits, because the way the logical connectives are written in ASD assumes that one is only ever proving things, never refuting them. You can speak of refutations in ASD, but that's done by dualizing the interpretation of the proposition. (In particular, there is no negation of propositions in ASD, involutory or otherwise, so one cannot speak of refuting a proposition by proving its negation.) Indeed, the statements to be proved in ASD are always open statements, meaning that the statements to be refuted are always closed ones, and this at least agrees with the characteristics of PP that help with the simpler linear interpretation. As for QQ, if you're refuting an existential quantification, then that's really proving a universal quantification, so we still want a compact domain, and so we still want QQ to be closed. (The overtness requirement for existential quantification then seems superfluous, which is fair enough, since overtness is trivial anyway in any topology that's either classical or pointwise; only intuitionistic pointless topology can see it, and that's pretty far out there.)

Anyway, if I assume for the sake of argument that universal quantification is straightforward over a compact domain, then it may not be straightforward over the set of natural numbers, which is not compact. However, the natural numbers form a nice (open) subspace of the compact space ¯\overline{\mathbb{N}} of extended natural numbers. So if I see Cn:,P[n]\forall^C\, n\colon \mathbb{N},\; P[n] (or equivalently Cn:¯,(n) cP[n]\forall^C\, n\colon \overline{\mathbb{N}},\; (n \ne \infty) \rightarrow^c P[n]), then I might interpret this as Ln:¯,(n= L) LP[n]\forall^L n\colon \overline{\mathbb{N}},\; (n =^L \infty) \vee^L P[n], which is proved as In:¯,(n= I) IP +[n]\forall^I\, n\colon \overline{\mathbb{N}},\; (n =^I \infty) \vee^I P^+[n] and refuted as In:¯,(n#) IP [n]\exists^I\, n\colon \overline{\mathbb{N}},\; (n \# \infty) \wedge^I P^-[n]. But there's generally no way to decide whether an extended natural number is finite or infinite, so unless n:¯,P[n]\forall\, n\colon \overline{\mathbb{N}},\; P[n] holds, we can't reasonably expect to ever prove this. A similar thing holds for existential quantification, except that it's now the refutation that's unreasonably difficult.

So instead, I should interpret it as Ln:¯,(n= L)P[x]\forall^L n\colon \overline{\mathbb{N}},\; (n =^L \infty) \parr P[x], which is proved as In:¯,((n#)P +[n]) IP [n]n=\forall^I\, n\colon \overline{\mathbb{N}},\; ((n \# \infty) \rightarrow P^+[n]) \wedge^I P^-[n] \rightarrow n = \infty and still refuted as In:¯,(n#) IP [n]\exists^I\, n\colon \overline{\mathbb{N}},\; (n \# \infty) \wedge^I P^-[n]. These simplify to In:,P +[n]\forall^I\, n\colon \mathbb{N},\; P^+[n] and In:,P [n]\exists^I\, n\colon \mathbb{N},\; P^-[n], although the simplification for the statement to be proved only works because \mathbb{N} is open in ¯\overline{\mathbb{N}} (so that once P +P^+ has been proved for each finite number, P [n]P^-[n] implies that nn is not finite, and because \mathbb{N} is open, this means that nn is infinite). This rather undercuts my idea that quantification is simple for compact spaces, since here it's simple because \mathbb{N} is open and not compact. (Existential quantification works similarly.)

On the other hand, if I want to consider P[]P[\infty], and for some reason I want to phrase this as either Cn:¯,(n=) CP[n]\forall^C\, n\colon \overline{\mathbb{N}},\; (n = \infty) \rightarrow^C P[n] or Cn:¯,(n=) CP[n]\exists^C\, n\colon \overline{\mathbb{N}},\; (n = \infty) \wedge^C P[n], then it's a little more complicated. By the simple interpretation, the first of these is proved as In:¯,(n#) IP +[n]\forall^I\, n\colon \overline{\mathbb{N}},\; (n \# \infty) \vee^I P^+[n], which is still unreasonably strong (and definitely stronger than P +[]P^+[\infty]), while the refutation of the second is similar. Then under the more complicated interpretation, the first classical statement is proved as In:¯,((n=)P +[n]) IP [n]n#\forall^I\, n\colon \overline{\mathbb{N}},\; ((n = \infty) \rightarrow P^+[n]) \wedge^I P^-[n] \rightarrow n \# \infty, which is still stronger than P +[]P^+[\infty], although at least something that one could reasonably hope to prove. And as long as P P^- is #\#-open, then it is equivalent to P[]P[\infty].

So subtyping works as expected if the subtype is defined by an open proposition or if the subtype is given by an equation involving the variable and the predicate is given by a subset of a strong set. And the whole argument works in general, not just for the example of \mathbb{N} and {}\{\infty\} as subtypes of ¯\overline{\mathbb{N}}. That is, if A{x:B|Q[x]}A \coloneqq \{x\colon B \;|\; Q[x]\} and QQ is an open proposition, then Lx:A,P[x]\forall^L\, x\colon A,\; P[x] is equivalent to Lx:B,Q[x]P[x]\forall^L\, x\colon B,\; Q[x] \multimap P[x], and Lx:A,P[x]\exists^L\, x\colon A,\; P[x] is equivalent to Lx:B,Q[x]P[x]\exists^L\, x\colon B,\; Q[x] \otimes P[x]. And also, if A{x:B|x=f[x]}A \coloneqq \{x\colon B \;|\; x = f[x]\}, where BB is a strong set, and SS is a strong subset of BB (an element of the L-power set PBP{B}), then Lx:A,xS\forall^L\, x\colon A,\; x \in S is equivalent to Lx:B,(x= Lf[x])xS\forall^L\, x\colon B,\; (x =^L f[x]) \multimap x \in S, and Lx:A,xS\exists^L\, x\colon A,\; x \in S is equivalent to Lx:B,(x= Lf[x])xS\exists^L\, x\colon B,\; (x =^L f[x]) \otimes x \in S. There are probably some other general situations in which this works, but it doesn't work generally.

I suppose that I had better say exactly what I mean by an open or closed proposition. This is folklore in constructive mathematics, where the typical examples are (respectively) a strict inequality or a weak inequality of real numbers. In ASD, it has some formalization, as everything to be proved is open (and everything to be refuted is closed), and this is reflected in the interpretation of ASD in locally compact spaces, where all types are topological spaces (or locales) and all propositions are open subspaces (or their dual closed subspaces if refuted). But in Mike's affine-logic formulation of constructive mathematics, it has a precise meaning in which they appear on equal footing (and a given proposition might well be neither or both): PP is open if P ¬P +P^- \equiv \neg{P^+} and closed if P +¬P P^+ \equiv \neg{P^-}. It is with this definition that the metatheorem in the previous paragraph holds.

Posted by: Toby Bartels on September 2, 2018 11:13 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Thanks for this very detailed comment!

I think whether or not quantification is straightforward depends on your perspective on what counts as “quantification”. (-: The perspective I took here and in the paper is that quantified variables always range over a set, not a subset, and that when QQ is a subset of AA, quantified implications like x A.Q(x)P(x)\forall x^A. Q(x) \to P(x) should be regarded as quantified implications (and dually for existentials), rather than as “quantifiers over QQ”. The fact that you have to choose whether to interpret them additively or multiplicatively confirms in my mind that the implication (or whatever it is) should be notated and thought of as a separate connective from the quantifier.

You’re absolutely right that whatever we call the latter, they are less straightforward. They do appear in the paper, for instance in the definition of neighborhoods in a metric space in examples 10.3 and 10.16, where a “quantifier over an open ball” gets interpreted intuitionistically as both a statement and its formal converse. My experience is that almost always one wants the multiplicative version, although there are some exceptions — for instance, the notion of “discrete field” (Definition 7.10 and following) arises by interpreting “every nonzero element is invertible” additively.

The notions of open and closed proposition do also appear in the paper, under the names “affirmative” and “refutative”. It didn’t occur to me to call them “open” and “closed”, although I suppose it should have. I think I’ll stick with “affirmative” and “refutative”, though, since “open” and “closed” would get confusing once we start actually doing topology as in section 10.

Posted by: Mike Shulman on September 2, 2018 11:44 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Sure, every quantification occurs over a set. But every subset defines a set (its tabulation); and in both classical and constructive mathematics, quantification over a subset's tabulation is equivalent to quantification (over the ambient set) guarded by the subset. In affine mathematics, it's not … unless membership in the subset is affirmative.

And yeah, that's the only case, because the other metatheorem that I stated, about quantifying membership in an L-subset guarded by an equation doesn't work as stated. It works for universal quantification when the apartness relation is tight, but it still doesn't work for existential quantification, not even in the motivating example (so that's wrong too), unless P +P^+ is also #\#-open, which being an L-subset-membership predicate doesn't do. In the end, while some theorem could be stated here, I don't think that this is worth salvaging.

Posted by: Toby Bartels on September 3, 2018 6:14 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

in both classical and constructive mathematics, quantification over a subset’s tabulation is equivalent to quantification (over the ambient set) guarded by the subset. In affine mathematics, it’s not

Right! The passage from a subset to its tabulation loses information, in a way that doesn’t happen classically or intuitionistically. It forgets about what it means to not belong to a subset, and when you guard a quantification by a subset you have to say something about the elements not in the subset too, whereas when you quantify over the tabulation you don’t.

At least this is the case in the particular affine higher-order logic that I’m using here, where the existence predicate of a set must be affirmative. I could imagine someone making a different choice in this regard, but I’m not sure exactly what the resulting theory would look like.

Posted by: Mike Shulman on September 3, 2018 6:44 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Yes, of course! I spent a lot of trouble figuring out that quantification over subsets works the most smoothly when the subset is given by an affirmative predicate, when this is naturally just because all sets are defined by (in part) an affirmative existence predicate.

Speaking of these existence predicates, how come I'd never seen it suggested before, in connection with Bishop's concept of sets, that sets are not just quotients of types but subquotients? (In the terminology of your paper, sets are quotients of presets, while presets are subobjects of types.) For one thing, this really clears up why the axiom of choice really feels as if it ought to apply to the free set on a given preset (in the sense that each such set is projective), but if every set is a quotient of a projective set, then this a substantive set-theoretic axiom (the presentation axiom) with important consequences (such as the axiom of countable dependent choice) that really ought to be optional. But now it seems easy: the free set on the cofree preset on a given type may be a choice set, but that just makes every set a subquotient of a projective set, which still says something, but perhaps not something important.

Posted by: Toby Bartels on September 3, 2018 7:36 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

how come I’d never seen it suggested before, in connection with Bishop’s concept of sets, that sets are not just quotients of types but subquotients?

I’m not sure. Maybe because Bishop sets are often formalized as setoids in Martin-Lof type theory, in which case you can build the existence predicate into the underlying type using a Σ\Sigma? And relatedly that many naturally-occurring triposes have comprehension, so that a similar thing can be done there?

this really clears up why the axiom of choice really feels as if it ought to apply to the free set on a given preset (in the sense that each such set is projective), but if every set is a quotient of a projective set, then this a substantive set-theoretic axiom

I don’t really follow this. I don’t think I share your feeling that AC ought to apply to the free set on the cofree preset on a type, but if I take that as given then I don’t see why it would apply any less to the free set on any preset on that type. If the argument is that all “existence” should be witnessed by an “operation” that it may not be a function in general, then since operations between presets are just operations between their underlying types that respect existence, why wouldn’t the witnessing operation that’s a function in the first place also be a function in the second place, since we’re only adding an extra condition on the domain elements?

Posted by: Mike Shulman on September 3, 2018 7:57 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Maybe because Bishop sets are often formalized as setoids in Martin-Lof type theory, in which case you can build the existence predicate into the underlying type using a Σ\Sigma?

That's certainly why you can get away with ignoring existence predicates, but I still think that philosophically somebody might have thought of it before. (Like maybe I should have thought of it before.)

If the argument is that all “existence” should be witnessed by an “operation” that it may not be a function in general, then since operations between presets are just operations between their underlying types that respect existence, why wouldn’t the witnessing operation that’s a function in the first place also be a function in the second place, since we’re only adding an extra condition on the domain elements?

The reason is the same reason that a subset SS of the free set on a type (even when types are the same as presets, so constructed as a quotient of a sum type) need not be projective, which is that the proof that a relation from that subset is entire might make use, in constructing the yy that any given xx is related to, of the proof that xx belongs to the subset. So here, where types are not the same as presets but presets are constructed directly as subobjects of types, the proof that a prerelation from that preset is entire might also make use, in constructing the yy that any given xx is related to, of the proof that xx exists. Thus identicial elements of the preset might be mapped (by the proof) to non-identical elements of the target preset, making the prefunction not extensional on identity, so not a function even when equality is defined to be identity (assuming that the type supports this).

However, thinking about whether a subset of a projective set must be projective has soured me on the whole idea that this a breakthrough in the formalization of Bishop sets. Using Excluded Middle (but no stronger form of Choice), a subset of a projective set does need to be projective, because any entire relation from SS can be extended to an entire relation from PP (say by saying that xx is related to everything[^1] if x PSx \notin_P S), which contains a function from PP, which restricts to a function from SS. So one still cannot adopt this formalization of Bishop sets as a neutral foundation of mathematics, because EMCCEM \rightarrow CC should not be a theorem.

[^1]: This only works if the relation's target TT is inhabited, but we use excluded middle again and note that TT empty makes SS empty, and we already know that \varnothing is projective.

(Incidentally, this is the same theorem that soured me on my own Bishop-set–based foundation of mathematics, which kept presets identified with types but broke the argument by allowing only identity judgements, not identity types. Since my approach was still propositions-as-types, having universal quantification still obliged me to have types of operations, making my foundation impredicative given a type of truth values, which exists if EM holds. And impredicativity allows identity types to be defined by Leibniz's definition, or equivalently as the conjunction of all equivalence predicates. So I also had EMCCEM \rightarrow CC.)

Posted by: Toby Bartels on September 4, 2018 7:38 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

the proof that a relation from that subset is entire might make use, in constructing the yy that any given xx is related to, of the proof that xx belongs to the subset.

Oh, of course.

So one still cannot adopt this formalization of Bishop sets as a neutral foundation of mathematics

I would be inclined to point the finger rather at the presumption that AC should apply to the cofree preset on a type. This is the part of your argument that breaks in a general tripos, for instance.

Posted by: Mike Shulman on September 4, 2018 7:57 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

I would be inclined to point the finger rather at the presumption that AC should apply to the cofree preset on a type.

OK, but then you can't use propositions as types, since this doesn't distinguish \forall \exists from \prod \sum. And obviously you don't need to use type theory this way —HoTT's treatment of the distinction between \exists and \sum takes care of the problem nicely—, but it has a long pedigree, and it mirrors Bishop's informal argument for Countable Choice in Constructive Analysis. So it would have been interesting if this subtle change could have made a difference.

It doesn't, so never mind.

Posted by: Toby Bartels on September 4, 2018 11:45 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

By the way, here's another thing that's blowing my mind about this paper: Everyone always says that the classical mathematician's disjunction is ¬¬(PQ)=¬(¬P¬Q)=P¬¬Q=¬¬PQ\neg\neg(P \vee Q) = \neg(\neg{P} \wedge \neg{Q}) = P \rightarrow \neg\neg{Q} = \neg\neg{P} \leftarrow Q, which (being a negation) has ‘no constructive content’, and sometimes I suppose that it is; but you point out that the default meaning should be PQ(¬PQ)(P¬Q)P \parr Q \coloneqq (\neg{P} \rightarrow Q) \wedge (P \leftarrow \neg{Q}), which is not a negation and so does have constructive content. (Of course, it's always even better if it can mean PQP \vee Q, but the only reason that we worry about the issue at all is that this doesn't always work; still, it has its place in your paper too, usually with the adjective ‘strong’.)

In fact, I expect that when doing constructive mathematics in the future, even if I'm not trying to derive it from linear logic with your method, I'll probably think of PQP \parr Q often. It's a nice operation; like the double-negation version, it's associative; unlike the double-negation operation, it also has an identity (\bot, just like you'd expect).

It also makes me wonder how useful the noncommutative versions ¬PQ\neg{P} \rightarrow Q (that is, unless PP then QQ) and P¬QP \leftarrow \neg{Q} (that is, PP unless QQ) might be. (These are still associative, but they only have identities on one side each.)

Here is a Hasse diagram of all of these:

¬(¬P¬Q) / \ ¬PQ P¬Q \ / PQ | PQ \array { & & \neg(\neg{P} \wedge \neg{Q}) \\ & / & & \backslash \\ \neg{P} \rightarrow Q & & & & P \leftarrow \neg{Q} \\ & \backslash & & / \\ & & P \parr Q \\ & & | \\ & & P \vee Q }

Every one of these has ¬P¬Q\neg{P} \wedge \neg{Q} as its negation.

Posted by: Toby Bartels on September 6, 2018 12:56 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

I’m pleased you find it mind-blowing; I was pretty surprised myself when I realized this.

Of course, when you write PQ(¬PQ)(P¬Q)P \parr Q \equiv (\neg P \to Q) \wedge (P \leftarrow \neg Q), you’re implicitly regarding the intuitionistic propositions P,QP,Q as affirmative/open affine propositions and then taking the “proof” part of the affine proposition PQP\parr Q. The “refutation” part of this affine proposition is ¬P¬Q\neg P \wedge \neg Q, and the fact that as you say ¬P¬Q\neg P \wedge \neg Q is the intuitionistic negation of (¬PQ)(P¬Q)(\neg P \to Q) \wedge (P \leftarrow \neg Q) means that the affine \parr in the standard interpretation preserves affirmative propositions. I didn’t notice this before!

Let me quickly write out a proof, to make sure nothing snuck past us. It’s clear that if ¬P¬Q\neg P \wedge \neg Q then ¬((¬PQ)(P¬Q))\neg ((\neg P \to Q) \wedge (P \leftarrow \neg Q)), in fact we can already derive a contradiction from ¬P¬Q\neg P \wedge \neg Q and ¬PQ\neg P \to Q. (This is just the compatibility condition saying that PQP\parr Q is indeed an affine proposition in the standard interpretation.) The less obvious part is that if ¬((¬PQ)(P¬Q))\neg ((\neg P \to Q) \wedge (P \leftarrow \neg Q)) then ¬P\neg P (and also ¬Q\neg Q by symmetry). But to show this, it suffices to show that if PP then (¬PQ)(P¬Q)(\neg P \to Q) \wedge (P \leftarrow \neg Q). Now on the one hand, if PP holds then ¬P\neg P is false and hence implies anything (such as QQ), while on the other hand if PP holds then it is implied by anything (such as ¬Q\neg Q).

The reason I find this surprising is that it’s not generally true in affine logic. The affirmative propositions are a coreflective sub-poset, which means they are closed under colimits such as \vee. Moreover, the coreflector !! is strongly monoidal (this is a law of affine logic), which implies that the sub-poset is closed under the tensor product \otimes. It is not closed under the affine additive conjunction \wedge: the refutations of PQP\wedge Q are the intuitionistic ¬P¬Q\neg P \vee \neg Q, which is stronger than ¬(PQ)\neg (P\wedge Q). So I wouldn’t have expected it to be closed under the dual \parr of \otimes either, and I’m sure that in general affine logic it is not; but this shows that in the special case of the standard interpretation, it is.

While I didn’t notice this particular fact before, I did notice several other special laws that hold in the standard interpretation but not in general affine logic, and listed some of them towards the end of section 3 of the paper. For instance, the fact that intuitionistic logic satisfies both distributive laws means that the standard interpretation satisfies the “purely additive” distributive law P(QR)(PQ)(PR)P \wedge (Q\vee R) \equiv (P \wedge Q) \vee (P\wedge R) and its dual, whereas in general affine logic one only has the mixed multiplicative/additive distributive law P(QR)(PQ)(PR)P\otimes (Q\vee R) \equiv (P\otimes Q) \vee (P\otimes R). Another interesting one is that the modality !! preserves \vee and \exists; this property doesn’t seem to have been considered before in linear/affine logic.

I wonder whether one can characterize somehow the additional logical laws that hold in the affine logic of a standard interpretation.

Posted by: Mike Shulman on September 6, 2018 5:15 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Of course, when you write PQ(¬PQ)(P¬Q)P \parr Q \equiv (\neg P \to Q) \wedge (P \leftarrow \neg Q), you’re implicitly regarding the intuitionistic propositions P,QP,Q as affirmative/open affine propositions and then taking the “proof” part of the affine proposition PQP\parr Q.

Right, but that's the default; we do the same thing when we write ¬PP\neg{P} \equiv P \to \bot. (Although we use a different symbol in that case.)

But even when the propositions aren't affirmative, it's easier to think of the correct interpretation of \parr as a modification of this default \parr rather than as a modifiction of \vee, at least for me. For example, today I taught my remedial Algebra students that a=0a = 0 or b=0b = 0 if ab=0a b = 0. I always feel a twinge of guilt when I do this, because I try to teach my students useful, practical knowledge, and nonconstructive reasoning is impractical, at least when precision is required. (Although at this stage, they're really working in the field of rational numbers, and most of these students will never go beyond the real algebraic numbers[^1], maybe with π\pi adjoined, and that's a discrete field. It's in the Calculus classes where I really point out when things are nonconstructive and at least gesture towards how one can deal with this in practice.)

[^1]: actually, the real radical numbers; that is, they'll never deal with the roots of nonsolvable polynomials such as x 5+2x+1x^5 + 2 x + 1

But if I interpret ‘or’ as \parr, then it's much more believable. Sure, a,b:,ab=0a=0b=0\forall\, a, b\colon \mathbb{R},\; a b = 0 \;\Rightarrow\; a = 0 \;\parr\; b = 0 is not strictly correct as a theorem in constructive mathematics (without accepting Markov's Rule). But neither is a:,¬a=0|a|>0\forall\, a\colon \mathbb{R},\; \neg\; a = 0 \;\Rightarrow\; {|a|} \gt 0, yet I wouldn't mind saying ‘The absolute value of aa is positive if aa is nonzero.’ (nor be surprised to hear a constructivist say it), because we're used to fudging the meaning of symbols like \ne and words like ‘nonzero’. (The purists will use #\# and ‘apart from zero’, but I'm not this much of a purist in ordinary language.)

In fact, much of your paper is just formalizing the intuition behind such fudging. The idea that instead of dealing with a negation directly, you take the de Morgan dual of everything, reinterpret ¬=\neg{=} as #\#, and so on, then see what you can do with that statement instead, is old hat. But the idea that, when you do this to a conjunction, you may end up with a \parr-like statement instead of an \vee-like statement is fairly new to me. And indeed, when I dualize ‘ab0a b \ne 0 if a0a \ne 0 and b0b \ne 0’, I can't get any correct statement involving \vee, but ‘a=0a = 0 or b=0b = 0 if ab=0a b = 0’ is correct as long as ‘or’ is understood to be a fudged \parr. (In practice, if I were writing a work of constructive mathematics, I'd probably say ‘a=0a = 0 if b0b \ne 0, and conversely’, but from now on, I'll be thinking \parr.)

I'm now trying to find a way to pronounce \parr other than ‘par’. If not a word, I'd be happy with a short phrase such as ‘if and only if’. Indeed, ‘if not’ (or ‘unless’) captures half of it, and ‘or else’ captures the other half, but neither ‘unless and or else’ nor the reverse seems to work grammatically.

Posted by: Toby Bartels on September 6, 2018 9:26 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Yes, I agree with all of that.

I don’t mind “par” myself; at least it’s unambiguous. But I could get used to “unless and or else” too; in principle it doesn’t seem different grammatically from “if and only if” where the conjunction “and” combines two other conjunctions (in the grammatical) sense) “if” and “only if”, or “unless” and “or else”.

Posted by: Mike Shulman on September 6, 2018 9:44 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

But I could get used to “unless and or else” too; in principle it doesn’t seem different grammatically from “if and only if” where the conjunction “and” combines two other conjunctions (in the grammatical [fixed link ―Toby] sense) “if” and “only if”, or “unless” and “or else”.

I think that it works for me because ‘if’ and ‘only if’ are subordinating conjunctions being joined by the coordinating conjunction ‘and’, which seems at a higher level; while ‘or else’ is also coordinating. Or maybe the problem is that ‘or else’ and ‘unless’ aren't the same kind, since ‘unless’ is still subordinating. In any case, it doesn't feel the same.

A subordinating conjunction introduces a dependent clause, and I feel like I can combine two of those by ‘and’ (even though ordinary language doesn't do this), just as I can combine two independent clauses or two prepositional phrases that way. But in ‘PP unless and or else QQ’, I'm simultaneously trying to subordinate QQ to PP and to coordinate them at an equal level, and then coordinate the results!

Posted by: Toby Bartels on September 6, 2018 11:07 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Maybe my understanding of grammar has been ruined by my understanding of mathematics, but I don’t feel any difference between “subordinating” and “coordinating” conjunctions. “If-then” and “unless” and “or else” are all just binary logical connectives, there’s no logical reason to denigrate one of their arguments as “subordinate” to the other, especially since (in classical logic) they are all interdefinable by sticking in some negations.

Posted by: Mike Shulman on September 6, 2018 11:12 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

The theory is that a dependent clause (introduced by a subordinating conjunction) is a modifier to the main sentence, while an independent clause (joined to the other independent clause by a coordinating conjunction) stands on its own. This is about emphasis, not denotation.

A practical consequence is that a dependent clause can be moved to the beginning of the sentence, taking its conjunction with it, remaining separated from the main clause by a comma. Since the most commonly used coordinating conjunctions are denotationally symmetric, you can rearrange independent clauses too, but the conjunction ends up between them, not in front of the same clause that it used to be in front of.

  • ‘I will take my umbrella unless the sun is out.’ → ‘Unless the sun is out, I will take my umbrella.’ (exactly the same except for a slight shift of emphasis)
  • ‘I will take my umbrella unless the sun is out.’ → ‘The sun is out, unless I will take my umbrella.’ (denotationally the same in classical logic, but not in intuitionistic logic, which is related the major shift in emphasis; these are not the same sentence at all)
  • ‘I will take my umbrella, or the sun is out.’ → ‘The sun is out, or I will take my umbrella.’ (the same meaning, except for a slight shift of emphasis, because of symmetry)
  • ‘I will take my umbrella, or else the sun is out.’ → ‘The sun is out, or else I will take my umbrella.’ (denotationally the same in classical logic, but not in intuitionistic logic, due to the asymmetry; not really the same sentence either, because ‘else’ isn't part of the conjunction)
Posted by: Toby Bartels on September 7, 2018 10:06 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Yeah, I recognize that a distinction is made in grammar, but since it only has to do with emphasis and with rules of syntax about the placement of words, it doesn’t feel to me as though it actually means anything. So it doesn’t impact my willingness to say “unless and or else”.

Posted by: Mike Shulman on September 7, 2018 10:19 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

What about “unless and otherwise”?

Posted by: Mike Shulman on September 10, 2018 8:18 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

That's not even a conjunction; that's an adverb! It's not ‘I will take my umbrella, otherwise the sun is out.’; it's ‘I will take my umbrella; otherwise, the sun is out.’. (And interpreted strictly, this has the same denotation as ‘I will take my umbrella.’; to get the desired meaning, it should be something like ‘I may take my umbrella; otherwise, the sun is out.’, with the first clause not claiming anything but providing the context needed to interpret the second clause. Or of course, write ‘I will take my umbrella, or otherwise, the sun is out.’, but now it's no different from ‘or else’, except that people are more likely to use the comma after a long word like ‘otherwise’.)

Posted by: Toby Bartels on September 11, 2018 12:03 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

I don’t know why we should be so finicky about the way words are used in English when we take them to give them a new mathematical meaning. I’m perfectly happy with “par” myself, but I was trying to help you out in finding a more descriptive phrase.

Posted by: Mike Shulman on September 11, 2018 9:20 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Well, ‘par’ is what I've been saying to myself when thinking about it lately, especially since nothing else works. I'd like to have a way to say it that fits in with preexisting natural language (which I think that ‘if and only if’ does), but we haven't found one. Or at any rate, we've found some that sound fine to you, but they don't work for me.

A similar situation exists with ‘xor’. (In certain contexts, ‘or’ can naturally mean the same as ‘xor’ (much as ‘if’ can naturally mean the same as ‘if and only if’); however, the default meaning or ‘or’ is inclusive.) If we played fast and loose with English grammar, then we could say ‘or but not and’ (a counterpoint to the legalese ‘and/or’), but it never occurred to me until today to do that. We can tag ‘but not both’ on to the end, and I'll do that sometimes, but the only phrase that really works as an infixed connective is ‘xor’, and that's what I say to myself. (For that matter, I say ‘iff’ to myself rather than ‘if and only if’: more jargon.)

So I'm rejecting these phrases as non-jargon terms because the grammar sounds wrong, not because I can't learn to use them as jargon. But as you noted, we already have the jargon term ‘par’, so I probably won't use the other phrases at all.

Posted by: Toby Bartels on September 11, 2018 7:00 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

By the way, if we are working inside linear logic, then instead of “par” we can simply say “unless”. “Unless” (P¬QP \leftarrow \neg Q) doesn’t even sound like a symmetric connective, but in linear logic it is equivalent to “par” (and in classical logic it is equivalent to “or”).

Posted by: Mike Shulman on February 18, 2019 2:43 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

By the way, the relation between affirmativity and openness does appear in Remark 3.6 of the paper, which compares this notion of affirmativity to that used by Vickers to motivate constructive/geometric logic. However, it’s worth noting that there are plenty of naturally occurring topologies in which the topological notion of “open” is quite different from the logical one of affirmativity, such as the cut-metric space defined by the Hausdorff distance (Theorem 9.11 and Example 10.22).

Posted by: Mike Shulman on September 3, 2018 4:55 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

I've been thinking about multiplicative quantification, and I think that this should exist. I don't know how to handle it in linear logic itself (where proving a multiplicatively existential statement, as well as using or refuting a multiplicatively universal statement, would seem to require an infinite proof if quantified over an infinite set), but I seem to know how to interpret it (both proof and refutation) in intuitionistic logic under the standard interpretation.

Specifically, the proof of xAP[x]\bigotimes_{x \in A} P[x] is xAP +[x]\forall_{x \in A} P^+[x], while the refutation of xAP[x]\parr_{x \in A} P[x] is xAP [x]\forall_{x \in A} P^-[x]; those are easy. And then the proof of xAP[x]\parr_{x \in A} P[x] is ( xA) xA( yA(yx)P [y])P +[x](\exists_{x \in A} \top) \wedge \forall_{x \in A} (\forall_{y \in A} (y \ne x) \Rightarrow P^-[y]) \Rightarrow P^+[x], while the refutation of xAP[x]\bigotimes_{x \in A} P[x] is ( xA) xA( yA(yx)P +[y])P [x](\exists_{x \in A} \top) \wedge \forall_{x \in A} (\forall_{y \in A} (y \ne x) \Rightarrow P^+[y]) \Rightarrow P^-[x]. (The existential bit at the beginning is annoying, but it's necessary so that existential quantification over the empty set is false rather than true.) Note that AA needs to be an L-set here, so that we know what yxy \ne x means.

If AA is of the form [n]{k|k<n}[n] \coloneqq \{k \in \mathbb{N} \;|\; k \lt n\} (where {0,1,2,}\mathbb{N} \coloneqq \{0, 1, 2, \ldots\}), then x[n]P[x]\bigotimes_{x \in [n]} P[x] is equivalent (in the sense of having the same proof and refutation) to P[0]P[1]P[n1]P[0] \otimes P[1] \otimes \cdots \otimes P[n-1], and x[n]P[x]\parr_{x \in [n]} P[x] is equivalent to P[0]P[1]P[n1]P[0] \parr P[1] \parr \cdots \parr P[n-1]. So quantification over a finite set reduces to conjunction or disjunction as it should, suggesting that it is an appropriate notion of quantification. And in the classical case, the formula certainly works, despite being a bit roundabout for that.

Posted by: Toby Bartels on September 11, 2018 10:44 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

That looks kind of ad hoc, especially the existential out in front. Are there any particular non-finite examples you’re trying to capture?

Posted by: Mike Shulman on September 12, 2018 2:10 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

The existential out front does seem weird, but the rest was straightforward once I saw the pattern for finite cases:

  1. P 0 +P_0^+;
  2. (P 0 P 1 +)(P 1 P 0 +)(P_0^- \Rightarrow P_1^+) \wedge (P_1^- \Rightarrow P_0^+);
  3. (P 0 P 1 P 2 +)(P 0 P 2 P 1 +)(P 1 P 2 P 0 +)(P_0^- \Rightarrow P_1^- \Rightarrow P_2^+) \wedge (P_0^- \Rightarrow P_2^- \Rightarrow P_1^+) \wedge (P_1^- \Rightarrow P_2^- \Rightarrow P_0^+);
  4. P 0 P 1 P 2 P 3 +)(P 0 P 1 P 3 P 2 +)(P 0 P 2 P 3 P 1 +)(P 1 P 2 P 3 P 0 +)P_0^- \Rightarrow P_1^- \Rightarrow P_2^- \Rightarrow P_3^+) \wedge (P_0^- \Rightarrow P_1^- \Rightarrow P_3^- \Rightarrow P_2^+) \wedge (P_0^- \Rightarrow P_2^- \Rightarrow P_3^- \Rightarrow P_1^+) \wedge (P_1^- \Rightarrow P_2^- \Rightarrow P_3^- \Rightarrow P_0^+);
  5. etc.

That is, for each statement, if all of the other statements are false, then that statement is true. Of course, classically, we only need to say that for one statement, and if we put it that way, then n=0n = 0 would no longer be an exception. So maybe we should think that the real statement (to prove the multiplicative existential quantification) is

( xA( yA(yx)P [y])P +[x]) xA( yA(yx)P [y])P +[x], (\exists_{x \in A} (\forall_{y \in A} (y \ne x) \Rightarrow P^-[y]) \Rightarrow P^+[x]) \wedge \forall_{x \in A} (\forall_{y \in A} (y \ne x) \Rightarrow P^-[y]) \Rightarrow P^+[x] ,

which merely simplifies to

( xA) xA( yA(yx)P [y])P +[x]. (\exists_{x \in A} \top) \wedge \forall_{x \in A} (\forall_{y \in A} (y \ne x) \Rightarrow P^-[y]) \Rightarrow P^+[x] .

Posted by: Toby Bartels on September 12, 2018 6:07 AM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

I see where it comes from, but I’d still like to see some examples before being convinced that it’s useful/interesting. Also, does it have a universal property?

If I recall correctly, bunched implications also has “multiplicative connectives”, but I never quite understood them. Perhaps they are something like left and right adjoints to pullback along the projections ABBA\otimes B \to B in a semicartesian category?

Posted by: Mike Shulman on September 12, 2018 12:43 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Coming back to this much later and hoping that you're still listening …

I don't know any universal property for this, but I don't know a universal property for the finitary version either. Semantically, it would have to be an additional structure on the category.

As for examples, I keep seeing them now that I'm looking for it! Like \parr, it isn't usually mentioned explicitly in constructive mathematics, but it's there.

For example, take the Intermediate-Value Theorem: if f:[a,b]f\colon [a,b] \to \mathbb{R} is pointwise-continuous and min(f(a),f(b))Lmax(f(a),f(b))\min(f(a),f(b)) \leq L \leq \max(f(a),f(b)), then there \parr-exists c[a,b]c \in [a,b] such that f(c)=Lf(c) = L. (Note that this doesn't work with \parr-existence as a purely intuitionistic quantifier; we have to use f(c)#Lf(c) \# L as the antithesis of f(c)=Lf(c) = L.) This is not the strongest version of the IVT, but it's pretty strong considering that we use mere pointwise continuity!

Here is the sort-of linear (or at least affine) proof: Suppose not. That is, for each c[a,b]c \in [a,b], f(c)#Lf(c) \# L. Note that f(a)<Lf(a) \lt L and f(b)>Lf(b) \gt L, or (\vee) f(a)>Lf(a) \gt L or f(b)<Lf(b) \lt L; I'll assume the former since the latter works similarly. Define infinite sequences AA and BB recursively with A 0=aA_0 = a, B 0=bB_0 = b, A n+1=A nA_{n+1} = A_n and B n+1=A n/2+B n/2B_{n+1} = A_n/2+B_n/2 if f(A n/2+B n/2)<Lf(A_n/2+B_n/2) \lt L, but A n+1=A n/2+B n/2A_{n+1} = A_n/2+B_n/2 and B n+1=B nB_{n+1} = B_n if f(A n/2+B n/2)>Lf(A_n/2+B_n/2) \gt L. By induction on nn, A n+1A nA_{n+1} \geq A_n, B n+1B nB_{n+1} \leq B_n, and B nA n=(ba)/2 nB_n - A_n = (b - a)/2^n; therefore, lim nA n\lim_n A_n and lim nB n\lim_n B_n exist and are equal, so let this common limit be CC. (We also have f(A n)<Lf(A_n) \lt L and f(B n)>Lf(B_n) \gt L by induction.) As with aa and bb, f(C)<Lf(C) \lt L or f(C)>Lf(C) \gt L; again, I'll assume the former since the latter works similarly. Let ϵ\epsilon be Lf(C)L - f(C), apply continuity at CC to get δ\delta, and pick NN so that N>log 2(ba)log 2δN \gt \log_2(b-a) - \log_2\delta. Then B NA N<δB_N - A_N \lt \delta; more specifically, 0B NC<δ0 \leq B_N - C \lt \delta, so f(B N)f(C)<ϵf(B_N) - f(C) \lt \epsilon, forcing f(B N)<Lf(B_N) \lt L, when in fact f(B N)>Lf(B_N) \gt L. Contradiction.

Here I use continuity only once; so this is pointwise continuity, stated as a normal (additive) universal quantification over points. The other quantifiers in the definition of continuity are also additive (one ϵ\epsilon, one δ\delta, one point within δ\delta of CC). In contrast I use f(c)#Lf(c) \# L repeatedly, so this is multiplicative universal quantification. (I don't use it for every cc in [a,b][a,b], but that's OK, since the logic is affine.) I also use values of ff repeatedly; I'm not sure how that fits in, but hopefully that's allowed.

This linear argument actually proves several intuitionistic theorems:

  • If f:[a,b]f\colon [a,b] \to \mathbb{R} is pointwise-continuous and min(f(a),f(b))Lmax(f(a),f(b))\min(f(a),f(b)) \leq L \leq \max(f(a),f(b)), then there is some cc in [a,b][a,b] (which is trivial) and for each such cc, if f(c)Lf(c') \ne L for each ccc' \ne c, then f(c)=Lf(c) = L.
  • If f:[a,b]f\colon [a,b] \to \mathbb{R} is pointwise-continuous and f(c)Lf(c) \ne L for each cc in [a,b][a,b], then min(f(a),f(b))>L\min(f(a),f(b)) \gt L or max(f(a),f(b))<L\max(f(a),f(b)) \lt L.
  • If f:[a,b]f\colon [a,b] \to \mathbb{R}, min(f(a),f(b))Lmax(f(a),f(b))\min(f(a),f(b)) \leq L \leq \max(f(a),f(b)), and f(c)Lf(c) \ne L for each cc in [a,b][a,b], then ff has a discontinuity.

(The existence of this discontinuity is true constructive existence, since it comes from a linear statement with additive quantification.) Which is just how you want the antithesis interpretation to work, right?

Incidentally, as you can see, I do have some rules of inference for the multiplicative quantifiers, which are really affine rules rather than linear ones. From xP[x]\bigotimes_x P[x], we may deduce P[a 1]P[a n]P[a_1] \otimes \cdots \otimes P[a_n] for any terms a 1,,a na_1, \ldots, a_n. To avoid using contraction, we probably need hypotheses that a ia ja_i \ne a_j whenever iji \ne j as well. (With strictly linear logic instead of affine, this rule could not be written.) Actually, my proof used a statement like this infinitely many times, in a sense, since it was used in a proof by induction; I'm not sure how to state the rule that I really used. (And I worry that I was really using contraction, since I used f(A n)#Lf(A_n) \# L and f(A n+1)#Lf(A_{n+1}) \# L in separate steps without always being able to verify that A n#A n+1A_n \# A_{n+1}. But this was in different stages of the induction, so maybe it's OK?) Similarly, we may use up any number of instances of a proposition to deduce its multiplicative existential quantification.

In the other direction, it should be possible to prove xP[x]\bigotimes_x P[x] by some method weaker than what would prove xP[x]\bigwedge_x P[x] (and if the logic were truly linear instead of affine, then it would have to be proved in this different way), but I can't think of what that would be. Similarly, I can't think of any good way to use multiplicative existential disjunction in a proof. But even if we never come up with anything here, the statements still have some applicability.

Posted by: Toby Bartels on February 17, 2020 10:41 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Thanks for coming back to this! It’s an exciting idea.

You’re right of course that the finitary \otimes and \parr are extra structure on Chu(C,)Chu(C,\bot) considered as a category. However, they have a universal property relative to Chu(C,)Chu(C,\bot) defined as a polycategory (which I explored further in this paper).

Perhaps we can describe a similar sort of “infinitary polycategory” to give these multiplicative quantifiers a universal property. In the finitary case we have (taking CC to be an arbitrary (closed, representable) multicategory and \bot an arbitrary object):

  • A morphism ()P() \to P is a morphism ()P +() \to P^+ (which induces a morphism P P^- \to \bot).
  • A morphism PQP\to Q is a pair of morphisms P +Q +P^+\to Q^+ and Q P Q^-\to P^- that induce the same morphism (P +,Q )(P^+,Q^-) \to \bot.
  • A morphism (P,Q)R(P,Q)\to R is a triple of morphisms (P +,Q +)R +(P^+,Q^+)\to R^+ and (P +,R )Q (P^+,R^-)\to Q^- and (R ,Q +)P (R^-,Q^+)\to P^- that induce the same morphism (P +,Q +,R )(P^+,Q^+,R^-)\to \bot.
  • A morphism (P,Q,R)S(P,Q,R)\to S is a quadruple of morphisms (P +,Q +,R +)S +(P^+,Q^+,R^+)\to S^+ and (P +,Q +,S )R (P^+,Q^+,S^-) \to R^- and (P +,S ,R +)Q (P^+,S^-,R^+)\to Q^- and (S ,Q +,R +)P (S^-,Q^+,R^+)\to P^- that induce the same morphism (P +,Q +,R +,S )(P^+,Q^+,R^+,S^-)\to \bot.

So in the infinitary case we should have

  • A morphism (P i) iQ(P_i)_i \to Q is a morphism (P i +) iQ +(P_i^+)_i \to Q^+ and a family of morphisms ((P i +) ij,Q )P j ((P_i^+)_{i\neq j}, Q^-) \to P_j^- that all induce the same morphism ((P i +) i,Q )((P_i^+)_i,Q^-)\to \bot.

Of course in the posetal case the “induce the same morphism to \bot” clauses are vacuous. But there’s still something a bit questionable going on here in how a morphism ((P i +) ij,Q )P j ((P_i^+)_{i\neq j}, Q^-) \to P_j^- induces a morphism ((P i +) i,Q )((P_i^+)_i,Q^-)\to \bot. What it naturally induces is a morphism ((P i +) ij,P j +,Q )((P_i^+)_{i\neq j}, P_j^+, Q^-) \to \bot. If the original “infinitary multicategory” we start from is cartesian then we can get from this to a morphism ((P i +) i,Q )((P_i^+)_i,Q^-)\to \bot, but this disconnect makes me suspicious that these operations will be at least ill-behaved if the indexing set doesn’t have decidable equality.

However, this perspective does solve the problem of quantification over the empty set. For morphisms (P,Q)R(P,Q)\to R to correspond to morphisms PQRP\otimes Q \to R we argue as follows:

  • The only map to R +R^+ in a morphism (P,Q)R(P,Q)\to R is (P +,Q +)R +(P^+,Q^+)\to R^+, so (PQ) +=P +Q +(P\otimes Q)^+ = P^+ \otimes Q^+ (the tensor product in the original multicategory, which in the case of the antithesis interpretation is P +Q +P^+ \wedge Q^+).

  • The maps out of R R^- in a morphism (P,Q)R(P,Q)\to R are (P +,R )Q (P^+,R^-)\to Q^- and (R ,Q +)P (R^-,Q^+)\to P^-, which correspond to morphisms R [P +,Q ]R^- \to [P^+, Q^-] and R [Q +,P ]R^- \to [Q^+, P^-] in the original (closed) multicategory… which must additionally induce the same morphism R [P +Q +,]R^- \to [P^+ \otimes Q^+, \bot]. Thus, (PQ) (P\otimes Q)^- should be the pullback [P +,Q ]× [P +Q +,][Q +,P ][P^+,Q^-] \times_{[P^+ \otimes Q^+, \bot]} [Q^+, P^-].

In general, (P 1P n) +=P 1 +P n +(P_1\otimes\cdots\otimes P_n)^+ = P_1^+ \otimes \cdots \otimes P_n^+, while (P 1P n) (P_1\otimes\cdots\otimes P_n)^- is the pullback of nn internal-homs with targets P i P_i^- over the internal-hom [P 1 +P n +,][P_1^+ \otimes \cdots \otimes P_n^+,\bot]. And this is also correct when n=0n=0: we have I +=II^+ = I, the unit object of CC which is the tensor product of zero objects, and I I^- is the pullback of zero objects over \bot, which is just \bot.

This tells us that ( iP i) +(\bigotimes_i P_i)^+ should be iP i +\forall_i P_i^+, as you proposed, but that ( iP i) (\bigotimes_i P_i)^- should be the wide pullback of [ ijP i +,P j ][ \forall_{i\neq j} P_i^+, P_j^- ], for all jj, over [ iP i +,][ \forall_i P_i^+, \bot ]. In the case of the antithesis interpretation this becomes

¬( xAP +[x]) xA(( yA(yx)P +[y])P [x]). \neg (\forall_{x\in A} P^+[x]) \wedge \forall_{x\in A}((\forall_{y\in A} (y\neq x) \to P^+[y]) \to P^-[x]).

This also has the correct behavior for the empty set, and seems more clearly correct since it arises from the abstract picture. Note also that with this definition, xA\bigotimes_{x\in A} and xA\parr_{x\in A} don’t use \exists at all, only \forall and ,\wedge,\to, which is analogous to how the finitary \otimes and \parr don’t use \vee at all.

However… after all that, I’m not sure how to make sense of your IVT proof. The universal property in infinitary-polycategories should give a reasonable sort of “infinitary logic”, which I suspect would actually just look like a somewhat odd sort of first-order logic. But before we try to make sense of your affine-logic induction, we should make sure that all the intuitionistic parts of your putative IVT are in fact true intuitionistically. (With \neq meaning apartness, I assume.)

I can believe this for the third “ff has a discontinuity” one, by an intuitionistic version of your bisection argument, and the second one probably follows from this by case analysis on f(a)Lf(a) \neq L and f(b)Lf(b)\neq L. The first one is trickier, but I could imagine proving it with a “trisection” argument. At each stage, if we have f(A n)<L<f(B n)f(A_n) \lt L \lt f(B_n), then at least one of 2A n+B n3\frac{2A_n +B_n}{3} and A n+2B n3\frac{A_n+2B_n}{3} must be apart from cc. Letting cc' be one that is, then by assumption f(c)Lf(c')\neq L, so we can let cc' be either A n+1A_{n+1} or B n+1B_{n+1} as usual. Now if CC is the common limit we find f(C)=Lf(C)=L, so ¬(f(C)L)\neg (f(C)\neq L) and hence ¬(Cc)\neg (C\neq c); whence C=cC=c (since apartness on the reals is tight) and so f(c)=Lf(c)=L.

This appears to use countable choice; it’s possible that that could be avoided with some trick like Matt Frank’s for the approximate IVT, but at the moment I don’t see how. And the use of tight apartness suggests that in an affine-logic proof we’ll have to use the fact that affine-logic equality on the reals is refutative, i.e. that its negation can be contracted — and interestingly, I see that you were worried about contracting a negated equality!

Yet, I don’t see right now any way that the trisection is relevant to the affine-logic proof, or how your possible contractions on f(A n)Lf(A_n)\neq L are related to my use of tight apartness on f(C)Lf(C)\neq L. It’s tricky partly because this sort of proof that constructs a sequence by recursion, using a logical case distinction at each step, fits very uncomfortably into the tripos logic that I used for the antithesis interpretation, in which the function comprehension principle has to be asserted as an axiom, and recursion and induction are very different-looking beasts.

Another thing worth pondering, at least a little, is whether the internal implication in the definition of multiplicative quantifiers should also be an antithesis one. That is, a proof of xAP[x]\parr_{x\in A} P[x] could be

¬( xAP [x]) xA(( yA((yx)P [y])(P +[y](y=x)))P +[x]). \neg (\forall_{x\in A} P^-[x]) \wedge \forall_{x\in A}((\forall_{y\in A} ((y\neq x) \to P^-[y]) \wedge (P^+[y] \to (y=x))) \to P^+[x]).

In particular, this would yield the necessary contrapositive “if f(c)=Lf(c')=L then c=cc'=c” without the need for tightness of \neq. And it’s related to the question of “quantification over a subset” that you brought up earlier.

Posted by: Mike Shulman on February 18, 2020 12:41 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Hmm, maybe I am overcomplicating things. To prove your first intuitionistic theorem, I guess we can just observe that if f(c)Lf(c)\neq L (apartness), then f(x)Lf(x)\neq L on some open interval II around cc by pointwise continuity. Thus since f(c)Lf(c')\neq L for all ccc'\neq c, and any c[a,b]c'\in [a,b] is either in II or apart from cc, we have f(c)Lf(c')\neq L for all c[a,b]c'\in [a,b]. This is impossible by your third intuitionistic theorem, so ¬(f(c)L)\neg(f(c)\neq L); hence f(c)=Lf(c)=L by tightness.

This argument is also much closer to an antithesis of the other two theorems, which makes your affine argument seem to me much more likely to be valid. But it’ll still take a bit of thought to find a formal system in which that argument makes sense.

Posted by: Mike Shulman on February 18, 2020 6:29 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

I’m so glad I came across this post, albeit three years late to the party, during my adventure in linear and polarized logic.

I’ve made an Agda embedding for this, and gone on to formulate setoids over partial equivalence relations (which automatically comes bundled with a partial apartness relation!). I stopped after defining functions on setoids, but theoretically I do not see any difficulty in extending this to more non-trivial mathematical constructs, apart from the setoid hell that we already have in intuitionistic type theory.

In fact, I think it is very promising to try and apply this technique to the construction of real numbers. But there is currently way too much low level plumbing happening, and I have yet to figure out how to make a set of combinator-like tools to sweep the details under the carpet. It is also entirely possible that we cannot hide the details in Agda (at least without some tactic mechanism in place). There might even be some interesting interaction between this and HoTT.

Posted by: Trebor Huang on December 3, 2021 3:57 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Very cool, thanks for sharing! Back when I was writing the paper, I spent a while playing around with formalizing arguments directly in affine logic (rather than embedding in a nonlinear proof assistant via the antithesis construction), using a linear sequent calculus in Isabelle. I think there are a lot of interesting directions to pursue here.

As long as I’m commenting on this post, I may as well mention that the paper was substantially updated last summer in response to referee comments. I recommend that anyone who read the old version should also go back and take a look at the new one.

Posted by: Mike Shulman on December 4, 2021 11:07 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Thanks for the link and the update!

I was really confused the first time, when I noticed that your “times” can’t distinguish twice from thrice (i.e. AAA=AAA \otimes A \otimes A = A \otimes A) IIRC. Which differs from Girard’s logic, where these are different. So changing the wording suits your paper well IMHO, makes the content clearer.

So I’ll gladly read the paper once more. I very much liked your explanation & adaption of the BHK-interpretation when I read it the first time. I’ll hopefully see some nice description of constructive reasoning this time as well.

Posted by: Stéphane Desarzens on December 22, 2021 10:03 PM | Permalink | Reply to this

Re: Linear Logic for Constructive Mathematics

Well, AAA=AAA\otimes A \otimes A = A\otimes A also doesn’t hold in fully general affine logic; either way, the antithesis interpretation is very special.

Posted by: Mike Shulman on December 23, 2021 5:01 PM | Permalink | Reply to this

Post a New Comment