9
$\begingroup$

There is a duality between locally strongly finitely presentable (LSFP) categories and (Cauchy complete) cartesian categories, i.e. multisorted algebraic theories [1]. The internal logic of cartesian categories is well known to be first-order equational logic. What is the internal logic of locally strongly finitely presentable categories? It should at least subsume "exact logic" (i.e. have finite conjunction, existential quantification, and quotients of equivalence relations), since the category of models for any multisorted algebraic theory is exact. However, it may not be describable as fragment of first-order logic, because although there exist arbitrary disjunctions, conjunction does not distributive over disjunction.

Edited in 2024. The original motivation for this question was to better understand the relationship between syntax and semantics. Cartesian categories have a well understood internal logic, but form a duality with a class of categories with (seemingly) much more structure. In theory, these should be described by a different internal language, and the duality between the two classes of categories (cartesian and LSFP) should then express some kind of equi-expressibility result between the respective logics, which could lend syntactic insight into the relationship between the two fragments of logic.

[1] On the duality between varieties and algebraic theories, J. Adámek, F.W. Lawvere & J. Rosický.

Improve this question
$\endgroup$
22
  • 2
    $\begingroup$ Ah yes you are right, I forgot they were always regular, so you do get existential quantification. In fact they are exact categories, so you also get quotient by equivalence relations internally. It is not clear to me you'll get much more than that though: so far I see no other good properties of these categories might not transpire in the internal logic, as a property needs to have some form of pullback stability to have an internal interpretation. But maybe I'm missing something... $\endgroup$
    – Simon Henry
    Commented Feb 9, 2021 at 15:59
  • 1
    $\begingroup$ It is going to be Barr exact, via monadicity. I think you can't say more than this. $\endgroup$
    – Ivan Di Liberti
    Commented Feb 9, 2021 at 16:01
  • 3
    $\begingroup$ For one thing, the more expressive the external logic, the more general the categories, so the weaker the corresponding internal logic will be. So if there were a general link between the properties of the external specifying logic and the interpretable internal logic, it would establish some kind of duality between highly expressive and highly restricted logics. I think it would be remarkable to discover such a duality. Sorry if I'm distracting from the specific question at hand! $\endgroup$
    – Tim Campion
    Commented Feb 9, 2021 at 16:07
  • 5
    $\begingroup$ The problem is that internal logic (even extended far beyind first order logic) can only talk about pullback stable properties. There is no reason you can arrive at a characterization of some class of categories only by pullback stable properties. However, something encouraging : if $C$ is a category of model of a multisorted algebraic theory, then any slice of $C$ is also a category of model of a multisorted algebraic theory. So that's a starting point... $\endgroup$
    – Simon Henry
    Commented Feb 9, 2021 at 16:12
  • 5
    $\begingroup$ A characterisation of algebraically exact categories was achieved by Garner in arxiv.org/pdf/1109.0106.pdf. $\endgroup$
    – Jiří Rosický
    Commented Feb 10, 2021 at 12:31

1 Answer 1

Reset to default
4
$\begingroup$

The comments are getting a bit long (sorry, that is largely my fault), so I think it's worth expanding on Jiří Rosický 's point, which comes very close to completely answering the question.

Adamek, Lawvere, and Rosicky introduced the notion of an algebraically exact category in How algebraic is algebra?, giving a precise definition of what it means for a category to have all of the "exactness" properties enjoyed by (possibly multisorted) varieties (= algebraic categories = locally strongly finitely-presentable) categories. The definition is conceptually illuminating: the forgetful functor $Var \to Cat$ has a left adjoint, and an algebraically exact category is defined to be a pseudoalgebra for the induced pseudomonad on $Cat$.

They observed that every algebraically exact category $\mathcal C$ has the following properties:

  • $\mathcal C$ has limits.

  • $\mathcal C$ has sifted colimits.

  • $\mathcal C$ is Barr-exact.

  • finite limits commute with filtered colimits in $\mathcal C$.

  • regular epimorphisms are stable under products in $\mathcal C$.

  • filtered colimits distribute over products in $\mathcal C$.\

  • (This one must apparently follow from the rest: regular epis are stable under pullback.)

They conjectured that these properties completely characterize the algebraically exact categories. This conjecture was proven under various additional assumptions by these and other authors, until it was finally proven in full generality by Garner in A characterization of algebraic exactness (see Garner for a full bibliography).

Upshot: It would seem the appropriate internal logic would be "whatever you can express using the above properties". In particular, Barr-exactness gives a good fragment of logic. Stability of regular epis under pullback probably lets you do a reasonable amount more. Perhaps others can elaborate on / correct these statements.

Side note: I would assume that only the "finitary" fragment of the above properties would be relevant to building an internal logic as it's usually conceived. I would be interested to be proven wrong about that though!

Improve this answer
$\endgroup$
6
  • $\begingroup$ I'm a bit confused because in his abstract, Garner states the characterization slightly differently than in the body of the paper. He includes the condition that the "take the sifted colimit" functor be continuous, which I thought was equivalent to sifted colimits commuting with all limits, which seems too strong. Perhaps the point is that limits in $Sind(C)$ are not computed "levelwise" when objects are viewed as diagrams in $C$ indexed by sifted categories? $\endgroup$
    – Tim Campion
    Commented Feb 10, 2021 at 16:40
  • 2
    $\begingroup$ Asking for $\mathrm{Sind}(\mathbf C) \to \mathbf C$ to be continuous is equivalent to asking for small limits to distribute over sifted colimits. (This is mentioned in How algebraic is algebra?.) $\endgroup$
    – varkor
    Commented Feb 10, 2021 at 16:50
  • $\begingroup$ Presumably there's one extra condition on the internal logic for LSFP categories, on top of that for algebraically exact categories, viz. some freeness condition on the sifted colimits, but this seems like a mostly inconsequential detail: if one is interesting in reasoning in a LSFP category, it should be enough to consider it simply as an algebraically exact category. $\endgroup$
    – varkor
    Commented Feb 10, 2021 at 16:54
  • $\begingroup$ @varkor Thanks for clearing up my confusion! Maybe the Barr-exactness and product-stability of regular epis are saying something about freeness. But I agree, the full force of freeness is basically what differentiates algebraic categories from algebraically-exact ones. I'd say the full force of freeness is a global property of the category, whereas internal logic relies on local properties of objects in the category." $\endgroup$
    – Tim Campion
    Commented Feb 10, 2021 at 17:02
  • $\begingroup$ By analogy, even the internal logic of $Set$ doesn't allow you to express anything with unbounded quantifiers; freeness as such feels like it would need an unbounded quantifier to express (EDIT: and maybe even quantification over "classes"?). Maybe something like Mike Shulman's stack semantics allows to express unbounded quantification? $\endgroup$
    – Tim Campion
    Commented Feb 10, 2021 at 17:02

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .