feat(model_theory/*): Facts about countability of first-order structu…

…res (#12819)

Shows that in a countable language, a structure is countably generated if and only if it is countable.

src/data/equiv/encodable/basic.lean

@@ -90,8 +90,8 @@ instance nat : encodable ℕ :=
 @[simp] theorem encode_nat (n : ℕ) : encode n = n := rfl
 @[simp] theorem decode_nat (n : ℕ) : decode ℕ n = some n := rfl
 
-instance empty : encodable empty :=
-⟨λ a, a.rec _, λ n, none, λ a, a.rec _⟩
+@[priority 100] instance is_empty [is_empty α] : encodable α :=
+⟨is_empty_elim, λ n, none, is_empty_elim⟩
 
 instance unit : encodable punit :=
 ⟨λ_, 0, λ n, nat.cases_on n (some punit.star) (λ _, none), λ _, by simp⟩

src/model_theory/basic.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson, Jesse Michael Han, Floris van Doorn
 -/
 import data.fin.tuple.basic
+import data.equiv.encodable.basic
+import set_theory.cardinal
 import category_theory.concrete_category.bundled
 
 /-!
@@ -45,6 +47,9 @@ the continuum hypothesis*][flypitch_itp]
 -/
 universes u v u' v' w
 
+open_locale cardinal
+open cardinal
+
 namespace first_order
 
 /-! ### Languages and Structures -/
@@ -74,6 +79,14 @@ variable (L : language.{u v})
 /-- The type of symbols in a given language. -/
 @[nolint has_inhabited_instance] def symbols := (Σl, L.functions l) ⊕ (Σl, L.relations l)
 
+/-- The cardinality of a language is the cardinality of its type of symbols. -/
+def card : cardinal := # L.symbols
+
+/-- A language is countable when it has countably many symbols. -/
+class countable : Prop := (card_le_omega' : L.card ≤ ω)
+
+lemma card_le_omega [L.countable] : L.card ≤ ω := countable.card_le_omega'
+
 /-- A language is relational when it has no function symbols. -/
 class is_relational : Prop :=
 (empty_functions : ∀ n, is_empty (L.functions n))
@@ -82,8 +95,20 @@ class is_relational : Prop :=
 class is_algebraic : Prop :=
 (empty_relations : ∀ n, is_empty (L.relations n))
 
+/-- A language is countable when it has countably many symbols. -/
+class countable_functions : Prop := (card_functions_le_omega' : # (Σl, L.functions l) ≤ ω)
+
+lemma card_functions_le_omega [L.countable_functions] :
+  # (Σl, L.functions l) ≤ ω :=
+countable_functions.card_functions_le_omega'
+
 variables {L} {L' : language.{u' v'}}
 
+lemma card_eq_card_functions_add_card_relations :
+  L.card = cardinal.lift.{v} (# (Σl, L.functions l)) +
+    cardinal.lift.{u} (# (Σl, L.relations l)) :=
+by rw [card, symbols, mk_sum]
+
 instance [L.is_relational] {n : ℕ} : is_empty (L.functions n) := is_relational.empty_functions n
 
 instance [L.is_algebraic] {n : ℕ} : is_empty (L.relations n) := is_algebraic.empty_relations n
@@ -106,6 +131,33 @@ instance is_relational_sum [L.is_relational] [L'.is_relational] : is_relational
 instance is_algebraic_sum [L.is_algebraic] [L'.is_algebraic] : is_algebraic (L.sum L') :=
 ⟨λ n, sum.is_empty⟩
 
+lemma encodable.countable [h : encodable L.symbols] :
+  L.countable :=
+⟨cardinal.encodable_iff.1 ⟨h⟩⟩
+
+instance countable_empty : language.empty.countable :=
+⟨begin
+  rw [card_eq_card_functions_add_card_relations, add_le_omega, lift_le_omega, lift_le_omega,
+    ← cardinal.encodable_iff, ← cardinal.encodable_iff],
+  exact ⟨⟨encodable.sigma⟩, ⟨encodable.sigma⟩⟩,
+end⟩
+
+@[priority 100] instance countable.countable_functions [L.countable] :
+  L.countable_functions :=
+⟨begin
+  refine lift_le_omega.1 (trans _ L.card_le_omega),
+  rw [card, symbols, mk_sum],
+  exact le_self_add,
+end⟩
+
+lemma encodable.countable_functions [h : encodable (Σl, L.functions l)] :
+  L.countable_functions :=
+⟨cardinal.encodable_iff.1 ⟨h⟩⟩
+
+@[priority 100] instance is_relational.countable_functions [L.is_relational] :
+  L.countable_functions :=
+encodable.countable_functions
+
 variables (L) (M : Type w)
 
 /-- A first-order structure on a type `M` consists of interpretations of all the symbols in a given

src/model_theory/finitely_generated.lean

@@ -128,7 +128,7 @@ end
 
 theorem cg_bot : (⊥ : L.substructure M).cg := fg_bot.cg
 
-theorem cg_closure {s : set M} (hs : countable s) : cg (closure L s) :=
+theorem cg_closure {s : set M} (hs : s.countable) : cg (closure L s) :=
 ⟨s, hs, rfl⟩
 
 theorem cg_closure_singleton (x : M) : cg (closure L ({x} : set M)) := (fg_closure_singleton x).cg
@@ -157,6 +157,14 @@ begin
   exact hom.map_le_range h'
 end
 
+theorem cg_iff_countable [L.countable_functions] {s : L.substructure M} :
+  s.cg ↔ nonempty (encodable s) :=
+begin
+  refine ⟨_, λ h, ⟨s, h, s.closure_eq⟩⟩,
+  rintro ⟨s, h, rfl⟩,
+  exact h.substructure_closure L
+end
+
 end substructure
 
 open substructure
@@ -217,6 +225,11 @@ begin
   exact h.range f,
 end
 
+lemma cg_iff_countable [L.countable_functions] :
+  cg L M ↔ nonempty (encodable M) :=
+by rw [cg_def, cg_iff_countable, cardinal.encodable_iff, cardinal.encodable_iff,
+  top_equiv.to_equiv.cardinal_eq]
+
 lemma fg.cg (h : fg L M) : cg L M :=
 cg_def.2 (fg_def.1 h).cg
 

src/model_theory/substructures.lean

@@ -262,7 +262,18 @@ begin
   rw [mk_sum, lift_umax', lift_umax],
 end
 
-variable (S)
+variable (L)
+
+lemma _root_.set.countable.substructure_closure
+  [L.countable_functions] (h : s.countable) :
+  nonempty (encodable (closure L s)) :=
+begin
+  haveI : nonempty (encodable s) := h,
+  rw [encodable_iff, ← lift_le_omega],
+  exact lift_card_closure_le_card_term.trans term.card_le_omega,
+end
+
+variables {L} (S)
 
 /-- An induction principle for closure membership. If `p` holds for all elements of `s`, and
 is preserved under function symbols, then `p` holds for all elements of the closure of `s`. -/

src/model_theory/terms_and_formulas.lean

@@ -150,6 +150,14 @@ instance [encodable α] [encodable ((Σ i, L.functions i))] [inhabited (L.term 
 encodable.of_left_injection list_encode (λ l, (list_decode l).head')
   (λ t, by rw [← bind_singleton list_encode, list_decode_encode_list, head'])
 
+lemma card_le_omega [h1 : nonempty (encodable α)] [h2 : L.countable_functions] :
+  # (L.term α) ≤ ω :=
+begin
+  refine (card_le.trans _),
+  rw [add_le_omega, mk_sum, add_le_omega, lift_le_omega, lift_le_omega, ← encodable_iff],
+  exact ⟨⟨h1, L.card_functions_le_omega⟩, refl _⟩,
+end
+
 instance inhabited_of_var [inhabited α] : inhabited (L.term α) :=
 ⟨var default⟩