From 9fddce7f23b6785a9e56a077521b7e8269b7adf9 Mon Sep 17 00:00:00 2001 From: Vaibhav Karve Date: Thu, 11 Mar 2021 18:01:59 -0600 Subject: [PATCH 1/9] lint --- src/model.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/model.lean b/src/model.lean index c985e83..87ddf04 100644 --- a/src/model.lean +++ b/src/model.lean @@ -681,7 +681,7 @@ begin left, split, rotate, - use function.const ℕ (default M.univ), + use function.const ℕ (arbitrary M.univ), cases σ₁, repeat {sorry}, end From 577483b6dbac719447def22b7c77b66397799225 Mon Sep 17 00:00:00 2001 From: Vaibhav Karve Date: Thu, 11 Mar 2021 18:02:07 -0600 Subject: [PATCH 2/9] remove variable assignment from definition of complete theory --- src/model.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/model.lean b/src/model.lean index 87ddf04..41daaba 100644 --- a/src/model.lean +++ b/src/model.lean @@ -745,8 +745,7 @@ def coeset : set(sentence L) → set(formula L) := set.image coe /-- A theory is complete if any pair of models satisfies exactly the same sentences.-/ structure complete_theory (t : theory L) := -(has_model : ∃ (A : struc L), ∀ (va : ℕ → A.univ), ∀ (σ ∈ t), - va ⊨ ↑σ) +(has_model : ∃ (A : struc L), ∀ (σ ∈ t), A ⊨ σ) (models_iff_models : ∀ (A₁ A₂ : Model t), ∀ (σ ∈ t), A₁.M ⊨ σ ↔ A₂.M ⊨ σ) From 786b1d8ef22a0f92d3fe558a6aa006da2cfaff85 Mon Sep 17 00:00:00 2001 From: Vaibhav Karve Date: Thu, 11 Mar 2021 18:02:30 -0600 Subject: [PATCH 3/9] add instance for nonempty universe of theory with infinite model --- src/model.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/model.lean b/src/model.lean index 41daaba..593f12d 100644 --- a/src/model.lean +++ b/src/model.lean @@ -764,6 +764,12 @@ class has_infinite_model (t : theory L) : Type 1 := (big : cardinal.omega ≤ μ.card) +instance nonempty_universe_of_theory_with_infinite_model + (t : theory L) [h : has_infinite_model t] : nonempty h.μ.M.univ := + by { haveI infinite_univ := cardinal.infinite_iff.mpr h.big, + inhabit h.μ.M.univ, + apply infinite.nonempty, + } /-- Lowenheim-Skolem asserts that for a theory over a language L, if that theory has an infinite model, then it has a model for any cardinality greater than From 4ae51855bd71f8889b97cd990851a3199236745b Mon Sep 17 00:00:00 2001 From: Vaibhav Karve Date: Thu, 11 Mar 2021 18:03:56 -0600 Subject: [PATCH 4/9] add noncomputable instance: inhabited univ of theory infinite model --- src/model.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/model.lean b/src/model.lean index 593f12d..01b261c 100644 --- a/src/model.lean +++ b/src/model.lean @@ -771,6 +771,14 @@ instance nonempty_universe_of_theory_with_infinite_model apply infinite.nonempty, } + +noncomputable instance inhabited_universe_of_theory_with_infinite_model + (t : theory L) [h : has_infinite_model t] : inhabited h.μ.M.univ := + {default := by {inhabit h.μ.M.univ, + exact arbitrary h.μ.M.univ} + } + + /-- Lowenheim-Skolem asserts that for a theory over a language L, if that theory has an infinite model, then it has a model for any cardinality greater than or equal to |L|-/ From 4e01426ba2f643fed6f3c793e7c51b3506221964 Mon Sep 17 00:00:00 2001 From: Vaibhav Karve Date: Thu, 11 Mar 2021 18:05:36 -0600 Subject: [PATCH 5/9] change def of k-categorical theory to yield inhabited isomorphism Previously, this definition yielded nonempty isomorphism instead --- src/model.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/model.lean b/src/model.lean index 01b261c..b2d2043 100644 --- a/src/model.lean +++ b/src/model.lean @@ -789,7 +789,7 @@ axiom LS_Lou (k : cardinal) (h : L.card ≤ k) (t : theory L) [has_infinite_mode /- A theory is k-categorical if all models of cardinality k are isomorphic as structures.-/ def theory_kcategorical (k : cardinal) (t : theory L) := - ∀ (M₁ M₂ : Model t), M₁.card = k ∧ M₂.card = k → nonempty (isomorphism M₁.M M₂.M) + ∀ (M₁ M₂ : Model t), M₁.card = k ∧ M₂.card = k → inhabited (isomorphism M₁.M M₂.M) From d776ed0cff680c6e9575602f0411aabb4952bf9c Mon Sep 17 00:00:00 2001 From: Vaibhav Karve Date: Thu, 11 Mar 2021 18:15:48 -0600 Subject: [PATCH 6/9] add instances has_union, has_mem for type (theory L) --- src/model.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/model.lean b/src/model.lean index b2d2043..2e0a39d 100644 --- a/src/model.lean +++ b/src/model.lean @@ -690,7 +690,10 @@ end /-- An `L`-theory `T` is simply a set of `L`-sentences. We say that `M` is a model of `T` and write `M ⊨ T` if `M ⊨ φ` for all sentences `φ ∈ T`.-/ def theory (L : lang) : Type := set (sentence L) + instance theory.has_mem : has_mem (sentence L) (theory L) := ⟨set.mem⟩ +instance theory.has_union : has_union (theory L) := set.has_union +instance theory.has_singleton : has_singleton (sentence L) (theory L) := set.has_singleton /-- We now define a model to be a structure that models a set of sentences From 531ba3cbadd0cd160ab6ba3ca6914991282cc752 Mon Sep 17 00:00:00 2001 From: Vaibhav Karve Date: Thu, 11 Mar 2021 18:22:59 -0600 Subject: [PATCH 7/9] add def for model of theory set extended by an addition sentence --- src/model.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/model.lean b/src/model.lean index 2e0a39d..c27fe7e 100644 --- a/src/model.lean +++ b/src/model.lean @@ -795,6 +795,12 @@ def theory_kcategorical (k : cardinal) (t : theory L) := ∀ (M₁ M₂ : Model t), M₁.card = k ∧ M₂.card = k → inhabited (isomorphism M₁.M M₂.M) +def model_of_extended {t : theory L} {μ : Model t} {σ : sentence L} (sat_σ: μ.M ⊨ σ) : + Model (t ∪ {σ}) := +begin + sorry, +end + /-- If a theory is k-categorical and has an infinite model, it is complete.-/ From 93772b096521d3d448e381457996a72d3ffba737 Mon Sep 17 00:00:00 2001 From: Vaibhav Karve Date: Thu, 11 Mar 2021 18:23:38 -0600 Subject: [PATCH 8/9] partial progress on proof of Vaught's theorem --- src/model.lean | 25 ++++++++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) diff --git a/src/model.lean b/src/model.lean index c27fe7e..d71a176 100644 --- a/src/model.lean +++ b/src/model.lean @@ -814,7 +814,30 @@ begin -- M₃ and M₄ both model T. -- But by kcategoricity, M₃ and M₄ are isomorphic. -- Achieve a contradiction using isomorphic_struc_satisfy_same_theory. - + fconstructor, + { use _inst_1.μ.M, + intros σ hσ, + cases _inst_1.μ, + simp, + apply satis, + assumption, +}, +intros μ₁ μ₂ σ hσ, +split, +intro hM₁, +unfold theory_kcategorical at hkc, +--by_contradiction not_satis, + + +by_cases same_card : (μ₁.card = k) ∧ (μ₂.card = k), +{ + have x := hkc μ₁ μ₂ same_card, + exact isomorphic_struc_satisfy_same_theory μ₁.M μ₂.M (x.default) σ hM₁, + }, +have LS := LS_Lou k h, +by_contradiction, +push_neg at same_card, +sorry, sorry, end From 0762b9d2a4cb6d5d7c0154d21eb6d31c8ebd30df Mon Sep 17 00:00:00 2001 From: Vaibhav Karve Date: Thu, 11 Mar 2021 18:23:56 -0600 Subject: [PATCH 9/9] clean up def extension_of_isomorphism --- src/model.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/model.lean b/src/model.lean index d71a176..394f19a 100644 --- a/src/model.lean +++ b/src/model.lean @@ -845,8 +845,8 @@ def extend_struc_by_element : sorry := sorry def extension_of_isomorphism (t : theory L) (M₁ M₂ : Model t) : - ∀ (S₁ : substruc M₁.M) (S₂ : substruc M₂.M) [fin_substruc S₁] [fin_substruc S₂] - (η : isomorphism S₁ S₂), + ∀ (S₁ : substruc M₁.M) (S₂ : substruc M₂.M) [fin_substruc S₁] [fin_substruc S₂], + ∀ (η : @isomorphism L ↑S₁ ↑S₂), ∀ (m : M₁.M.univ), ∃ (m': M₂.M.univ), ∃ (η' : extend_struc_by_element S₁ m → extend_struc_by_element S₂ m'), η' is_isomorphism ∧ (η' m = m') ∧ (η = η' on S₁)