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.

July 23, 2019

Summer Meanderings About Enriched Logic

Posted by David Corfield

Reading the recently appeared article

which treats Gabriel-Ulmer and related dualities in an enriched setting, I was wondering what sense we should make of “enriched logic”.

If, for instance, we may think of ordinary Gabriel-Ulmer duality as operating between essentially algebraic theories and their categories of models, then how to think of a finitely complete 𝒱\mathcal{V}-category as a kind of enriched essentially algebraic theory?

That got me wondering about the case where 𝒱\mathcal{V} is the reals or the real interval, i.e., something along the lines of a Lawvere metric space, which led me to some recent work on continuous logic. This logic is associated with a longstanding program on continuous model theory, but it seems that the time is ripe now for category theoretic recasting, as in:

  • Simon Cho, Categorical semantics of metric spaces and continuous logic, (arXiv:1901.09077).

In this article Cho argues that the object of truth values of continuous logic is to be seen as a “continuous subobject classifier” in the sense of topos theory.

This raises questions of the proximity between real-enrichment and plain set-enrichment. Cho notes in his earlier thesis that the relevant thought is briefly discussed in the comments section of a post on the nn-Category Café. This is the idea that SetSet itself is a (subcategory of a) category of categories enriched in the poset of truth values, and came up in the discussion of Tom Avery’s post for the Kan Extension Seminar, starting with this comment.

Another sign that real-enriched category theory shares similarities to ordinary category theory is that we can have something close to conceptual completeness there.

  • Jean-Martin Albert, Bradd Hart, Metric logical categories and conceptual completeness for first order continuous logic, (arXiv:1607.03068)

Even though “Grothendieck’s notion of pre-topos is much too strong for the needs of continuous logic”, the authors arrive at the concept of a metric pre-topos.

The nn-Café spilled over to a discussion on fuzzy logic as an enriched logic. I wonder if continuous logic has better categorical credentials.

And did Lawvere ever link his metric space ideas with his ideas on cohesion?

Posted at July 23, 2019 6:47 AM UTC

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

27 Comments & 0 Trackbacks

Re: Summer meanderings about enriched logic

If we think of a category enriched over the monoidal poset ([0,],,+)([0, \infty], \geq, +) as a Lawvere metric space, what does it mean for this enriched category to be finitely complete? I’m too lazy to work it out.

Posted by: John Baez on July 28, 2019 2:34 AM | Permalink | Reply to this

Re: Summer meanderings about enriched logic

Right. So we need to know what it takes for one of these metric spaces to have all finite weighted limits. Surely the experts around here know what this entails. But then why should such a thing act like it’s a kind of theory?

Posted by: David Corfield on July 28, 2019 8:49 PM | Permalink | Reply to this

Re: Summer meanderings about enriched logic

I guess Simon is our go-to-guy:

Theorem 18. A skeletal generalized metric space is finitely complete if and only if it can be given a metric semi-tropical structure. (Tight spans, Isbell completions and semi-tropical modules)

Posted by: David Corfield on July 28, 2019 9:01 PM | Permalink | Reply to this

Re: Summer meanderings about enriched logic

Yes, indeed. That’s the paper I would have sent you to.

Posted by: Simon Willerton on July 29, 2019 10:31 PM | Permalink | Reply to this

Re: Summer meanderings about enriched logic

OK, so does your space equipped with a metric semi-tropical structure look anything like what one might call a theory?

Hmm, your pair of monoid multiplications and actions on p. 4 seem to resemble the (binary case of) \sqcap and \sqcup, \star and \rhd of the Babus and Kutz paper (p. 19) that I mention below.

So it seems that this ‘logic’ is about satisfaction up to a degree (example 50.2, p. 19). I wonder if contact can be made with the idea of ‘partial entailment’, which goes back (at least) to Keynes’ A treatise on probability (1921).

Posted by: David Corfield on July 30, 2019 10:10 AM | Permalink | Reply to this

Re: Summer meanderings about enriched logic

I don’t have time right now to work out whether this is related to any of what you’re talking about, but Example 11.3 of Linear logic for constructive mathematics observes that Łukasiewicz logic is a semicartesian *\ast-autonomous structure on [0,1][0,1], giving rise to an affine logic in which sets are classical metric spaces, subsets of discrete spaces are fuzzy sets, etc.

Posted by: Mike Shulman on July 28, 2019 4:35 AM | Permalink | Reply to this

Re: Summer meanderings about enriched logic

This seems closer to Cho’s perspective. Metric spaces are being compared to sets/posets rather than to categories, i.e., values in the reals being compared to values in truth values.

Posted by: David Corfield on July 28, 2019 9:26 PM | Permalink | Reply to this

Re: Summer meanderings about enriched logic

It seems that there’s a binary connective dotdiv\dotdiv which plays the role of implication in Łukasiewicz logic and continuous logic, but that the latter also can express the operation of halving a proposition, and so multiplication by any dyadic number.

The idea seems to be that an nn-ary connective is a continuous function [0,1] n[0,1][0, 1]^n \to [0, 1] and these may be approximated by functions generated by {¬,dotdiv,12}\{\neg, \dotdiv, \frac{1}{2}\}.

Posted by: David Corfield on August 1, 2019 5:12 PM | Permalink | Reply to this

Re: Summer meanderings about enriched logic

I came across a paper – On the logic of generalised metric spaces – by Octavian Babus and Alexander Kurz – one of whose aims is to say what a propositional Ω\Omega-logic looks like for a commutative quantale Ω\Omega.

From section 5.3, it involves atomic propositions, a pair of unary operations indexed by values in Ω\Omega, and a generalised join and meet. Satisfaction of a proposition in a state occurs to a degree given by an element of Ω\Omega.

You can see there why things turn out so simply in the ordinary case where Ω=𝟚\Omega = \mathbb{2} (example 50.1).

The authors conclude:

It lies in the nature of this method that the logic…we derived from Ω\Omega is not purely syntactic but still depends on Ω\Omega. The operations are infinitary and the laws contain side conditions depending on Ω\Omega. We can think of Ω\Omega as an oracle that we need to consult in our reasoning. Restricting to particular, syntactically given Ω\Omega and then describing [the logic] fully syntactically, so that consulting the oracle can be replaced by asking an automated theorem prover, is a task of future research.

Posted by: David Corfield on July 29, 2019 9:19 AM | Permalink | Reply to this

Re: Summer meanderings about enriched logic

Why isn’t propositional logic over an arbitrary commutative quantale just intuitionistic multiplicative-additive linear logic?

Posted by: Mike Shulman on July 29, 2019 10:55 AM | Permalink | Reply to this

Re: Summer meanderings about enriched logic

Um. Is this just a matter of their wanting to specify the logic tailored to a specific choice of quantale?

I thought you were indicating over here that the logic tied to a specific enrichment would be odd syntactically.

Puts me in mind of something your n-theory post raised for me as to why there shouldn’t be other things that models might form:

It definitively expects the models of an nn-theory to form an nn-category, and not just an nn-groupoid.

Why only nn-categories?

Posted by: David Corfield on July 29, 2019 11:27 AM | Permalink | Reply to this

Re: Summer meanderings about enriched logic

I see I was chipping away at that last thought in the final comment there. But here why not some enriched version of an nn-category?

Posted by: David Corfield on July 29, 2019 11:42 AM | Permalink | Reply to this

Re: Summer meanderings about enriched logic

I don’t know what “the logic tailored to a particular choice of quantale” means. Generally, a logic corresponds to a class of models: classical logic to Boolean algebras, intuitionistic logic to Heyting algebras, IMALL to commutative quantales, etc. What would “the logic tailored to a particular choice of Boolean algebra” be?

My comment about 𝒱Lex\mathcal{V}Lex was about a different kind of “theory”. An ordinary lex category is the semantic incarnation of an (essentially) algebraic theory, with sets of sorts, operations, and axioms. The enriched version of that would have 𝒱\mathcal{V}-objects of operations, which are fine semantically but it’s not clear how a syntax could specify them.

Or am I misunderstanding what role the quantale plays? Are we not thinking of replacing the Boolean algebra (such as 2={,}\mathbf{2}=\{\bot,\top\}) of truth values with a quantale Ω\Omega of truth values, but instead of something like regarding our Boolean algebra as enriched over 2\mathbf{2} and replacing it with some kind of lattice enriched over Ω\Omega instead?

Posted by: Mike Shulman on July 31, 2019 9:32 PM | Permalink | Reply to this

Re: Summer meanderings about enriched logic

Yes, your latter paragraph has the right idea. In his thesis (Remark 8.15), Cho takes as important the idea that we take posets as 2\mathbf{2}-enriched and then sets as symmetric 2\mathbf{2}-enriched. Then we generalise to other quantales.

How about this? Our standard (n,r)-category story has us start out with 2\mathbf{2} in (1,0)(-1,0) position. Movement in the (+1,+1)(+1, +1) direction is enrichment, while movement in the (0,1)(0, -1) direction is some form of symmetrisation.

Applying both of these steps twice to 2\mathbf{2}, for instance, we zigzag through Poset, Set, Category, Groupoid (leaving aside preorder/poset issues).

Now do similarly for a different quantale, Ω\Omega. Say we choose the extended non-negative reals. The corresponding steps are to Met (generalized metric spaces), then SymMet (symmetric such spaces), from where we could look to enrich in these and so on. People do such things as I see in Tholen and Wang’s Metagories Def 2.5.

Now, for any of these entities we may look to require (co)completeness properties. Gathering all entities of a kind generates a particularly nice case of the enriched entity, e.g., SetSet as a category which is a topos. There will be doctrinal dualities appropriate for each kind of enriched entity, relating forms of theory to their models.

In his work on the Isbell completion of a generalized metric space, Simon unearthed monoidal operations and multiplications which correspond to what Babus and Kutz argue is the syntax for a propositional logic of metric spaces.

Cho is looking at the category of metric spaces, which one might predict to be a topos-like MetMet-enriched thing. Hence [0,1][0, 1] is appearing as a ‘continuous subobject classifier’. So-called ‘continuous logic’ seems to be the appropriate logic for such settings.

Back in the simple propositional metric case, I have a suspicion that philosophers have been coming close. One might hope that category-theoretic tools would provide guidance. Say we can understand a sufficiently (co)complete generalized metric space as a kind of theory (with partial entailment?), doctrinal duality would appear to tell us that models of such a theory should also form a metric space but with features such as being locally finitely presented.

What’s a locally finitely presented generalized metric space?

Posted by: David Corfield on August 1, 2019 8:49 AM | Permalink | Reply to this

Re: Summer meanderings about enriched logic

No, looking at the paper I think it’s more like what I was originally thinking, with Ω\Omega as the truth values and therefore the symmetric Ω\Omega-enriched categories as “sets” — which is also what happens in linear constructive mathematics. I guess the answer to my question

Why isn’t propositional logic over an arbitrary commutative quantale just intuitionistic multiplicative-additive linear logic?

is actually “it is, plus constant elements corresponding to the elements of Ω\Omega itself — this is where it gets different depending on what Ω\Omega is — but they’re only considering a fragment of it.” Plus they’re really looking at what I would call a version of predicate logic rather than propositional logic, since they have quantifiers \bigsqcup and \bigsqcap indexed by arbitrary sets.

General IMALL has additive connectives \sqcap and \sqcup with units \top and \bot, additive quantifiers \bigsqcap and \bigsqcup (that reduce to \sqcap and \sqcup on 2-element sets and \top and \bot on 0-element sets), a multiplicative conjuction \otimes, and a multiplicative implication \multimap. Over Ω\Omega we can augment this with constants v¯\bar{v} for all vΩv\in \Omega; abstractly this is the theory of commutative quantales under Ω\Omega, which includes all the posets of predicates Ω X\Omega^X in the linear tripos generated by Ω\Omega.

Their fragment includes \bigsqcap and \bigsqcup (hence also ,,,\sqcap,\sqcup,\top,\bot) plus operations vv\star - and vv \rhd - that I think can be defined for vΩv\in\Omega by vx=v¯xv\star x = \bar{v} \otimes x and vx=v¯xv\rhd x = \bar{v}\multimap x. Which seem certainly like useful operations, but it seems to me clearly better to also keep around the binary operations \otimes and \multimap and derive \star and \rhd from these and the constants.

The “\overset{\cdot}{-}” connective in Łukasiewicz logic is just another name for \multimap (with arguments reversed). The corresponding \otimes is min(x+y,1)\min(x+y,1) (which can be induced by regarding [0,1][0,1] as a reflective subcategory of [0,][0,\infty]). This defines a *\ast-autonomous structure on [0,1][0,1] with ¬x=1x\neg x = 1-x and therefore

xy=¬xy=¬(x¬y)=1min(1+xy,1)=max(yx,0)=yx.x\multimap y = \neg x \parr y = \neg (x \otimes \neg y) = 1 - \min(1+x-y,1) = \max(y-x,0) = y \overset{\cdot}{-} x.

Posted by: Mike Shulman on August 2, 2019 1:56 PM | Permalink | Reply to this

Re: Summer meanderings about enriched logic

I’m confused. There are different quantales on [0,1][0, 1] aren’t there. Yours here with the Łukasiewicz tensor is the item 3(c) (in fact the second isomorphic version mentioned there) of the list on p.5 of Enriched Stone-type dualities.

The one given by Babus and Kutz for [0,][0, \infty] is equivalent to the one on [0,1][0,1] (via the map exp(x)exp(-x)) which is the first in the list, 3(a).

But maybe the difference isn’t important to what you say. Enriching with the three versions leads to metric, ultrametric and bounded metric space, respectively.

Posted by: David Corfield on August 4, 2019 10:24 AM | Permalink | Reply to this

Re: Summer meanderings about enriched logic

Well, the general stuff about quantales will apply to any such. Łukasiewicz logic is the one on [0,1][0,1] obtained by reflection as a subcategory of [0,][0,\infty], and it happens to be *\ast-autonomous and thus a model of classical linear logic; the others are not *\ast-autonomous and thus only model intuitionistic linear logic. I guess I blurred the difference between ([0,1],min(+,1))([0,1],\min(+,1)) and ([0,],+)([0,\infty],+) a bit, but both have \overset{\cdot}{-} as their \multimap. In the latter case the computation would instead be

x+yzxzyxmax(zy,0) x+y \ge z \quad\iff\quad x \ge z - y\quad \iff\quad x \ge \max(z-y,0)

since x0x\ge 0.

Posted by: Mike Shulman on August 4, 2019 2:51 PM | Permalink | Reply to this

Re: Summer meanderings about enriched logic

So to return to the original question, it seems we might say that in some version of real-enrichment, (the Lindenbaum algebra of) some variety of propositional theory is a kind of exact generalized metric space, and its models will form another kind of generalized metric space.

A theory may include judgements as to partial derivation to a degree. And the distance between models depends on the distances between the values they assign to propositions.

Or something like that.

Posted by: David Corfield on August 6, 2019 8:22 AM | Permalink | Reply to this

Re: Summer meanderings about enriched logic

Which original question? And how do you get a metric on the set of models (rather than on the propositions in particular model) — doesn’t that mix dimensions? The collection of VV-enriched categories is not in general itself a VV-category (it’s a VV-2-category).

Posted by: Mike Shulman on August 6, 2019 6:49 PM | Permalink | Reply to this

Re: Summer meanderings about enriched logic

The original question was:

In view of the fact that duality results such as Gabriel-Ulmer duality can be considered as ways of making correspond theories of a certain doctrinal strength with their models, how might we understand enriched versions of these dualities in similar terms?

So where does the following line of thought go wrong?

  1. GU duality tells us of the equivalence between the 2-categories LexLex and LFPLFP, relating categories corresponding to essential algebraic theories to their categories of models.

  2. There is an analogous duality in the truth value-enriched case between meet semilattices and algebraic lattices, i.e., between two kinds of poset.

  3. Just as we can see (1) as concerning theories presented in cartesian logic, a fragment of first-order logic, so we can see (2) as concerning theories in a fragment of propositional logic. [Side question: In (2), is it really some equivalence between 2-posets?]

  4. So now in the case where in (2), 2\mathbf{2} is replaced by [0,][0, \infty] or [0,1][0,1], it would seem that we have a duality between two kinds of metric space instead of two kinds of poset. In particular, in the GU case, we’d expect a ‘theory’ to be a finitely complete metric space, the kind of thing Simon tells us about.

  5. This ‘theory’ should be presented in a fragment of some form of [0,][0, \infty]-propositional logic.

  6. The models of any such theory should form a metric space of a locally-finitely presented kind. A reasonable idea of the ‘distance’ involved in this space of models is the supremum of distances between the values assigned by two models to points (propositions) in the theory.

OK so far?

But then why when we turn up the dial on the logic, say from cartesian propositional to full-on Boolean propositional does the collection of models for a theory in that logic form a set rather than a kind of poset? That endless stream of dualities in Johnstone’s Stone Spaces relates varieties of poset. Could we say that we’ve made it so much harder to have models that they only form the kind of poset which allows no comparisons, i.e., a set?

Have we forced the poset to be symmetric? In which case we might expect a symmetric metric space of models for a real-enriched Boolean propositional logic, which makes sense considering the values assigned by two models to a proposition and its negation.

Posted by: David Corfield on August 7, 2019 10:52 AM | Permalink | Reply to this

Re: Summer meanderings about enriched logic

Since we have a quantale map from truth values to [0,1][0, 1], we can see a poset as a kind of metric space. So, passing across syntax-semantics duality, we should expect to see people treating sets of models of propositional theories as metric spaces, and indeed we do:

…the widely used Hamming distance (which merely counts the number of propositional symbols assigned a different value by two worlds) (Propositional Distances and Preference Representation)

The distance between models of a classical propositional logic is symmetric, as predicted. (Naturally, the Hamming distance has appeared in the context of enriched categories before at the Café, here.)

Up a level, I guess we shouldn’t be surprised that even though we had dualities relating varieties of category, e.g., LexLex and LfpLfp, that when the ‘logic’ is dialled up to first-order classical, we find that the models corresponding to a theory, that is a Boolean pretopos, form a kind of groupoid (an ultragroupoid for Makkai). Symmetrisation again.

So we might expect a classical continuous first-order logical theory to be a kind of symmetric metric space-enriched category, and this is called a ‘metric pretopos’ by Albert and Hart. There should then be a continuous Makkai duality to accompany their version of conceptual completeness.

Posted by: David Corfield on August 8, 2019 11:15 AM | Permalink | Reply to this

Re: Summer meanderings about enriched logic

Ah, I think I was thinking about a more general kind of model. (Sorry, I think I haven’t been giving this conversation my full attention.) By default when I talk about a model of a theory, I always mean a model in some category, but you mean models in the base enriching category (e.g. a model of a classical cartesian theory is a model in SetSet). So here, you mean models of a Ω\Omega-theory in Ω\Omega itself, i.e. functors to Ω\Omega from the Lindenbaum algebra TT, and so the functor category Lex(T,Ω)Lex(T,\Omega) is again an Ω\Omega-enriched category.

Posted by: Mike Shulman on August 8, 2019 11:32 AM | Permalink | Reply to this

Re: Summer meanderings about enriched logic

The “continuous subobject classifier” is I think also just the object of predicates in the linear tripos.

However, it’s trickier to say exactly what the linear topos should be. The symmetric Ω\Omega-enriched categories (e.g. metric spaces) should clearly be its objects. But it’s unclear to me whether the linear logic of such objects can be recovered from the category of such in an analogous way to how the logic of a topos is determined by the subobjects in the topos, or whether we have to continue to regard the category of “Ω\Omega-sets” as equipped with a separate fibration of predicates.

Posted by: Mike Shulman on August 2, 2019 2:01 PM | Permalink | Reply to this

Re: Summer meanderings about enriched logic

Winding back further in the flow of thoughts, I was wondering a few weeks ago about the two senses taken on by the term ‘graded modality’. One that can traced back to the philosophers Goble and Fine in the early 70s, gives rise to graded modalities and more generally graded monads. The second approach from a similar time starts with the philosopher David Lewis, and looks to generalise predicates to take values in degrees. That’s what started me looking at continuous logic.

But perhaps these streams flow together. The unary operators vv \star and vv \rhd in the Babus and Kurz paper point in a graded modal direction.

Lewis is famous for his analysis of counterfactuals, “were A true, then B”, as stating that relative to this world, in the closest world(s) in which A holds, there B holds. So one needs something like a (generalised) metric space of worlds. Again a kind of enriched category as the collection of worlds/models.

Posted by: David Corfield on July 29, 2019 3:36 PM | Permalink | Reply to this

Re: Summer Meanderings About Enriched Logic

I just wanted to add briefly to this discussion by adding that there is still an unresolved tension in the “continuous semantics” examined in my paper, namely that continuous logic very much cares about what specific real number value a given predicate takes at each point, which is decidedly not isomorphism-invariant if you’re working in any flavor of the category of metric spaces which allows for distance-increasing morphisms such as uniformly continuous or Lipschitz maps (and continuous logic allows for uniformly continuous maps).

This is mostly fine for the purposes of the paper, but has e.g. the unpleasant aesthetic effect that a pullback of a specified metric in general has no special relationship to the metric of the domain of the map you’re pulling back across, aside from the same continuity condition required of all predicates. This is also the root cause for why one has to restrict to 1-Lipschitz maps when trying to apply the same framework to categories of presheaves of metric spaces.

Posted by: Simon Cho on August 11, 2019 6:05 AM | Permalink | Reply to this

Re: Summer Meanderings About Enriched Logic

But of course, that’s what you would expect from the general perspective that continuous logic is [0,][0,\infty]-enriched logic, since the functors between [0,][0,\infty]-enriched categories are 1-Lipschitz maps.

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

Re: Summer meanderings about enriched logic

More on syntax-semantics duality for continuous (infinitary) logic in metric situations just out

  • Ruiyuan Chen, Representing Polish groupoids via metric structures, (arXiv:1908.03268)
Posted by: David Corfield on August 12, 2019 10:24 AM | Permalink | Reply to this

Post a New Comment