Finitely Generated First-Order Structures #
This file defines what it means for a first-order (sub)structure to be finitely or countably generated, similarly to other finitely-generated objects in the algebra library.
Main Definitions #
FirstOrder.Language.Substructure.FGindicates that a substructure is finitely generated.
FirstOrder.Language.Structure.FGindicates that a structure is finitely generated.
FirstOrder.Language.Substructure.CGindicates that a substructure is countably generated.
FirstOrder.Language.Structure.CGindicates that a structure is countably generated.
Develop a more unified definition of finite generation using the theory of closure operators, or use this definition of finite generation to define the others.