In this chapter, we use first-order logic to build by formal definitions higher-level concepts from more fundamental ones; in particular, we present the types and operations that are essential for the construction of mathematical models. We start with a general explanation of how we can introduce mathematical theories from scratch by characterizing their fundamental entities via logical axioms; on top of these we can later introduce other entities by explicit definitions.