Categorical abstract algebraic logic: The largest theory system included in a theory family

In this note, it is shown that, given a π ‐institution ℐ = 〈 Sign , SEN, C 〉, with N a category of natural transformations on SEN, every theory family T of ℐ includes a unique largest theory system $ \overleftarrow T $ of ℐ. $ \overleftarrow T $ satisfies the important property that its N ‐Leibniz congruence system always includes that of T . As a consequence, it is shown, on the one hand, that the relation Ω N ( $ \overleftarrow T $ ) = Ω N ( T ) characterizes N ‐protoalgebraicity inside the class of N ‐prealgebraic π ‐institutions and, on the other, that all N ‐Leibniz theory families associated with theory families of a protoalgebraic π ‐institution ℐ are in fact N ‐Leibniz theory systems. (© 2006 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)