In this chapter we study the axiomatization of classes of structures in (finitary and infinitary) first-order logic. We will show that locally presentable categories are precisely the categories of models of limit theories, and accessible categories are precisely the categories of models of basic theories. There is a substantial difference between those two cases: in the locally presentable case we can specialize to a given cardinal λ, and we see that locally λ-presentable categories are precisely the categories of models of limit theories in the λ-ary logic Lλ. Nothing like that is possible in the case of accessible categories: we will see that a finitely accessible category need not have an axiomatization in the finitary logic Lω, and that a basic theory in Lω need not have a finitely accessible category of models.

5.A Finitary Logic

Formulas, Models, and Satisfaction

Up to now, we have worked with many-sorted operations and many-sorted relations separately (see Example 1.2(4) and Chapter 3). We will now combine them: by a signature we will mean a set Σ of operation and relation symbols of prescribed arities. A Σ-structure A is, then, a many-sorted set together with appropriate operations and relations, and a homomorphism is an S-sorted function preserving the given operations and relations. Although infinitary logic is needed for general locally presentable categories, we start with the classical finitary (but many-sorted) first-order logic.

5.1. Σ-structures and homomorphisms. Let S be a set (of sorts). A finitary S-sorted signature is a set Σ = Σope ∪ Σrei with Σope and Σrei dis-joint.