Vaught conjecture

Reference: Wikipedia

def VaughtConjecture.numberOfCountableModels {L : FirstOrder.Language} (T : L.Theory) : Cardinal.{max (max u_2 u_1) (u_3 + 1)}

The number of countable models of some L-Theory T up to isomorphism

Equations

• One or more equations did not get rendered due to their size.

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

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}$.