Basic facts about first-order languages

Additions to Mathlib's Mathlib.ModelTheory.Basic.

Main results

• FirstOrder.Language.countable_functions_of_countable_sigma, FirstOrder.Language.countable_relations_of_countable_sigma: a language with countably many function or relation symbols in total has countably many of each arity.
• FirstOrder.Language.Countable.countable_relations: a language with countably many symbols has countably many relation symbols in total, complementing Mathlib's function-symbol instance.
• FirstOrder.Language.nonempty_structure_of_nonempty, FirstOrder.Language.nonempty_structure_of_isRelational: a type carries some L-structure when it is nonempty, and over any type when L is relational. On the empty type a constant symbol has no interpretation, so some such hypothesis is needed.

instance FirstOrder.Language.countable_functions_of_countable_sigma {L : Language} [Countable ((n : ℕ) × L.Functions n)] (n : ℕ) : Countable (L.Functions n)

A language with countably many function symbols has countably many of each arity.

instance FirstOrder.Language.countable_relations_of_countable_sigma {L : Language} [Countable ((n : ℕ) × L.Relations n)] (n : ℕ) : Countable (L.Relations n)

A language with countably many relation symbols has countably many of each arity.

instance FirstOrder.Language.Countable.countable_relations {L : Language} [Countable L.Symbols] : Countable ((n : ℕ) × L.Relations n)

A language with countably many symbols has countably many relation symbols in total.

instance FirstOrder.Language.nonempty_structure_of_nonempty {L : Language} (M : Type u_1) [Nonempty M] : Nonempty (L.Structure M)

A nonempty type carries some L-structure: Mathlib's Inhabited.trivialStructure for a chosen element.

instance FirstOrder.Language.nonempty_structure_of_isRelational {L : Language} [L.IsRelational] (M : Type u_1) : Nonempty (L.Structure M)

Every type, including the empty one, carries some structure for a relational language: make every relation empty.