Countability of infinitary syntax

With countably many variables and countably many function and relation symbols, the atomic infinitary formulas form a countable type, as for Mathlib's finitary terms in Mathlib.ModelTheory.Encoding.

Main results

• FirstOrder.Language.BoundedFormulaInf.countable_subtype_isAtomic: there are countably many atomic formulas.

instance FirstOrder.Language.BoundedFormulaInf.countable_subtype_isAtomic {L : Language} {ι : Type w} {α : Type u'} {n : ℕ} [Countable α] [Countable ((l : ℕ) × L.Functions l)] [Countable ((l : ℕ) × L.Relations l)] : Countable { φ : L.BoundedFormulaInf ι α n // φ.IsAtomic }

With countably many variables and countably many function and relation symbols, there are countably many atomic formulas.