Saturation of Ultraproducts?

Stream: Is there code for X?

[Keith J. Bauer]

I was looking for small things to do to practice using Mathlib's model theory library, and I realized that (at least to my knowledge) there are no theorems about saturation. Now I am interested in seeing if I can contribute some small theorems about saturation to Mathlib. But before I set my sights on that, I want to make sure I am not duplicating existing work. Here is what I have written so far, it is an implementation of the statement of the theorem "countably incomplete ultraproducts over structures with countable languages are w_1-saturated":

import Mathlib
open FirstOrder

class CountablyIncompleteUltrafilter (α : Type) where
  u : Ultrafilter α
  chain (n : Nat) : Set α
  is_chain (m n : Nat) (h : m ≤ n) : chain n ⊆ chain m
  chain_in_u (n : Nat) : chain n ∈ u
  inter_empty (a : α) : ∃n : Nat, a ∉ chain n

class SatisfiableFormulaChain (L : Language) (M : Type) extends L.Structure M where
  chain (n : Nat) : Language.BoundedFormula L _ 1
  is_chain (m n : Nat) (h : m ≤ n) : M ⊨ ∀' (chain n ⟹ chain m)
  satisfiable (n : Nat) : M ⊨ ∃' chain n

variable (α : Type) (u : Ultrafilter α) (L : Language) (M : α → Type) [(a : α) → L.Structure (M a)]
instance : L.Structure (u.Product M) := Language.Ultraproduct.structure
theorem ultraproduct_saturation
  [CountablyIncompleteUltrafilter α]
  [SatisfiableFormulaChain L (u.Product M)] :
  ∃x : u.Product M, ∀n : Nat, Language.BoundedFormula.Realize
  (@SatisfiableFormulaChain.chain L (u.Product M) _ n) (fun _ ↦ x) (fun _ ↦ x) :=
  sorry

Some notes:

• I am not sure how I would easily go about enumerating every formula with countably many parameters, so I abstracted some of the early steps of the proof to just be structure that is provided to the theorem itself.
• I couldn't find an implementation of kappa-completeness of ultrafilters, so i came up with my own ad-hoc implementation.
• I suspect that some of my code is janky because of the @ sign code smell, but I'm still relatively inexperienced with Lean so I'm not sure how I'd fix this.
• I have not worked towards proving this yet, so I may update this post later with details on that, especially if I somehow bungled something that makes this an untrue theorem as stated.

[Aaron Anderson]

One can describe saturation in terms of all types in languages with additional constants being realized. Realized types are defined in docs#FirstOrder.Language.Theory.realizedTypes

[Keith J. Bauer]

@Aaron Anderson How would one go about proving that there are countably many formulae in a complete type over a countable language? Does such a theorem have an easy solution via Mathlib?

[Aaron Anderson]

The critical idea is here: docs#FirstOrder.Language.BoundedFormula.card_le

[Aaron Anderson]

You can get countability from a little bit of cardinal arithmetic from there.

[Keith J. Bauer]

Whoa, that's really cool. I blame my unfamiliarity with Lean's cardinality library, but that design choice makes sense.

[Keith J. Bauer]

I think it will be good practice for me (in using these types of theorems in Lean) to formalize the saturation of ultraproducts theorem using these library calls.

[Keith J. Bauer]

I suppose for completeness (no pun intended), is there a standard way to refer to countably incomplete ultrafilters?

[Aaron Liu]

are you talking about (the negation of) docs#CountableInterFilter

[Keith J. Bauer]

Yes! I didn't think to check the Filter library, although I probably would have missed it because I wouldn't have known the right search terms.