You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Fawzi Hreiki (Mar 09 2021 at 11:17):I've been learning about density and I can't help but notice the analogy with completeness theorems in logic - I was hoping this could be made precise in some way.
For example, any small category can be regarded as a diagrammatic theory (just sorts and function symbols) and the UMP of the Yoneda embedding tells us that is dense in its category of models. Likewise, any Lawvere theory is dense in its category of algebras. More generally, the Kleisli category of any monad is dense in the Eilenberg-Moore category. When the monad has arities, the free algebras on just those arities are dense in the Eilenberg-Moore category (e.g. how the first three walking ordinals are dense in ).
These could all be seen as 'completeness theorems'. Can this be extended to other forms of logic (e.g. regular, geometric, etc...) and how does this connect to the traditional formulation of the completeness theorem (if a statement is true in all models then its true from the theory).
John Baez (Mar 09 2021 at 15:52):That's an interesting question. I guess to extend the idea one wants to get a "purely syntactic" model of a theory where the model is built directly from the theory itself.
Morgan Rogers (he/him) (Mar 09 2021 at 15:53):Sounds like a universal model to me :+1:
Morgan Rogers (he/him) (Mar 09 2021 at 15:58):This is exactly how the completeness theorems work in categorical logic. You have a syntactic category carrying the universal model (interpret sorts as themselves etc), a class of categories with enough structure to carry models of/interpret the theory, and functors between these preserving the structure required to interpret the theory, so that a model is the image under such a functor of the universal model.
Then the completeness theorem has a trivial version which says "true in all models iff provable in the theory" because the syntactic category carries the universal model, but non-trivial completeness results such as "true in all set-models iff provable in the theory" are recovered as soon as there are 'enough' Set-models for the corresponding functors to be jointly conservative.
John Baez (Mar 09 2021 at 16:02):Nice.
Fawzi Hreiki (Mar 09 2021 at 16:09):Morgan Rogers (he/him) said:
This is exactly how the completeness theorems work in categorical logic. You have a syntactic category carrying the universal model (interpret sorts as themselves etc), a class of categories with enough structure to carry models of/interpret the theory, and functors between these preserving the structure required to interpret the theory, so that a model is the image under such a functor of the universal model.
Then the completeness theorem has a trivial version which says "true in all models iff provable in the theory" because the syntactic category carries the universal model, but non-trivial completeness results such as "true in all set-models iff provable in the theory" are recovered as soon as there are 'enough' Set-models for the corresponding functors to be jointly conservative.
Sure I know that, but I was wondering if (assuming completeness) this syntactic category always embeds/maps densely into the category of models
Morgan Rogers (he/him) (Mar 09 2021 at 16:11):Unfortunately not, that's kind of a special feature of essentially algebraic theories
Fawzi Hreiki (Mar 09 2021 at 16:13):Yeah that makes sense I suppose, since the hom-functor need not be regular/geometric/etc.. so we usually don't get a 'copy' of the theory in the category of models
Morgan Rogers (he/him) (Mar 09 2021 at 16:15):If you're aware of Caramello's book, her approach is to embed the classifying topos of a given theory into a presheaf topos, in part because what you're saying is true of theories of presheaf type (geometric theories classified by presheaf toposes)
Fawzi Hreiki (Mar 09 2021 at 16:16):I've only briefly glanced at the book but I'll check that section out. Thanks