mathlib3

812518d9 - feat(model_theory/semantics, satisfiability): Complete Theories (#13558)

feat(model_theory/semantics, satisfiability): Complete Theories (#13558) Defines `first_order.language.Theory.is_complete`, indicating that a theory is complete. Defines `first_order.language.complete_theory`, the complete theory of a structure. Shows that the complete theory of a structure is complete.