Model theory

Relations between formal theories and their structures: first-order languages of algebraic structures, quantifier elimination, categoricity and o-minimality.

• First-order language of groups
• Quantifier elimination for real closed fields
• Wilkie's conjecture

TheoremMorley's categoricity theorem#●ready to prove

Let \(L\) be a first-order language with at most countably many symbols, and let \(T\) be a complete \(L\)-theory all of whose models are infinite. Call \(T\) \(\kappa\)-categorical if any two models of \(T\) of cardinality \(\kappa\) are isomorphic. If \(T\) is \(\kappa\)-categorical for some uncountable cardinal \(\kappa\), then \(T\) is \(\mu\)-categorical for every uncountable cardinal \(\mu\).

public theorem_wanted morley_categoricity_theorem
    (L : FirstOrder.Language.{0, 0}) (hL : L.card ≤ ℵ₀)
    (T : L.Theory) (hT : T.IsComplete)
    (hInf : ∀ M : FirstOrder.Language.Theory.ModelType.{0, 0, 0} T, Infinite M)
    {κ : Cardinal.{0}} (hκ : ℵ₀ < κ) (hcat : κ.Categorical T)
    {μ : Cardinal.{0}} (hμ : ℵ₀ < μ) :
    μ.Categorical T

Sources

• M. Ramsey, Morley's Categoricity Theorem (UChicago VIGRE REU 2010), Corollary 7.3. https://www.math.uchicago.edu/~may/VIGRE/VIGRE2010/REUPapers/RamseyN.pdf. Problem morley_categoricity_theorem of the lean-eval benchmark.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.