diff --git a/FormalTextbookModelTheory.lean b/FormalTextbookModelTheory.lean index 3c10936..d686522 100644 --- a/FormalTextbookModelTheory.lean +++ b/FormalTextbookModelTheory.lean @@ -1,2 +1,3 @@ -import FormalTextbookModelTheory.ForMathlib.Matrix -import FormalTextbookModelTheory.ForMathlib.DLO +import FormalTextbookModelTheory.ForMathlib.Data.Fin.VecNotation +import FormalTextbookModelTheory.ForMathlib.ModelTheory.Order +import FormalTextbookModelTheory.ForMathlib.ModelTheory.DLO diff --git a/FormalTextbookModelTheory/ForMathlib/DLO.lean b/FormalTextbookModelTheory/ForMathlib/DLO.lean deleted file mode 100644 index 0b7a2e9..0000000 --- a/FormalTextbookModelTheory/ForMathlib/DLO.lean +++ /dev/null @@ -1,246 +0,0 @@ -import Mathlib.SetTheory.Cardinal.Basic -import Mathlib.ModelTheory.Basic -import Mathlib.ModelTheory.Syntax -import Mathlib.ModelTheory.Semantics -import Mathlib.ModelTheory.Satisfiability -import Mathlib.ModelTheory.Bundled -import Mathlib.ModelTheory.Order -import Mathlib.Order.CountableDenseLinearOrder - -import FormalTextbookModelTheory.ForMathlib.Matrix - - -open Cardinal -open FirstOrder Language Structure Theory Order -open Matrix (Vector_eq_VecNotation₂ comp_VecNotation₂) - -namespace FirstOrder.Language.Order - -section - -variable {M : Type w} [instStructure : Language.order.Structure M] - -/-- -The interpretation of the unique binary relation symbol of the language `Language.order` on a type `M` gives a -natural binary relation on `M` and it is written with `≤`. --/ -instance instLE : LE M where - le := fun x y => instStructure.RelMap leSymb ![x, y] - -/-- -Given a type `M` and `𝓜 : Language.order.Structure`, the `Language.order.Structure M` instance induced by the `LE M` -instance which is induced by `𝓜` is equal to `𝓜`. In other words, for a fixed type `M`, `@orderStructure M` is the -left-inverse of `@instLE M`. --/ -@[simp] -lemma orderStructure_of_LE : @orderStructure M (@instLE M instStructure) = instStructure := by - ext1 - · funext _ r - exfalso - exact IsEmpty.elim (by infer_instance) r - · funext n r x - match n with - | 0 | 1 | _ + 3 => - exfalso - simp only [Language.order, mk₂_Relations, Sequence₂] at r - exact IsEmpty.elim (by infer_instance) r - | 2 => - rw [Vector_eq_VecNotation₂ x, (by apply Subsingleton.allEq : r = leSymb)] - simp only [orderStructure, LE.le, Structure.relMap_apply₂] - -/-- -By definition, the binary relation `≤` is equal to the interpretation of the unique binary relation symbol of the -language `Language.order`. --/ -instance : @OrderedStructure Language.order M _ instLE instStructure := by - simp only [OrderedStructure, orderLHom_order, orderStructure_of_LE] - exact @LHom.id_isExpansionOn Language.order M instStructure - -end - -section - -variable {M : Type w} [Language.order.Structure M] -variable {N : Type w} [Language.order.Structure N] - -/-- -An order embedding `φ : M ↪o N`, induces and embedding of structures with the same underlying function. --/ -def toLEmbedding (φ : M ↪o N) : M ↪[Language.order] N where - toEmbedding := φ.toEmbedding - map_fun' := by - intro n f - exfalso - exact IsEmpty.elim (by infer_instance) f - map_rel' := by - intro n r x - match n with - | 0 | 1 | _ + 3 => - exfalso - simp [Language.order, Sequence₂] at r - exact IsEmpty.elim (by infer_instance) r - | 2 => - rw [Vector_eq_VecNotation₂ x, comp_VecNotation₂ φ.toFun, - (by apply Subsingleton.allEq : r = leSymb), relMap_leSymb, relMap_leSymb] - exact φ.map_rel_iff - -/-- -An order isomorphism `φ : M ≃o N`, induces and isomorphism of structures with the same underlying function. --/ -def toLIso (φ : M ≃o N) : M ≃[Language.order] N where - toEquiv := φ.toEquiv - map_fun' := (toLEmbedding (φ.toOrderEmbedding)).map_fun' - map_rel' := (toLEmbedding (φ.toOrderEmbedding)).map_rel' - -end - -namespace DLO --region - -section - -variable (M : Type w) [Language.order.Structure M] -variable [M ⊨ Language.order.dlo] - -/-- -Models of the theory `Language.order.dlo` satisfies the reflexivity sentence. --/ -protected lemma realize_reflexive : M ⊨ (leSymb (L := Language.order)).reflexive := by - apply realize_sentence_of_mem Language.order.dlo - unfold dlo linearOrderTheory - left; left; rfl - -/-- -Models of the theory `Language.order.dlo` satisfies the transitivity sentence. --/ -protected lemma realize_transitive : M ⊨ (leSymb (L := Language.order)).transitive := by - apply realize_sentence_of_mem Language.order.dlo - unfold dlo linearOrderTheory - left; right; right; left; rfl - -/-- -Models of the theory `Language.order.dlo` satisfies the antisymmetric sentence. --/ -protected lemma realize_antisymmetric : M ⊨ (leSymb (L := Language.order)).antisymmetric := by - apply realize_sentence_of_mem Language.order.dlo - unfold dlo linearOrderTheory - left; right; left; rfl - -/-- -Models of the theory `Language.order.dlo` satisfies the totality sentence. --/ -protected lemma realize_total : M ⊨ (leSymb (L := Language.order)).total := by - apply realize_sentence_of_mem Language.order.dlo - unfold dlo linearOrderTheory - left; right; right; right; rfl - -/-- -Models of the theory `Language.order.dlo` satisfies the densely ordered sentence. --/ -protected lemma realize_denselyOrderedSentence : M ⊨ Language.order.denselyOrderedSentence := by - apply realize_sentence_of_mem Language.order.dlo - unfold dlo linearOrderTheory - right; right; right; rfl - -/-- -Models of the theory `Language.order.dlo` satisfies the noBotOrder sentence. --/ -protected lemma realize_noBotOrderSentence : M ⊨ Language.order.noBotOrderSentence := by - apply realize_sentence_of_mem Language.order.dlo - unfold dlo linearOrderTheory - right; right; left; rfl - -/-- -Models of the theory `Language.order.dlo` satisfies the noTopOrder sentence. --/ -protected lemma realize_noTopOrderSentence : M ⊨ Language.order.noTopOrderSentence := by - apply realize_sentence_of_mem Language.order.dlo - unfold dlo linearOrderTheory - right; left; rfl - -end - -section - -variable {M : Type w} [instStructure : Language.order.Structure M] -variable [instModel : M ⊨ Language.order.dlo] - -instance instPreorder : Preorder M where - le := (@instLE M instStructure).le - le_refl := by - have := DLO.realize_reflexive M - simp only [Relations.realize_reflexive] at this - exact this - le_trans := by - have := DLO.realize_transitive M - simp only [Relations.realize_transitive] at this - exact this - -@[simp] -lemma toLE_of_Preorder - : (@instPreorder M instStructure instModel).toLE = @instLE M instStructure := rfl - -noncomputable instance instLinearOrder : LinearOrder M where - toPreorder := @instPreorder M instStructure instModel - le_antisymm := by - have := DLO.realize_antisymmetric M - simp only [Relations.realize_antisymmetric] at this - exact this - le_total := by - have := DLO.realize_total M - simp only [Relations.realize_total] at this - exact this - decidableLE := by apply Classical.decRel - -@[simp] -lemma toLE_of_LinearOrder - : (@instLinearOrder M instStructure instModel).toLE = @instLE M instStructure := rfl - -instance : @NoMinOrder M instLinearOrder.toLT where - exists_lt := by - have := DLO.realize_noBotOrderSentence M - simp only [noBotOrderSentence] at this - intro a - replace this := this a - simp at this - rcases this with ⟨b, h⟩ - use b - exact h - -instance : @NoMaxOrder M instLinearOrder.toLT where - exists_gt := by - have := DLO.realize_noTopOrderSentence M - simp only [noTopOrderSentence] at this - intro a - replace this := this a - simp at this - rcases this with ⟨b, h⟩ - use b - exact h - -instance : DenselyOrdered M where - dense := by - have := DLO.realize_denselyOrderedSentence M - simp only [denselyOrderedSentence] at this - intro a₁ a₂ h - replace this := this a₁ a₂ - simp only [BoundedFormula.realize_imp, Term.realize_lt, Term.realize_var, - BoundedFormula.realize_ex, BoundedFormula.realize_inf] at this - replace this := this h - rcases this with ⟨a, h₁, h₂⟩ - use a - exact ⟨h₁, h₂⟩ - -end - -theorem aleph0_categorical_of_dlo : aleph0.Categorical Language.order.dlo := by - unfold Categorical - rintro ⟨M⟩ ⟨N⟩ hM hN - simp only at * - apply Nonempty.map toLIso - have : Countable M := by apply mk_le_aleph0_iff.mp; rw [hM] - have : Countable N := by apply mk_le_aleph0_iff.mp; rw [hN] - apply iso_of_countable_dense - -end DLO --end - -end FirstOrder.Language.Order diff --git a/FormalTextbookModelTheory/ForMathlib/Matrix.lean b/FormalTextbookModelTheory/ForMathlib/Data/Fin/VecNotation.lean similarity index 100% rename from FormalTextbookModelTheory/ForMathlib/Matrix.lean rename to FormalTextbookModelTheory/ForMathlib/Data/Fin/VecNotation.lean diff --git a/FormalTextbookModelTheory/ForMathlib/ModelTheory/DLO.lean b/FormalTextbookModelTheory/ForMathlib/ModelTheory/DLO.lean new file mode 100644 index 0000000..0a30b71 --- /dev/null +++ b/FormalTextbookModelTheory/ForMathlib/ModelTheory/DLO.lean @@ -0,0 +1,181 @@ +import Mathlib.SetTheory.Cardinal.Basic +import Mathlib.ModelTheory.Basic +import Mathlib.ModelTheory.Syntax +import Mathlib.ModelTheory.Semantics +import Mathlib.ModelTheory.Satisfiability +import Mathlib.ModelTheory.Bundled +import Mathlib.ModelTheory.Order +import Mathlib.Order.CountableDenseLinearOrder + +import FormalTextbookModelTheory.ForMathlib.ModelTheory.Order +import FormalTextbookModelTheory.ForMathlib.Data.Fin.VecNotation + + +open Cardinal +open FirstOrder Language Structure Theory Order +open Matrix (Vector_eq_VecNotation₂ comp_VecNotation₂) + +namespace FirstOrder.Language + +namespace Order + +section + +variable {M : Type w} [instStructure : Language.order.Structure M] + +/-- +The interpretation of the unique binary relation symbol of the language `Language.order` on a type `M` gives a natural binary relation on `M` and it is written with `≤`. +-/ +instance instLE : LE M where + le := fun x y => instStructure.RelMap leSymb ![x, y] + +/-- +Given a type `M` and `𝓜 : Language.order.Structure`, the `Language.order.Structure M` instance induced by the `LE M` +instance which is induced by `𝓜` is equal to `𝓜`. In other words, for a fixed type `M`, `@orderStructure M` is the +left-inverse of `@instLE M`. +-/ +@[simp] +lemma orderStructure_of_LE : @orderStructure M (@instLE M instStructure) = instStructure := by + ext1 + · funext _ r + exfalso + exact IsEmpty.elim (by infer_instance) r + · funext n r x + match n with + | 0 | 1 | _ + 3 => + exfalso + simp only [Language.order, mk₂_Relations, Sequence₂] at r + exact IsEmpty.elim (by infer_instance) r + | 2 => + rw [Vector_eq_VecNotation₂ x, (by apply Subsingleton.allEq : r = leSymb)] + simp only [orderStructure, LE.le, Structure.relMap_apply₂] + +/-- +By definition, the binary relation `≤` is equal to the interpretation of the unique binary relation symbol of the +language `Language.order`. +-/ +instance : @OrderedStructure Language.order M _ instLE instStructure := by + simp only [OrderedStructure, orderLHom_order, orderStructure_of_LE] + exact @LHom.id_isExpansionOn Language.order M instStructure + +end + +section + +variable {M : Type w} [Language.order.Structure M] +variable {N : Type w} [Language.order.Structure N] + +/-- +An order embedding `φ : M ↪o N`, induces and embedding of structures with the same underlying function. +-/ +def toLEmbedding (φ : M ↪o N) : M ↪[Language.order] N where + toEmbedding := φ.toEmbedding + map_fun' := by + intro n f + exfalso + exact IsEmpty.elim (by infer_instance) f + map_rel' := by + intro n r x + match n with + | 0 | 1 | _ + 3 => + exfalso + simp [Language.order, Sequence₂] at r + exact IsEmpty.elim (by infer_instance) r + | 2 => + rw [Vector_eq_VecNotation₂ x, comp_VecNotation₂ φ.toFun, + (by apply Subsingleton.allEq : r = leSymb), relMap_leSymb, relMap_leSymb] + exact φ.map_rel_iff + +/-- +An order isomorphism `φ : M ≃o N`, induces and isomorphism of structures with the same underlying function. +-/ +def toLIso (φ : M ≃o N) : M ≃[Language.order] N where + toEquiv := φ.toEquiv + map_fun' := (toLEmbedding (φ.toOrderEmbedding)).map_fun' + map_rel' := (toLEmbedding (φ.toOrderEmbedding)).map_rel' + +end + +namespace DLO --region + +section + +variable {M : Type w} [instStructure : Language.order.Structure M] +variable [instModel : M ⊨ Language.order.dlo] + +instance instPreorder : Preorder M where + le := (@instLE M instStructure).le + le_refl := by + apply Relations.realize_reflexive.mp + apply realize_sentence_of_mem Language.order.dlo + simp only [reflexive_mem_dlo] + le_trans := by + apply Relations.realize_transitive.mp + apply realize_sentence_of_mem Language.order.dlo + simp only [transitive_mem_dlo] + +instance instPartialOrder : PartialOrder M where + toPreorder := @instPreorder M instStructure instModel + le_antisymm := by + apply Relations.realize_antisymmetric.mp + apply realize_sentence_of_mem Language.order.dlo + simp only [antisymmetric_mem_dlo] + +noncomputable instance instLinearOrder : LinearOrder M where + toPartialOrder := @instPartialOrder M instStructure instModel + le_total := by + apply Relations.realize_total.mp + apply realize_sentence_of_mem Language.order.dlo + simp only [total_mem_dlo] + decidableLE := by apply Classical.decRel + +-- @[simp] +-- lemma toLE_of_Preorder +-- : (@instPreorder M instStructure instModel).toLE = @instLE M instStructure := rfl + +-- @[simp] +-- lemma toLE_of_PartialOrder +-- : (@instPartialOrder M instStructure instModel).toLE = @instLE M instStructure := rfl + +-- @[simp] +-- lemma toLE_of_LinearOrder +-- : (@instLinearOrder M instStructure instModel).toLE = @instLE M instStructure := rfl + +instance : @NoBotOrder M instLinearOrder.toLE where + exists_not_ge := by + apply Relations.realize_noBot.mp + apply realize_sentence_of_mem Language.order.dlo + simp only [noBotOrder_mem_dlo] + +instance : @NoMinOrder M instLinearOrder.toLT := NoBotOrder.to_noMinOrder M + +instance : @NoTopOrder M instLinearOrder.toLE where + exists_not_le := by + apply Relations.realize_noTop.mp + apply realize_sentence_of_mem Language.order.dlo + simp only [noTopOrder_mem_dlo] + +instance : @NoMaxOrder M instLinearOrder.toLT := NoTopOrder.to_noMaxOrder M + +instance : @DenselyOrdered M instLinearOrder.toLT where + dense := by + apply Relations.realize_denselyOrdered.mp + apply realize_sentence_of_mem Language.order.dlo + simp only [denselyOrdered_mem_dlo] + +end + +theorem aleph0_categorical_of_dlo : aleph0.Categorical Language.order.dlo := by + unfold Categorical + rintro ⟨M⟩ ⟨N⟩ hM hN + simp only at * + apply Nonempty.map toLIso + have : Countable M := by apply mk_le_aleph0_iff.mp; rw [hM] + have : Countable N := by apply mk_le_aleph0_iff.mp; rw [hN] + apply iso_of_countable_dense + +end DLO --end + +end Order + +end FirstOrder.Language diff --git a/FormalTextbookModelTheory/ForMathlib/ModelTheory/Order.lean b/FormalTextbookModelTheory/ForMathlib/ModelTheory/Order.lean new file mode 100644 index 0000000..573bfa7 --- /dev/null +++ b/FormalTextbookModelTheory/ForMathlib/ModelTheory/Order.lean @@ -0,0 +1,78 @@ +import Mathlib.ModelTheory.Semantics +import Mathlib.ModelTheory.Order + +namespace FirstOrder.Language + +section + +variable (L : Language) [L.IsOrdered] + +@[simp] +theorem reflexive_mem_dlo : leSymb.reflexive ∈ L.dlo := by + unfold dlo linearOrderTheory + left; left; rfl + +@[simp] +theorem transitive_mem_dlo : leSymb.transitive ∈ L.dlo := by + unfold dlo linearOrderTheory + left; right; right; left; rfl + +@[simp] +theorem antisymmetric_mem_dlo : leSymb.antisymmetric ∈ L.dlo := by + unfold dlo linearOrderTheory + left; right; left; rfl + +@[simp] +theorem total_mem_dlo : leSymb.total ∈ L.dlo := by + unfold dlo linearOrderTheory + left; right; right; right; rfl + +@[simp] +theorem noBotOrder_mem_dlo : L.noBotOrderSentence ∈ L.dlo := by + unfold dlo linearOrderTheory + right; right; left; rfl + +@[simp] +theorem noTopOrder_mem_dlo : L.noTopOrderSentence ∈ L.dlo := by + unfold dlo linearOrderTheory + right; left; rfl + +@[simp] +theorem denselyOrdered_mem_dlo : L.denselyOrderedSentence ∈ L.dlo := by + unfold dlo linearOrderTheory + right; right; right; rfl + +end + +namespace Relations + +open Structure +open BoundedFormula + +variable {L : Language.{u, v}} [instIsOrdered : L.IsOrdered] +variable {M : Type w} [instStructure : L.Structure M] + +local infix:50 " ≼ " => fun x y : M => @RelMap L M instStructure 2 (@leSymb L instIsOrdered) ![x, y] +local infix:50 " ≺ " => fun x y : M => x ≼ y ∧ ¬ y ≼ x + +@[simp] +theorem realize_noBot : M ⊨ L.noBotOrderSentence ↔ ∀ x, ∃ y, ¬ x ≼ y := by + unfold noBotOrderSentence Sentence.Realize Formula.Realize Term.le + simp only [realize_all, realize_ex, realize_not, realize_rel₂] + rfl + +@[simp] +theorem realize_noTop : M ⊨ L.noTopOrderSentence ↔ ∀ x, ∃ y, ¬ y ≼ x := by + unfold noTopOrderSentence Sentence.Realize Formula.Realize Term.le + simp only [realize_all, realize_ex, realize_not, realize_rel₂] + rfl + +@[simp] +theorem realize_denselyOrdered : M ⊨ L.denselyOrderedSentence ↔ ∀ x y, x ≺ y → ∃ z, x ≺ z ∧ z ≺ y := by + unfold denselyOrderedSentence Sentence.Realize Formula.Realize Term.lt Term.le + simp only [realize_all, realize_imp, realize_inf, realize_rel₂, realize_not, realize_ex] + rfl + +end Relations + +end FirstOrder.Language diff --git a/blueprint/lean_decls b/blueprint/lean_decls index baedaa7..8dacee6 100644 --- a/blueprint/lean_decls +++ b/blueprint/lean_decls @@ -1,16 +1,26 @@ Matrix.Vector_eq_VecNotation₂ Matrix.comp_VecNotation₂ -FirstOrder.Language.Order.DLO.realize_reflexive -FirstOrder.Language.Order.DLO.realize_transitive -FirstOrder.Language.Order.DLO.realize_antisymmetric -FirstOrder.Language.Order.DLO.realize_total -FirstOrder.Language.Order.DLO.realize_denselyOrderedSentence -FirstOrder.Language.Order.DLO.realize_noBotOrderSentence -FirstOrder.Language.Order.DLO.realize_noTopOrderSentence +FirstOrder.Language.reflexive_mem_dlo +FirstOrder.Language.transitive_mem_dlo +FirstOrder.Language.antisymmetric_mem_dlo +FirstOrder.Language.total_mem_dlo +FirstOrder.Language.noBotOrder_mem_dlo +FirstOrder.Language.noTopOrder_mem_dlo +FirstOrder.Language.denselyOrdered_mem_dlo +FirstOrder.Language.Relations.realize_noBot +FirstOrder.Language.Relations.realize_noTop +FirstOrder.Language.Relations.realize_denselyOrdered FirstOrder.Language.Order.instLE FirstOrder.Language.Order.orderStructure_of_LE +FirstOrder.Language.Order.instOrderedStructureOrder_formalTextbookModelTheory FirstOrder.Language.Order.DLO.instPreorder +FirstOrder.Language.Order.DLO.instPartialOrder FirstOrder.Language.Order.DLO.instLinearOrder +FirstOrder.Language.Order.DLO.instNoBotOrder_formalTextbookModelTheory +FirstOrder.Language.Order.DLO.instNoMinOrder_formalTextbookModelTheory +FirstOrder.Language.Order.DLO.instNoTopOrder_formalTextbookModelTheory +FirstOrder.Language.Order.DLO.instNoMaxOrder_formalTextbookModelTheory +FirstOrder.Language.Order.DLO.instDenselyOrdered_formalTextbookModelTheory FirstOrder.Language.Order.toLEmbedding FirstOrder.Language.Order.toLIso FirstOrder.Language.Order.DLO.aleph0_categorical_of_dlo \ No newline at end of file diff --git a/blueprint/print/print.aux b/blueprint/print/print.aux index 4aa5171..3a20813 100644 --- a/blueprint/print/print.aux +++ b/blueprint/print/print.aux @@ -10,26 +10,36 @@ \newlabel{lem:vector-notation}{{1.1.1}{1}{}{theorem.1.1.1}{}} \newlabel{lem:vector-notation-under-composition}{{1.1.2}{1}{}{theorem.1.1.2}{}} \@writefile{toc}{\contentsline {section}{\numberline {1.2}Theories}{1}{section.1.2}\protected@file@percent } -\newlabel{lem:realize-reflexivity}{{1.2.1}{1}{}{theorem.1.2.1}{}} -\newlabel{lem:realize-transitivity}{{1.2.2}{1}{}{theorem.1.2.2}{}} -\newlabel{lem:realize-antisymmetric}{{1.2.3}{1}{}{theorem.1.2.3}{}} -\newlabel{lem:realize-total}{{1.2.4}{1}{}{theorem.1.2.4}{}} -\newlabel{lem:realize-densely-ordered}{{1.2.5}{1}{}{theorem.1.2.5}{}} -\newlabel{lem:realize-no-min}{{1.2.6}{1}{}{theorem.1.2.6}{}} -\newlabel{lem:realize-no-max}{{1.2.7}{1}{}{theorem.1.2.7}{}} -\@writefile{toc}{\contentsline {chapter}{\numberline {2}Model Theory and The Rest of Mathlib}{2}{chapter.2}\protected@file@percent } +\newlabel{lem:reflexive_mem_dlo}{{1.2.1}{1}{}{theorem.1.2.1}{}} +\newlabel{lem:transitive_mem_dlo}{{1.2.2}{1}{}{theorem.1.2.2}{}} +\newlabel{lem:antisymmetric_mem_dlo}{{1.2.3}{1}{}{theorem.1.2.3}{}} +\newlabel{lem:total_mem_dlo}{{1.2.4}{1}{}{theorem.1.2.4}{}} +\newlabel{lem:noBotOrder_mem_dlo}{{1.2.5}{1}{}{theorem.1.2.5}{}} +\newlabel{lem:noTopOrder_mem_dlo}{{1.2.6}{1}{}{theorem.1.2.6}{}} +\newlabel{lem:denselyOrdered_mem_dlo}{{1.2.7}{2}{}{theorem.1.2.7}{}} +\newlabel{lem:realize_noBot}{{1.2.8}{2}{}{theorem.1.2.8}{}} +\newlabel{lem:realize_noTop}{{1.2.9}{2}{}{theorem.1.2.9}{}} +\newlabel{lem:realize_denselyOrdered}{{1.2.10}{2}{}{theorem.1.2.10}{}} +\@writefile{toc}{\contentsline {chapter}{\numberline {2}Model Theory and The Rest of Mathlib}{3}{chapter.2}\protected@file@percent } \@writefile{lof}{\addvspace {10\p@ }} \@writefile{lot}{\addvspace {10\p@ }} -\@writefile{toc}{\contentsline {section}{\numberline {2.1}Instances}{2}{section.2.1}\protected@file@percent } -\newlabel{def:le-instance-language-order}{{2.1.1}{2}{}{theorem.2.1.1}{}} -\newlabel{lem:order-structure-of-le}{{2.1.2}{2}{}{theorem.2.1.2}{}} -\newlabel{def:preorder-dlo}{{2.1.3}{2}{}{theorem.2.1.3}{}} -\newlabel{def:linearorder-dlo}{{2.1.4}{2}{}{theorem.2.1.4}{}} -\@writefile{toc}{\contentsline {section}{\numberline {2.2}Homomorphisms}{2}{section.2.2}\protected@file@percent } -\newlabel{lem:to-embedding}{{2.2.1}{2}{}{theorem.2.2.1}{}} -\newlabel{lem:to-isomorphism}{{2.2.2}{2}{}{theorem.2.2.2}{}} -\@writefile{toc}{\contentsline {chapter}{\numberline {3}Main Result}{3}{chapter.3}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {2.1}Instances}{3}{section.2.1}\protected@file@percent } +\newlabel{def:le-instance-language-order}{{2.1.1}{3}{}{theorem.2.1.1}{}} +\newlabel{lem:order-structure-of-le}{{2.1.2}{3}{}{theorem.2.1.2}{}} +\newlabel{lem:instOrderedStructureOrder_formalTextbookModelTheory}{{2.1.3}{3}{}{theorem.2.1.3}{}} +\newlabel{lem:preorder-dlo}{{2.1.4}{3}{}{theorem.2.1.4}{}} +\newlabel{lem:partial-order-dlo}{{2.1.5}{3}{}{theorem.2.1.5}{}} +\newlabel{lem:linearorder-dlo}{{2.1.6}{3}{}{theorem.2.1.6}{}} +\newlabel{lem:no-bot-order-dlo}{{2.1.7}{3}{}{theorem.2.1.7}{}} +\newlabel{lem:no-min-order-dlo}{{2.1.8}{3}{}{theorem.2.1.8}{}} +\newlabel{lem:no-top-order-dlo}{{2.1.9}{4}{}{theorem.2.1.9}{}} +\newlabel{lem:no-max-order-dlo}{{2.1.10}{4}{}{theorem.2.1.10}{}} +\newlabel{lem:densely-ordered-dlo}{{2.1.11}{4}{}{theorem.2.1.11}{}} +\@writefile{toc}{\contentsline {section}{\numberline {2.2}Homomorphisms}{4}{section.2.2}\protected@file@percent } +\newlabel{lem:to-embedding}{{2.2.1}{4}{}{theorem.2.2.1}{}} +\newlabel{lem:to-isomorphism}{{2.2.2}{4}{}{theorem.2.2.2}{}} +\@writefile{toc}{\contentsline {chapter}{\numberline {3}Main Result}{5}{chapter.3}\protected@file@percent } \@writefile{lof}{\addvspace {10\p@ }} \@writefile{lot}{\addvspace {10\p@ }} -\newlabel{thm:dlo-aleph0-categorical}{{3.0.1}{3}{}{theorem.3.0.1}{}} -\gdef \@abspage@last{4} +\newlabel{thm:dlo-aleph0-categorical}{{3.0.1}{5}{}{theorem.3.0.1}{}} +\gdef \@abspage@last{6} diff --git a/blueprint/print/print.fdb_latexmk b/blueprint/print/print.fdb_latexmk index 372ed95..73dbd98 100644 --- a/blueprint/print/print.fdb_latexmk +++ b/blueprint/print/print.fdb_latexmk @@ -1,7 +1,7 @@ # Fdb version 4 -["pdflatex"] 1723661794.7511 "print.tex" "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.pdf" "print" 1723661795.69292 0 - "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.aux" 1723661795.4694 2232 b6b67c3fcb3329da2c254c2d8baad30a "pdflatex" - "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.out" 1723661795.4694 935 0e20a0f58d1d7838ffc59f27f356d900 "pdflatex" +["pdflatex"] 1723815716.39049 "print.tex" "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.pdf" "print" 1723815717.48559 0 + "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.aux" 1723815717.22314 2910 6bf91ad4171cfa1daafd8f054c4268cd "pdflatex" + "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.out" 1723815717.22314 935 0e20a0f58d1d7838ffc59f27f356d900 "pdflatex" "/usr/local/texlive/2024/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 "" "/usr/local/texlive/2024/texmf-dist/fonts/tfm/adobe/zapfding/pzdr.tfm" 1136768653 1528 f853c4d1b4e0550255e02831fdc8496f "" "/usr/local/texlive/2024/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm" 1246382020 916 f87d7c45f9c908e672703b83b72241a3 "" @@ -83,13 +83,13 @@ "/usr/local/texlive/2024/texmf-dist/web2c/texmf.cnf" 1719785820 42007 0b741a3c21a5ca32b40e3846e75b3548 "" "/usr/local/texlive/2024/texmf-var/web2c/xetex/xelatex.fmt" 1722380463 10868501 e521c25442cce99c56ff9a77d153050d "" "/usr/local/texlive/2024/texmf.cnf" 1722380410.43027 455 5b996dcaa0eb4ef14a83b026bc0a008c "" - "chapters/basics.tex" 1723659066.66334 2441 b48c6cf0620ad41684aeac4b58dc95e7 "" - "chapters/main.tex" 1723661787.37893 321 18d95ad5a64d5d1a73dc8caacf660dd9 "" - "chapters/model_theory.tex" 1723659684.69707 2076 ed78731b4190e4a400ab523aaea36373 "" + "chapters/basics.tex" 1723812304.01876 3240 439ee73da8dd9acc44433db5dfacbb11 "" + "chapters/main.tex" 1723815095.35872 389 07f785e08b4826fa5ebcb2e51bb44484 "" + "chapters/model_theory.tex" 1723815297.81403 5093 b77939e0766bbf0b48b06fe4aab07ca9 "" "content.tex" 1723660673.45768 1004 792b81f5308bf1a333bd495ff2e0fd5a "" "macros/common.tex" 1722759673.52174 604 ca3e9443483cfefd693019fb112f2d18 "" "macros/print.tex" 1722422546.45932 1101 87627b2ec24fef68edc71c13f43f7bab "" - "print.tex" 1722837065.5925 1131 bf5d368546e76888c21bf562766212eb "" + "print.tex" 1723815697.02348 1138 2b86096090134771126de5cfa2eeef68 "" (generated) "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.aux" "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.log" diff --git a/blueprint/print/print.log b/blueprint/print/print.log index 197a8f2..a85d99b 100644 --- a/blueprint/print/print.log +++ b/blueprint/print/print.log @@ -1,4 +1,4 @@ -This is XeTeX, Version 3.141592653-2.6-0.999996 (TeX Live 2024) (preloaded format=xelatex 2024.7.31) 14 AUG 2024 21:56 +This is XeTeX, Version 3.141592653-2.6-0.999996 (TeX Live 2024) (preloaded format=xelatex 2024.7.31) 16 AUG 2024 16:41 entering extended mode restricted \write18 enabled. %&-line parsing enabled. @@ -683,21 +683,25 @@ LaTeX Font Info: Font shape `TU/latinmodern-math.otf(3)/m/n' will be (Font) scaled to size 6.99925pt on input line 9. LaTeX Font Info: Font shape `TU/latinmodern-math.otf(3)/m/n' will be (Font) scaled to size 4.99947pt on input line 9. -) + [1 -] +]) + +[2] Chapter 2. -(./chapters/model_theory.tex) +(./chapters/model_theory.tex -[2 +[3 -] +]) + +[4] Chapter 3. (./chapters/main.tex)) -[3 +[5 ] (/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.aux) @@ -709,13 +713,13 @@ Package rerunfilecheck Info: File `print.out' has not changed. (rerunfilecheck) Checksum: 0E20A0F58D1D7838FFC59F27F356D900;935. ) Here is how much of TeX's memory you used: - 16792 strings out of 474240 - 309351 string characters out of 5742353 - 1929557 words of memory out of 5000000 - 39267 multiletter control sequences out of 15000+600000 + 16802 strings out of 474240 + 309613 string characters out of 5742353 + 1928557 words of memory out of 5000000 + 39277 multiletter control sequences out of 15000+600000 563440 words of font info for 85 fonts, out of 8000000 for 9000 1348 hyphenation exceptions out of 8191 - 90i,6n,116p,542b,463s stack positions out of 10000i,1000n,20000p,200000b,200000s + 90i,6n,116p,542b,481s stack positions out of 10000i,1000n,20000p,200000b,200000s Output written on /home/metinersin/projects/FormalTextbookModelTheory/blueprint -/print/print.pdf (4 pages). +/print/print.pdf (6 pages). diff --git a/blueprint/print/print.pdf b/blueprint/print/print.pdf index df19e09..27000bb 100644 Binary files a/blueprint/print/print.pdf and b/blueprint/print/print.pdf differ diff --git a/blueprint/print/print.synctex.gz b/blueprint/print/print.synctex.gz index 1371aed..6626378 100644 Binary files a/blueprint/print/print.synctex.gz and b/blueprint/print/print.synctex.gz differ diff --git a/blueprint/src/chapters/basics.tex b/blueprint/src/chapters/basics.tex index a075b18..22cd256 100644 --- a/blueprint/src/chapters/basics.tex +++ b/blueprint/src/chapters/basics.tex @@ -28,70 +28,100 @@ \section{Theories} %%% Really trivial stuff about theories \begin{lemma} - \label{lem:realize-reflexivity} - \lean{FirstOrder.Language.Order.DLO.realize_reflexive} + \label{lem:reflexive_mem_dlo} + \lean{FirstOrder.Language.reflexive_mem_dlo} \leanok - Models of the theory of dense linear orders realize the reflexivity sentence. + The theory of dense linear orders contains the reflexive sentence. \end{lemma} \begin{proof} \leanok \end{proof} \begin{lemma} - \label{lem:realize-transitivity} - \lean{FirstOrder.Language.Order.DLO.realize_transitive} + \label{lem:transitive_mem_dlo} + \lean{FirstOrder.Language.transitive_mem_dlo} \leanok - Models of the theory of dense linear orders realize the transitivity sentence. + The theory of dense linear orders without end points contains the transitive sentence. \end{lemma} \begin{proof} \leanok \end{proof} \begin{lemma} - \label{lem:realize-antisymmetric} - \lean{FirstOrder.Language.Order.DLO.realize_antisymmetric} + \label{lem:antisymmetric_mem_dlo} + \lean{FirstOrder.Language.antisymmetric_mem_dlo} \leanok - Models of the theory of dense linear orders realize the antisymmetry sentence. + The theory of dense linear orders without end points contains the antisymmetric sentence. \end{lemma} \begin{proof} \leanok \end{proof} \begin{lemma} - \label{lem:realize-total} - \lean{FirstOrder.Language.Order.DLO.realize_total} + \label{lem:total_mem_dlo} + \lean{FirstOrder.Language.total_mem_dlo} \leanok - Models of the theory of dense linear orders realize the totality sentence. + The theory of dense linear orders without end points contains the total sentence. \end{lemma} \begin{proof} \leanok \end{proof} \begin{lemma} - \label{lem:realize-densely-ordered} - \lean{FirstOrder.Language.Order.DLO.realize_denselyOrderedSentence} + \label{lem:noBotOrder_mem_dlo} + \lean{FirstOrder.Language.noBotOrder_mem_dlo} \leanok - Models of the theory of dense linear orders realize the densely ordered sentence. + The theory of dense linear orders without end points contains the no bottom element sentence. \end{lemma} \begin{proof} \leanok \end{proof} \begin{lemma} - \label{lem:realize-no-min} - \lean{FirstOrder.Language.Order.DLO.realize_noBotOrderSentence} + \label{lem:noTopOrder_mem_dlo} + \lean{FirstOrder.Language.noTopOrder_mem_dlo} \leanok - Models of the theory of dense linear orders realize no minimum sentence. + The theory of dense linear orders without end points contains the no top element sentence. \end{lemma} \begin{proof} \leanok \end{proof} \begin{lemma} - \label{lem:realize-no-max} - \lean{FirstOrder.Language.Order.DLO.realize_noTopOrderSentence} + \label{lem:denselyOrdered_mem_dlo} + \lean{FirstOrder.Language.denselyOrdered_mem_dlo} \leanok - Models of the theory of dense linear orders realize no maximum sentence. + The theory of dense linear orders without end points contains the densely ordered sentence. +\end{lemma} +\begin{proof} + \leanok +\end{proof} + +\begin{lemma} + \label{lem:realize_noBot} + \lean{FirstOrder.Language.Relations.realize_noBot} + \leanok + Models of the theory of dense linear orders without end points satisfies the no bottom element sentence. +\end{lemma} +\begin{proof} + \leanok +\end{proof} + +\begin{lemma} + \label{lem:realize_noTop} + \lean{FirstOrder.Language.Relations.realize_noTop} + \leanok + Models of the theory of dense linear orders without end points satisfies the no top element sentence. +\end{lemma} +\begin{proof} + \leanok +\end{proof} + +\begin{lemma} + \label{lem:realize_denselyOrdered} + \lean{FirstOrder.Language.Relations.realize_denselyOrdered} + \leanok + Models of the theory of dense linear orders without end points satisfies the densely ordered sentence. \end{lemma} \begin{proof} \leanok diff --git a/blueprint/src/chapters/main.tex b/blueprint/src/chapters/main.tex index a7ff0ae..1f07f6a 100644 --- a/blueprint/src/chapters/main.tex +++ b/blueprint/src/chapters/main.tex @@ -1,4 +1,3 @@ - \begin{theorem} \label{thm:dlo-aleph0-categorical} \lean{FirstOrder.Language.Order.DLO.aleph0_categorical_of_dlo} @@ -7,5 +6,5 @@ \end{theorem} \begin{proof} \leanok - \uses{def:linearorder-dlo, lem:to-isomorphism} + \uses{lem:linearorder-dlo, lem:no-min-order-dlo, lem:no-max-order-dlo, lem:densely-ordered-dlo, lem:to-isomorphism} \end{proof} diff --git a/blueprint/src/chapters/model_theory.tex b/blueprint/src/chapters/model_theory.tex index 89fd629..bcda268 100644 --- a/blueprint/src/chapters/model_theory.tex +++ b/blueprint/src/chapters/model_theory.tex @@ -1,4 +1,7 @@ \section{Instances} + +Mathlib already contains a proof for the categoricity of the theory of dense linear orders without end points but it is written in terms of various instances such as `DenselyOrdered`. In this section, we produce these instances for a `FirstOrder.Language.Order` structure. + %%% Simple instances \begin{definition} @@ -20,26 +23,120 @@ \section{Instances} \uses{def:le-instance-language-order, lem:vector-notation} \end{proof} -\begin{definition} - \label{def:preorder-dlo} +\begin{lemma} + \label{lem:instOrderedStructureOrder_formalTextbookModelTheory} + \lean{FirstOrder.Language.Order.instOrderedStructureOrder_formalTextbookModelTheory} + \leanok + \uses{def:le-instance-language-order} + By definition, the binary relation $\le$ is equal to the interpretation of the unique binary relation symbol of the language `Language.order`. +\end{lemma} +\begin{proof} + \leanok + \uses{lem:order-structure-of-le} +\end{proof} + +\begin{lemma} + \label{lem:preorder-dlo} \lean{FirstOrder.Language.Order.DLO.instPreorder} \leanok - \uses{def:le-instance-language-order, lem:realize-reflexivity, lem:realize-transitivity} - Models of the theory of dense linear orders are preorders. -\end{definition} + \uses{def:le-instance-language-order} + Models of the theory of dense linear orders without end points are preorders. +\end{lemma} +\begin{proof} + \leanok + \uses{lem:reflexive_mem_dlo, lem:transitive_mem_dlo} +\end{proof} -\begin{definition} - \label{def:linearorder-dlo} +\begin{lemma} + \label{lem:partial-order-dlo} + \lean{FirstOrder.Language.Order.DLO.instPartialOrder} + \leanok + \uses{lem:preorder-dlo} + Models of the theory of dense linear orders without end points are partial orders. +\end{lemma} +\begin{proof} + \leanok + \uses{lem:antisymmetric_mem_dlo} +\end{proof} + +\begin{lemma} + \label{lem:linearorder-dlo} \lean{FirstOrder.Language.Order.DLO.instLinearOrder} \leanok - \uses{def:le-instance-language-order, def:preorder-dlo, lem:realize-antisymmetric, lem:realize-total} - Models of the theory of dense linear orders are linear orders. -\end{definition} + \uses{lem:partial-order-dlo} + Models of the theory of dense linear orders without end points are linear orders. +\end{lemma} +\begin{proof} + \leanok + \uses{lem:total_mem_dlo} +\end{proof} + +\begin{lemma} + \label{lem:no-bot-order-dlo} + \lean{FirstOrder.Language.Order.DLO.instNoBotOrder_formalTextbookModelTheory} + \leanok + \uses{lem:linearorder-dlo} + Models of the theory of dense linear orders without end points do not have a bottom element. +\end{lemma} +\begin{proof} + \leanok + \uses{lem:noBotOrder_mem_dlo, lem:realize_noBot} +\end{proof} + +\begin{lemma} + \label{lem:no-min-order-dlo} + \lean{FirstOrder.Language.Order.DLO.instNoMinOrder_formalTextbookModelTheory} + \leanok + \uses{lem:linearorder-dlo} + Models of the theory of dense linear orders without end points do not have a minimum element. +\end{lemma} +\begin{proof} + \leanok + \uses{lem:no-bot-order-dlo} +\end{proof} + +\begin{lemma} + \label{lem:no-top-order-dlo} + \lean{FirstOrder.Language.Order.DLO.instNoTopOrder_formalTextbookModelTheory} + \leanok + \uses{lem:linearorder-dlo} + Models of the theory of dense linear orders without end points do not have a top element. +\end{lemma} +\begin{proof} + \leanok + \uses{lem:noTopOrder_mem_dlo, lem:realize_noTop} +\end{proof} + +\begin{lemma} + \label{lem:no-max-order-dlo} + \lean{FirstOrder.Language.Order.DLO.instNoMaxOrder_formalTextbookModelTheory} + \leanok + \uses{lem:linearorder-dlo} + Models of the theory of dense linear orders without end points do not have a maximum element. +\end{lemma} +\begin{proof} + \leanok + \uses{lem:no-top-order-dlo} +\end{proof} + +\begin{lemma} + \label{lem:densely-ordered-dlo} + \lean{FirstOrder.Language.Order.DLO.instDenselyOrdered_formalTextbookModelTheory} + \leanok + \uses{lem:linearorder-dlo} + Models of the theory of dense linear orders without end points are densely ordered. +\end{lemma} +\begin{proof} + \leanok + \uses{lem:denselyOrdered_mem_dlo, lem:realize_denselyOrdered} +\end{proof} %%% \section{Homomorphisms} +We also need to show that maps respecting the order structure are homomorphisms in the model theoretic sense. + \begin{lemma} \label{lem:to-embedding} \lean{FirstOrder.Language.Order.toLEmbedding} @@ -49,7 +146,7 @@ \section{Homomorphisms} \end{lemma} \begin{proof} \leanok - \uses{def:le-instance-language-order, lem:vector-notation, lem:vector-notation-under-composition} + \uses{def:le-instance-language-order, lem:instOrderedStructureOrder_formalTextbookModelTheory, lem:vector-notation, lem:vector-notation-under-composition} \end{proof} \begin{lemma} @@ -61,7 +158,7 @@ \section{Homomorphisms} \end{lemma} \begin{proof} \leanok - \uses{def:le-instance-language-order, lem:vector-notation, lem:vector-notation-under-composition, lem:to-embedding} + \uses{lem:to-embedding} \end{proof} diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex index c09089b..f0edf4f 100644 --- a/blueprint/src/print.tex +++ b/blueprint/src/print.tex @@ -24,7 +24,7 @@ \input{macros/common} \input{macros/print} -\title{My formalization project} +\title{Formal Textbook of Model Theory} \author{Metin Ersin Arıcan} \begin{document} diff --git a/blueprint/src/web.paux b/blueprint/src/web.paux index 76313b9..f7be49c 100644 Binary files a/blueprint/src/web.paux and b/blueprint/src/web.paux differ diff --git a/blueprint/web/dep_graph_document.html b/blueprint/web/dep_graph_document.html index 2158c80..57d456e 100644 --- a/blueprint/web/dep_graph_document.html +++ b/blueprint/web/dep_graph_document.html @@ -91,22 +91,142 @@

Dependencies

-
+
- +
+ + + +
+
+ + + + +
+
+ + + +
+
+ + + + +
+
+ + + +
+
+ + + + +
+
+ + + +
+
+ + +