The n-Category Café

I’m confused. There are different quantales on $[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, \infty]$ is equivalent to the one on $[0,1]$ (via the map $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.

Well, the general stuff about quantales will apply to any such. Łukasiewicz logic is the one on $[0,1]$ obtained by reflection as a subcategory of $[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))$ and $([0,\infty],+)$ a bit, but both have $\overset{\cdot}{-}$ as their $\multimap$. In the latter case the computation would instead be

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

since $x\ge 0$.

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.

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 $V$-enriched categories is not in general itself a $V$-category (it’s a $V$-2-category).

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 $Lex$ and $LFP$, 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), $\mathbf{2}$ is replaced by $[0, \infty]$ or $[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, \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.

Since we have a quantale map from truth values to $[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., $Lex$ and $Lfp$, 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.

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 $Set$). So here, you mean models of a $\Omega$-theory in $\Omega$ itself, i.e. functors to $\Omega$ from the Lindenbaum algebra $T$, and so the functor category $Lex(T,\Omega)$ is again an $\Omega$-enriched category.