Vaught conjecture

Conjecture · vaught_conjecture

The Vaught conjecture states that for a countable language L and a complete L-Theory T the number of countable models of T (up to isomorphism) is finite, $\aleph_0$ or $2^{\aleph_0}$ .

Formal statement · Lean 4.lean

theorem vaught_conjecture {L : FirstOrder.Language} (hL : Countable L.Symbols)
                          {T : L.Theory} (hT : T.IsComplete) :
  numberOfCountableModels T ≤ Cardinal.aleph0 ∨ numberOfCountableModels T = Cardinal.continuum := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗