Skip to content

feat(ModelTheory): Add Morley's categoricity theorem #269

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
A-M-Berns wants to merge 1 commit into
base: main
Choose a base branch
from
+37 −0
Open

feat(ModelTheory): Add Morley's categoricity theorem #269

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 26 additions & 0 deletions LeanEval/ModelTheory/MorleyCategoricity.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
import Mathlib.ModelTheory.Satisfiability
import EvalTools.Markers

namespace LeanEval
namespace ModelTheory

open Cardinal

/-!
Morley's categoricity theorem.

A complete theory in a countable language, all of whose models are infinite, that is
categorical in some uncountable cardinal is categorical in every uncountable cardinal. -/

@[eval_problem]
theorem 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 := by
sorry

end ModelTheory
end LeanEval
11 changes: 11 additions & 0 deletions manifests/problems.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -673,3 +673,14 @@ module = "LeanEval.Geometry.Uniformization"
holes = ["uniformization"]
submitter = "Junyan Xu"
source = "John Hamal Hubbard, *Teichmüller theory and applications to geometry, topology, and dynamics. Vol. 1*, Chapter 1."

[[problem]]
id = "morley_categoricity_theorem"
title = "Morley's categoricity theorem"
test = false
module = "LeanEval.ModelTheory.MorleyCategoricity"
holes = ["morley_categoricity_theorem"]
submitter = "A. M. Berns"
notes = "A complete theory in a countable language with only infinite models that is categorical in some uncountable cardinal is categorical in every uncountable cardinal."
source = "M. Ramsey, *Morley's Categoricity Theorem* (UChicago VIGRE REU 2010), Corollary 7.3. https://www.math.uchicago.edu/~may/VIGRE/VIGRE2010/REUPapers/RamseyN.pdf"
informal_solution = "Show that categoricity in an uncountable cardinal forces the theory to be ω-stable, and then use Vaughtian pairs to prove that any two models of the same uncountable size are isomorphic and categoricity transfers to all uncountable cardinals."
Loading