The n-Category Café

When we first learn about logic, we often learn various tautologies such as de Morgan’s laws $\neg(P \wedge Q ) \equiv (\neg P \vee \neg Q)$ and the law of excluded middle $P \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” $P\to Q$ satisfying $(P\le Q\to R) \iff (P \wedge Q \le R)$. Any Boolean algebra is a Heyting algebra (with $(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 $(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 \equiv (P\to 0)\to 0$, where $0$ is the bottom element and $P\to 0$ is the intuitionistic “not $P$”.) 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 \equiv (P\multimap \bot)\multimap \bot$. Such a lattice has a contravariant involution defined by $P^\perp = (P \multimap \bot)$ and a “cotensor product” $(P \parr Q) \equiv (P^\perp \otimes Q^\perp)^\perp$, and its internal-hom is definable in terms of these: $(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 $C$ is a closed symmetric monoidal lattice, and $\bot$ is any element of $C$ at all. Then there is a star-autonomous lattice $Chu(C,\bot)$ whose objects are pairs $(P^+,P^-)$ such that $P^+ \otimes P^- \le \bot$, and whose order is defined by $$((P^+,P^-) \le (Q^+,Q^-)) \iff (P^+ \le Q^+) \;\text{and}\; (Q^- \le P^-).$$ In other words, $Chu(C,\bot)$ is a full sub-poset of $C\times C^{op}$. Its lattice operations are pointwise: $$(P^+,P^-) \wedge (Q^+,Q^-) \equiv (P^+ \wedge Q^+, P^- \vee Q^-)$$ $$(P^+,P^-) \vee (Q^+,Q^-) \equiv (P^+ \vee Q^+, P^- \wedge Q^-)$$ while the tensor product is more interesting: $$(P^+,P^-) \otimes (Q^+,Q^-) \equiv (P^+ \otimes Q^+, (P^+ \multimap Q^-) \wedge (Q^+ \multimap P^-))$$ The self-duality is $$(P^+,P^-)^\bot \equiv (P^-,P^+).$$ from which we can deduce the definitions of $\parr$ and $\multimap$: $$(P^+,P^-) \parr (Q^+,Q^-) \equiv ((P^- \multimap Q^+) \wedge (Q^- \multimap P^+), P^- \otimes 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 $0$, since that would be the self-dualizing object if our Heyting algebra were a Boolean algebra. The resulting monoidal structure on $Chu(H,0)$ is actually semicartesian: the monoidal unit coincides with the top element $(1,0)$.

The point, now, is to look at this Chu construction $Chu(H,0)$ from the logical perspective, where elements of $H$ are regarded as propositions in intuitionistic logic. The elements of $Chu(H,0)$ are pairs $(P^+, P^-)$ such that $P^+ \wedge P^- = 0$, i.e. pairs of mutually incompatible propositions. We think of such a pair as a proposition $P$ together with information $P^+$ about what it means to affirm or prove it and also information $P^-$ about what it means to refute or disprove it. The condition $P^+ \wedge P^- = 0$ means that $P$ cannot be both proven and refuted; but we might still have propositions such as $(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 $P\wedge Q$ is a proof of $P$ together with a proof of $Q$. A refutation of $P\wedge Q$ is either a refutation of $P$ or a refutation of $Q$.
• A proof of $P\vee Q$ is either a proof of $P$ or a proof of $Q$. A refutation of $P\vee Q$ is a refutation of $P$ together with a refutation of $Q$.
• A proof of $P^\perp$ is a refutation of $P$. A refutation of $P^\perp$ is a proof of $P$.
• A proof of $P\otimes Q$ is, like for $P\wedge Q$, a proof of $P$ together with a proof of $Q$. But a refutation of $P\otimes Q$ consists of both (1) a construction of a refutation of $Q$ from any proof of $P$, and (2) a construction of a refutation of $P$ from any proof of $Q$.
• A proof of $P\parr Q$ consists of both (1) a construction of a proof of $Q$ from any refutation of $P$, and (2) a construction of a proof of $P$ from any refutation of $Q$. A refutation of $P\parr Q$ is, like for $P\vee Q$, a refutation of $P$ together with a refutation of $Q$.

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” $P \vee P^\perp$ fails for the same reason that it fails under the BHK-interpretation: we cannot decide for an arbitrary $P$ whether to prove it or refute it. However, the “multiplicative law of excluded middle” $P \parr P^\perp$ is a tautology: if we can refute $P$, then by definition we can prove $P^\perp$, while if we can refute $P^\perp$, then again by definition we can prove $P$. 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 $P\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=^L y)$ valued in linear propositions. Since each of these is an element of $Chu(H,0)$, it is a pair of mutually incompatible intuitionistic relations; we will call these $(x=^I y$ and $(x\neq^I y)$ respectively.

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

Of course, transitivity says that if $x=y$ and $y=z$, then $x=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=^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)$, this says that $(x=^I y) \wedge (y=^I z) \vdash (x=^I z)$ (that is, $=^I$ is transitive) and $(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$ is reflexive, symmetric, and transitive say that (1) $=^I$ is reflexive, symmetric, and transitive, and (2) $\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 $A$ and $B$ are L-sets, then in the cartesian product L-set $A\times B$ we have $(a_1,b_1) =^L (a_2,b_2)$ defined by $(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) \neq^I (a_2,b_2)$ means $(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 $A$ and $B$ are sets, the elements of the function L-set $A\to B$ are I-functions that are strongly extensional: $(f(x) \neq^I f(y)) \vdash (x\neq^I y)$ (this is called “strong” because the apartness $\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 =^L g)$ is defined by $\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=^I g)$ meaning $\forall x. (f(x) =^I g(x))$, the usual pointwise equality of functions, and $(f\neq^I g)$ meaning $\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)$ of an L-set $A$ are pairs $(U^+,U^-)$ of I-subsets of the underlying I-set of $A$, which must additionally be strongly disjoint in that $(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=^L y) \wedge (x\in U) \vdash (y\in U)$ translates to the requirement that $U^-$ be strongly extensional (also called “$\neq^I$-open”): $(y\in U^-) \vdash (x\neq^I y) \vee (x\in U^-)$.

5. Equality between L-subsets $(U=^L V)$ means $\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^-)$ means $(U^+=V^+) \wedge (U^- = V^-)$ as we would expect, while $(U^+,U^-) \neq^I (V^+,V^-)$ means $(\exists x \in U^+ \cap V^-) \vee (\exists x\in U^- \cap V^+)$. In particular, we have $U \neq^L \emptyset$ (where the empty L-subset is $(\emptyset,A)$) just when $\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\times G\to G$, unit $e\in G$, and inversion $i:G\to G$ satisfying the usual axioms. In the standard interpretation, this corresponds to an ordinary I-group equipped with an apartness $\neq^I$ such that multiplication and inversion are strongly extensional: $(x^{-1} \neq^I y^{-1}) \vdash (x \neq^I y)$ and $(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^-)$ as above such that $H^+$ is an ordinary I-subgroup and $H^-$ is an antisubgroup, meaning a set not containing $e$, closed under inversion ($(x\in H^-) \vdash (x^{-1}\in H^-)$), and satisfying $(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^+$ by $[x]\neq^I [y]$ if $x y^{-1} \in H^-$.

8. An L-poset is an L-set with a relation $\le^L$ that is reflexive, transitive ($(x\le^L y) \wedge (y\le^L z) \vdash (x\le^L z)$) and antisymmetric ($(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 $\le^I$ and $\lt^I$: then $\le^I$ is an ordinary I-partial-order, $\lt^I$ is a “bimodule” over it ($(x\le^I y) \wedge (y \lt^I z) \vdash (x\lt^I z)$ and dually) which is cotransitive ($(x\lt^I z) \vdash (x\lt^I y) \vee (y\lt^I z)$) and “anti-antisymmetric” in the sense that $(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 $P \otimes Q \vdash P\wedge Q$ and $P\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=^L 0) \vee \exists y. (x y =^L 1)$. Under the standard interpretation, this corresponds to an I-ring (with apartness) such that $(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=^L 0) \parr \exists y. (x y =^L 1)$. Under the standard interpretation, this corresponds to an I-ring (with apartness) such that $(x \neq^I 0) \to \exists y. (x y =^I 1)$ and $(\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, $x\le y$ means $(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\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=^L y) \otimes (y=^L z) \vdash (x=^L z)$, then in the standard interpretation the comparison condition disappears, so that $\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 $\neq^I$ satisfies substitution with respect to $=^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”.