nLab empty theory

The empty theory is the theory with no sorts (and therefore no functions or relations) and no axioms. This can be formulated in any doctrine: there is an empty algebraic theory, an empty essentially algebraic theory, an empty first-order theory, and so on.

Each empty theory has a unique model in any category of the sort appropriate to the doctrine. Its classifying category is the initial object of the category of such categories. For instance, the classifying topos of the empty geometric theory is the terminal (since geometric morphisms of toposes are backwards from the “logical” direction) Grothendieck topos Set.