diff --git a/FormalTextbookModelTheory.lean b/FormalTextbookModelTheory.lean index d81e0ad..2b6111a 100644 --- a/FormalTextbookModelTheory.lean +++ b/FormalTextbookModelTheory.lean @@ -1,4 +1,114 @@ --- This module serves as the root of the `FormalTextbookModelTheory` library. --- Import modules here that should be built as part of the library. -import FormalTextbookModelTheory.ForMathlib.DLO -import FormalTextbookModelTheory.Basic +import FormalTextbookModelTheory.ForMathlib2.Matrix +import FormalTextbookModelTheory.ForMathlib2.Cardinal +import FormalTextbookModelTheory.ForMathlib2.DLO + +---region automatically create leanblueprint + +import Lean.Elab.Print +import Mathlib.Lean.Expr.Basic +import Batteries.Tactic.PrintDependents + +set_option linter.hashCommand false + +open Lean Elab Command + +abbrev excludedRootNames : NameSet := NameSet.empty + |>.insert `Init + |>.insert `Lean + |>.insert `Qq + |>.insert `ImportGraph + |>.insert `ProofWidgets + |>.insert `Std + |>.insert `Aesop + |>.insert `Batteries + |>.insert `Mathlib + +def userDefinedModules : CommandElabM (Array Name) := do + let env ← getEnv + let allowedImports := env.allImportedModuleNames.filter (!excludedRootNames.contains ·.getRoot) + return allowedImports.qsort Name.lt + +def test_userDefinedModules : CommandElabM Unit := do + let modules ← userDefinedModules + logInfo modules.toList.toString + +def moduleNameToFileName (moduleName : Name) : System.FilePath := + System.FilePath.addExtension (System.mkFilePath $ moduleName.toString.splitOn ".") "lean" + +def test_moduleNameToFileName : CommandElabM Unit := do + let modules ← userDefinedModules + let mut fnames := #[] + for module in modules do + fnames := fnames.push (moduleNameToFileName module) + logInfo fnames.toList.toString + +def userDefinedDecls : CommandElabM (Array Name) := do + let env ← getEnv + -- + let mut modIdx : HashSet Nat := .empty + let mut modsSeen : NameSet := .empty + let allowedImports ← userDefinedModules + for imp in allowedImports do + if let some nm := env.getModuleIdx? imp then + modIdx := modIdx.insert nm + modsSeen := modsSeen.insert imp + -- + let consts := env.constants + let newDeclNames := consts.fold (init := ({} : NameSet)) fun a b _c => + match env.getModuleIdxFor? b with + | none => a + | some idx => if modIdx.contains idx then a.insert b else a + -- + let mut newDeclNamesFiltered := #[] + for decl in newDeclNames do + if decl.isAnonymous then + continue + if decl.isNum then + continue + if decl.isAuxLemma then + continue + if decl.isInternal then + continue + if decl.isInternalDetail then + continue + if decl.isImplementationDetail then + continue + if decl.isInaccessibleUserName then + continue + newDeclNamesFiltered := newDeclNamesFiltered.push decl + return newDeclNamesFiltered.qsort Name.lt + +def test_userDefinedDecls : CommandElabM Unit := do + let decls ← userDefinedDecls + logInfo decls.size.repr + logInfo decls.toList.toString + +def getDocstring (decl : Name) : CoreM (Option String) := do + return ← findDocString? (← getEnv) decl + +def test_getDocstring : CoreM Unit := do + let doc ← getDocstring `FirstOrder.Language.Order.DLO.aleph0_categorical_of_dlo + IO.println doc + + +/-- extracts the names of the declarations in `env` on which `decl` depends. -/ +-- source: +-- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Counting.20prerequisites.20of.20a.20theorem/near/425370265 +def getVisited (env : Environment) (decl : Name) := + let (_, { visited, .. }) := Elab.Command.CollectAxioms.collect decl |>.run env |>.run {} + visited + +def getDependencies (decl : Name) : CommandElabM (Array Name) := do + let env ← getEnv + let visited := (getVisited env decl).toArray + let decls ← userDefinedDecls + let visited := visited.filter $ fun name => name ∈ decls ∧ name ≠ decl + return visited + +#eval test_userDefinedModules +#eval test_moduleNameToFileName +#eval test_userDefinedDecls +#eval test_getDocstring +#eval (getDependencies `FirstOrder.Language.Order.orderStructure_of_LE) + +--end diff --git a/FormalTextbookModelTheory/ForMathlib/DLO.lean b/FormalTextbookModelTheory/ForMathlib/DLO.lean index 1f26fd2..83e7352 100644 --- a/FormalTextbookModelTheory/ForMathlib/DLO.lean +++ b/FormalTextbookModelTheory/ForMathlib/DLO.lean @@ -3,19 +3,34 @@ 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.Order open Cardinal open FirstOrder +open Language +open Order -universe u v w +namespace FirstOrder.Language.Order -notation "L≤" => Language.order +-- def to_Lle_homomorphism {M N : Type w} [L≤.Structure M] [L≤.Structure N] (f : M →o N) : M →[L≤] N := +-- by sorry theorem aleph0_categorical_of_dlo : aleph0.Categorical L≤.dlo := by + unfold Categorical + rintro ⟨M⟩ ⟨N⟩ hM hN + simp only at * + constructor + + have instLinearOrderM : LinearOrder M := by exact inst_LinearOrder_of_dlo L≤ + have instLinearOrderN : LinearOrder N := by exact inst_LinearOrder_of_dlo L≤ + have instDensolyOrderedM : @DenselyOrdered M (inst_Preorder_of_dlo L≤).toLT := by + exact inst_DenselyOrdered_of_dlo L≤ + sorry -#check aleph0_categorical_of_dlo +#check iso_of_countable_dense --- Here, we will put definitions and theorems about the theory --- of dense linear orders without endpoints. +end FirstOrder.Language.Order diff --git a/FormalTextbookModelTheory/ForMathlib/Language.lean b/FormalTextbookModelTheory/ForMathlib/Language.lean new file mode 100644 index 0000000..5efd461 --- /dev/null +++ b/FormalTextbookModelTheory/ForMathlib/Language.lean @@ -0,0 +1,87 @@ +import Mathlib.SetTheory.Cardinal.Basic +import Mathlib.ModelTheory.Basic +import Mathlib.ModelTheory.Satisfiability +import Mathlib.ModelTheory.Order + +universe u v w + +open Cardinal +open FirstOrder Language Structure + +namespace FirstOrder.Language + +class IsRelational₂ (L : Language.{u, v}) extends IsRelational L : Prop where + only_rel₂ : ∀ {n}, n ≠ 2 → IsEmpty (L.Relations n) + +namespace Structure --region Structure + +variable {L : Language.{u, v}} {M : Type w} + +section Relational + +lemma funMap_eq_funMap_of_relational [IsRelational L] (𝓜₁ 𝓜₂ : L.Structure M) + : @funMap L M 𝓜₁ = @funMap L M 𝓜₂ := by + rw [Subsingleton.elim (@funMap L M 𝓜₁) (@funMap L M 𝓜₂)] + +lemma funMap_eq_funMap_of_relational' [IsRelational L] (𝓜₁ 𝓜₂ : L.Structure M) + {n} (nFun : L.Functions n) (x : Fin n → M) + : 𝓜₁.funMap nFun x = 𝓜₂.funMap nFun x := by + rw [Subsingleton.elim (𝓜₁.funMap) (𝓜₂.funMap)] + +@[ext] +lemma structure_eq_structure_of_relational [IsRelational L] + {𝓜₁ 𝓜₂ : L.Structure M} (h : @RelMap L M 𝓜₁ = @RelMap L M 𝓜₂) : 𝓜₁ = 𝓜₂ := by + ext1 + · apply funMap_eq_funMap_of_relational + · apply h + +lemma structure_eq_of_structure_of_relational_iff [IsRelational L] + {𝓜₁ 𝓜₂: L.Structure M} : 𝓜₁ = 𝓜₂ ↔ @RelMap L M 𝓜₁ = @RelMap L M 𝓜₂ := by + constructor <;> intro h + · simp only [h, implies_true] + · ext1; exact h + +lemma structure_eq_of_structure_of_relational_iff' [IsRelational L] + {𝓜₁ 𝓜₂: L.Structure M} : 𝓜₁ = 𝓜₂ ↔ ∀ {n} r x, @RelMap L M 𝓜₁ n r x = @RelMap L M 𝓜₂ n r x := by + constructor <;> intro h + · simp only [h, implies_true] + · ext1; funext n r x; exact h r x + +end Relational + +section Relational₂ + +lemma RelMap_eq_RelMap_of_relational₂ [IsRelational₂ L] (𝓜₁ 𝓜₂ : L.Structure M) + {n} (hn : n ≠ 2) : @RelMap L M 𝓜₁ n = @RelMap L M 𝓜₂ n := by + have : IsEmpty (L.Relations n) := by exact IsRelational₂.only_rel₂ hn + rw [Subsingleton.elim (@RelMap L M 𝓜₁ n) (@RelMap L M 𝓜₂ n)] + +lemma RelMap_eq_RelMap_of_relational₂' [IsRelational₂ L] (𝓜₁ 𝓜₂ : L.Structure M) + {n} (hn : n ≠ 2) (nRel : L.Relations n) (x : Fin n → M) : + 𝓜₁.RelMap nRel x ↔ 𝓜₂.RelMap nRel x := by + have : IsEmpty (L.Relations n) := by exact IsRelational₂.only_rel₂ hn + rw [Subsingleton.elim (𝓜₁.RelMap) (𝓜₂.RelMap)] + +@[ext] +lemma structure_eq_structure_of_relational₂ [IsRelational₂ L] + {𝓜₁ 𝓜₂ : L.Structure M} + (h : @RelMap L M 𝓜₁ 2 = @RelMap L M 𝓜₂ 2) : 𝓜₁ = 𝓜₂ := by + ext1 + funext n + by_cases h' : n = 2 + · subst h' + exact h + · apply RelMap_eq_RelMap_of_relational₂ + exact h' + +lemma structure_eq_of_structure_of_relational₂_iff [IsRelational₂ L] + {𝓜₁ 𝓜₂ : L.Structure M} : 𝓜₁ = 𝓜₂ ↔ @RelMap L M 𝓜₁ 2 = @RelMap L M 𝓜₂ 2 := by + constructor <;> intro h + · simp only [h, implies_true] + · ext1; exact h + +end Relational₂ + +end Structure --end + +end FirstOrder.Language diff --git a/FormalTextbookModelTheory/ForMathlib/Matrix.lean b/FormalTextbookModelTheory/ForMathlib/Matrix.lean new file mode 100644 index 0000000..7543902 --- /dev/null +++ b/FormalTextbookModelTheory/ForMathlib/Matrix.lean @@ -0,0 +1,27 @@ +import Mathlib.Data.Fin.VecNotation +import Mathlib.Logic.Equiv.Fin + +namespace Matrix + +variable {α : Type*} + +lemma Vector_eq_VecNotation₂ (v : Fin 2 → α) : v = ![v 0, v 1] := by + simp only [vecCons] + induction (‹_› : Fin _ → α) using Fin.consCases + simp only [Fin.cons_eq_cons] + induction (‹_› : Fin _ → α) using Fin.consCases + simp only [Fin.cons_eq_cons] + simp only [Fin.cons_zero, Fin.cons_one, true_and] + apply (by infer_instance : Subsingleton (Fin 0 → α)).allEq + +end Matrix + +/- +lemma Vector_eq_VecNotation (v : Fin 2 → α) : v = ![v 0, v 1] := by + simp only [vecCons] + + repeat induction (‹_› : Fin _ → α) using Fin.consCases; simp only [Fin.cons_eq_cons] + + simp [Fin.cons_zero, Fin.cons_one] + apply (by infer_instance : Subsingleton (Fin 0 → α)).allEq +-/ diff --git a/FormalTextbookModelTheory/ForMathlib/Order.lean b/FormalTextbookModelTheory/ForMathlib/Order.lean new file mode 100644 index 0000000..cd6e434 --- /dev/null +++ b/FormalTextbookModelTheory/ForMathlib/Order.lean @@ -0,0 +1,324 @@ +import Mathlib.SetTheory.Cardinal.Basic +import Mathlib.ModelTheory.Basic +import Mathlib.ModelTheory.Satisfiability +import Mathlib.ModelTheory.Order +import Mathlib.Order.CountableDenseLinearOrder +import Mathlib.Order.Basic +import FormalTextbookModelTheory.ForMathlib.Matrix +import FormalTextbookModelTheory.ForMathlib.Language + +universe u v w + +open Cardinal +open Matrix +open FirstOrder Language Theory Order Structure + +namespace FirstOrder.Language.Order --{{{ + +section Language.order + +scoped notation "L≤" => Language.order + +instance instIsRelational₂: IsRelational₂ L≤ where + empty_functions := Language.instIsRelational.empty_functions + only_rel₂ := by + intro n hn + simp only [Language.order, Language.mk₂, Sequence₂] + match n with + | 0 => exact instIsEmptyPEmpty + | 1 => exact instIsEmptyEmpty + | 2 => contradiction + | _ + 3 => exact instIsEmptyPEmpty + +end Language.order + +section LE + +#check (@orderStructure) + +#check (@orderLHom) + +#check (@OrderedStructure) +/- +tabiki L≤.Structure yapisi orderStructure ile LE M den infer ediliyor. +orderLHom : L≤ →ᴸ L homomorphismasinin expansion oldugunu soyluyor. +-/ + +#check (@orderedStructure_LE) +/- +bu baya trivial bir sey. orderLHom : L≤ →ᴸ L≤ zaten identity. bunun bir expansion oldugunu soyluyor. +-/ + +def inst_LE_of_IsOrdered + (L : Language.{u, v}) [IsOrdered L] {M : Type w} [L.Structure M] : LE M where + le := fun x y => (@RelMap L M _ 2 leSymb) ![x, y] + +#check (@inst_LE_of_IsOrdered) +/- +burada da ordered bir languageden LE M turetiyoruz. +-/ + +@[simp] +lemma orderStructure_of_LE_of_structure {M : Type w} [inst : L≤.Structure M] + : @orderStructure M (inst_LE_of_IsOrdered L≤) = inst := by + ext r₂ m + simp only [orderStructure, inst_LE_of_IsOrdered] + rw [Vector_eq_VecNotation₂ m, relMap_apply₂] + simp only [Nat.succ_eq_add_one, Nat.reduceAdd] + rw [←eq_iff_iff] + apply congrArg (fun s => RelMap s _) + apply Subsingleton.allEq +/- +bu aslinda onemli. L≤.Structure M --(inst_LE_of_IsOrdered)--> LE M --(orderStructure)--> L≤.Structure M isleminin +bizi ayni noktaya getirdigini soyluyor. +-/ + +end LE + +section IsOrdered + +variable {L : Language.{u, v}} [instIsOrdered : IsOrdered L] +variable {M : Type w} [instStructure : L.Structure M] + +lemma OrderedStructure_of_IsOrdered + : @OrderedStructure L M instIsOrdered (inst_LE_of_IsOrdered L) instStructure := by + let inst : L≤.Structure M := by exact @orderStructure M (inst_LE_of_IsOrdered L) + simp only [OrderedStructure] + refine { + map_onFunction := by simp only [IsEmpty.forall_iff, implies_true] + map_onRelation := ?map_onRelation + } + intro n + match n with + | 0 | 1 | _ + 3 => + simp only [Language.order, mk₂_Relations, Sequence₂, instIsEmptyPEmpty, IsEmpty.forall_iff] + | 2 => + intro _ x + rw [Vector_eq_VecNotation₂ x] + simp only [inst_LE_of_IsOrdered, orderStructure_of_LE_of_structure, relMap_apply₂] + apply congrArg (fun r => @RelMap L M instStructure 2 r ![x 0, x 1]) + rfl + +section LinearOrder + +lemma linearOrderTheory_subset_dlo : L.linearOrderTheory ⊆ L.dlo := by + simp only [dlo] + exact Set.subset_union_left + +lemma reflexive_in_linearOrderTheory : leSymb.reflexive ∈ L.linearOrderTheory := by + simp only [linearOrderTheory, Set.mem_insert_iff, Set.mem_singleton_iff, true_or] + +lemma transitive_in_linearOrderTheory : leSymb.transitive ∈ L.linearOrderTheory := by + simp only [linearOrderTheory, Set.mem_insert_iff, Set.mem_singleton_iff, true_or, or_true] + +lemma antisymmetric_in_linearOrderTheory : leSymb.antisymmetric ∈ L.linearOrderTheory := by + simp only [linearOrderTheory, Set.mem_insert_iff, Set.mem_singleton_iff, true_or, or_true, or_true] + +lemma total_in_linearOrderTheory : leSymb.total ∈ L.linearOrderTheory := by + simp only [linearOrderTheory, Set.mem_insert_iff, Set.mem_singleton_iff, true_or, or_true, or_true, or_true] + +lemma realize_reflexive_of_model_linearOrderTheory (h : M ⊨ L.linearOrderTheory) + : M ⊨ (leSymb (L := L)).reflexive := by + simp only [model_iff] at h + replace h := h leSymb.reflexive reflexive_in_linearOrderTheory + exact h + +lemma realize_transitive_of_model_linearOrderTheory (h : M ⊨ L.linearOrderTheory) + : M ⊨ (leSymb (L := L)).transitive := by + simp only [model_iff] at h + replace h := h leSymb.transitive transitive_in_linearOrderTheory + exact h + +lemma realize_antisymmetric_of_model_linearOrderTheory (h : M ⊨ L.linearOrderTheory) + : M ⊨ (leSymb (L := L)).antisymmetric := by + simp only [model_iff] at h + replace h := h leSymb.antisymmetric antisymmetric_in_linearOrderTheory + exact h + +lemma realize_total_of_model_linearOrderTheory (h : M ⊨ L.linearOrderTheory) + : M ⊨ (leSymb (L := L)).total := by + simp only [model_iff] at h + replace h := h leSymb.total total_in_linearOrderTheory + exact h + +end LinearOrder + +section DLO + +section + +variable {L : Language.{u, v}} [instIsOrdered : IsOrdered L] + +lemma reflexive_in_dlo : leSymb.reflexive ∈ L.dlo := + linearOrderTheory_subset_dlo reflexive_in_linearOrderTheory + +lemma transitive_in_dlo : leSymb.transitive ∈ L.dlo := + linearOrderTheory_subset_dlo transitive_in_linearOrderTheory + +lemma antisymmetry_in_dlo : leSymb.antisymmetric ∈ L.dlo := + linearOrderTheory_subset_dlo antisymmetric_in_linearOrderTheory + +lemma total_in_dlo : leSymb.total ∈ L.dlo := + linearOrderTheory_subset_dlo total_in_linearOrderTheory + +lemma denselyOrderedSentence_in_dlo : L.denselyOrderedSentence ∈ L.dlo := by + simp only [dlo, Set.union_insert, Set.union_singleton, Set.mem_insert_iff, true_or, or_true] + +end + +section + +variable {L : Language.{u, v}} [instIsOrdered : IsOrdered L] +variable {M : Type w} [instStructure : L.Structure M] + +lemma realize_reflexive_of_model_dlo (h : M ⊨ L.dlo) : M ⊨ (leSymb (L := L)).reflexive := by + simp only [model_iff] at h + replace h := h leSymb.reflexive reflexive_in_dlo + exact h + +lemma realize_transitive_of_model_dlo (h : M ⊨ L.dlo) : M ⊨ (leSymb (L := L)).transitive := by + simp only [model_iff] at h + replace h := h leSymb.transitive transitive_in_dlo + exact h + +lemma model_linearOrderTheory_of_model_dlo (h : M ⊨ L.dlo) : M ⊨ L.linearOrderTheory := by + simp [model_iff] at * + intro φ hφ + exact h φ (linearOrderTheory_subset_dlo hφ) + +lemma realize_denselyOrderedSentence_of_model_dlo (h : M ⊨ L.dlo) : M ⊨ L.denselyOrderedSentence := by + simp only [model_iff] at h + replace h := h L.denselyOrderedSentence denselyOrderedSentence_in_dlo + exact h + +end + +section + +variable (L : Language.{u, v}) [instIsOrdered : IsOrdered L] +variable {M : Type w} [instStructure : L.Structure M] [instModel : M ⊨ L.dlo] + +def inst_Preorder_of_dlo : Preorder M where + le := (inst_LE_of_IsOrdered L).le + le_refl := by + have := realize_reflexive_of_model_dlo instModel + simp only [Relations.realize_reflexive, Reflexive] at this + exact this + le_trans := by + have := realize_transitive_of_model_dlo instModel + simp only [Relations.realize_transitive, Transitive] at this + exact this + +noncomputable def inst_LinearOrder_of_dlo : LinearOrder M where + toPreorder := inst_Preorder_of_dlo L + le_antisymm := by + have := realize_antisymmetric_of_model_linearOrderTheory + (model_linearOrderTheory_of_model_dlo instModel) + simp only [Relations.realize_antisymmetric, Antisymm] at this + exact this + le_total := by + have := realize_total_of_model_linearOrderTheory + (model_linearOrderTheory_of_model_dlo instModel) + simp only [Relations.realize_total, Total] at this + exact this + decidableLE := Classical.decRel _ + +def inst_DenselyOrdered_of_dlo : @DenselyOrdered M (inst_Preorder_of_dlo L).toLT := by + + have : M ⊨ L.denselyOrderedSentence := realize_denselyOrderedSentence_of_model_dlo instModel + + simp only [Sentence.Realize, denselyOrderedSentence, Formula.Realize, BoundedFormula.realize_all, + BoundedFormula.realize_imp, BoundedFormula.realize_ex, BoundedFormula.realize_inf] at this + + let _ : LT M := (inst_Preorder_of_dlo L).toLT + refine { + dense := ?dense + } + + intro a b h + replace this := this a b + simp only [ + @Term.realize_lt L _ M 2 instIsOrdered instStructure (inst_Preorder_of_dlo L) OrderedStructure_of_IsOrdered] at this + replace this := this h + rcases this with ⟨a₂, ⟨h₁, h₂⟩⟩ + use a₂ + simp only [ + @Term.realize_lt L _ M 3 instIsOrdered instStructure (inst_Preorder_of_dlo L) OrderedStructure_of_IsOrdered, + Function.comp_apply] at h₁ h₂ + exact ⟨h₁, h₂⟩ + +end + +end DLO + +end IsOrdered + +end FirstOrder.Language.Order --}}} + +namespace FirstOrder + +namespace Language + +/- +section + +variable {L : Language.{u, v}} [IsOrdered L] {M : Type w} [L.Structure M] + +theorem realize_sentence_of_mem_of_model_theory + {T : Theory L} (h : M ⊨ T) {p : L.Sentence} (hp : p ∈ T) : M ⊨ p := by + simp only [model_iff] at h + exact h p hp + +theorem model_theory_of_subset_of_model_theory {T T' : Theory L} (h : T' ⊆ T) (hT : M ⊨ T) : + M ⊨ T' := by + simp only [model_iff] at * + intro φ hφ + exact hT φ (h hφ) + +theorem realize_reflexive_of_model_linearOrderTheory (h : M ⊨ L.linearOrderTheory) : + M ⊨ (leSymb (L := L)).reflexive := + realize_sentence_of_mem_of_model_theory h reflexive_in_linearOrderTheory + +end +-/ + +/- +section -- {{{ + +variable {M : Type w} [inst₁ : L≤.Structure M] + +theorem realize_reflexive_iff : M ⊨ (leSymb (L := L≤)).reflexive ↔ ∀ a : M, a ≤ a := by + simp only [Relations.realize_reflexive, Reflexive] + constructor <;> {intro; assumption} + +theorem realize_transitive_iff + : M ⊨ (leSymb (L := L≤)).transitive ↔ ∀ (a b c : M), a ≤ b → b ≤ c → a ≤ c := by + simp only [Relations.realize_transitive, Transitive] + constructor <;> {intro; assumption} + +instance [inst : M ⊨ L≤.dlo] : Preorder M where + le := (· ≤ ·) + le_refl := by + apply realize_reflexive_iff.1 + apply realize_sentence_of_mem_of_model_theory inst + apply reflexive_in_dlo + le_trans := by + apply realize_transitive_iff.1 + apply realize_sentence_of_mem_of_model_theory inst + apply transitive_in_dlo + +instance [inst : M ⊨ L≤.dlo] : DenselyOrdered M := by + apply realize_denselyOrdered_iff.mp + #check @realize_sentence_of_mem L≤ M inst₁ L≤.dlo inst L≤.denselyOrderedSentence + apply @realize_sentence_of_mem L≤ M inst₁ L≤.dlo inst L≤.denselyOrderedSentence + sorry + +#check realize_denselyOrdered_iff +#check realize_sentence_of_mem + +end -- }}} +-/ + +end Language + +end FirstOrder diff --git a/FormalTextbookModelTheory/ForMathlib2/Cardinal.lean b/FormalTextbookModelTheory/ForMathlib2/Cardinal.lean new file mode 100644 index 0000000..7d4dfff --- /dev/null +++ b/FormalTextbookModelTheory/ForMathlib2/Cardinal.lean @@ -0,0 +1,7 @@ +import Mathlib.SetTheory.Cardinal.Basic + +namespace Cardinal + +instance countable_of_mk_eq_aleph0 {α : Type w} (h : #α = ℵ₀) : Countable α := by + apply mk_le_aleph0_iff.mp + rw [h] diff --git a/FormalTextbookModelTheory/ForMathlib2/DLO.lean b/FormalTextbookModelTheory/ForMathlib2/DLO.lean new file mode 100644 index 0000000..e4a228b --- /dev/null +++ b/FormalTextbookModelTheory/ForMathlib2/DLO.lean @@ -0,0 +1,218 @@ +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.ForMathlib2.Matrix +import FormalTextbookModelTheory.ForMathlib2.Cardinal + +open Cardinal +open FirstOrder Language Structure Theory Order +open Matrix (Vector_eq_VecNotation₂ comp_VecNotation₂) + +namespace FirstOrder.Language.Order --region + +section + +variable {M : Type w} [instStructure : Language.order.Structure M] + +instance instLE : LE M where + le := fun x y => instStructure.RelMap leSymb ![x, y] + +@[simp] +lemma orderStructure_of_LE : @orderStructure M instLE = 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₂] + +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] + +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 + +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] + +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 + +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 + +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 + +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 + +protected lemma realize_denselyOrderedSentence : M ⊨ Language.order.denselyOrderedSentence := by + apply realize_sentence_of_mem Language.order.dlo + unfold dlo linearOrderTheory + right; right; right; rfl + +protected lemma realize_noBotOrderSentence : M ⊨ Language.order.noBotOrderSentence := by + apply realize_sentence_of_mem Language.order.dlo + unfold dlo linearOrderTheory + right; right; left; rfl + +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 + -- 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 + 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 instDenselyOrdered : 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 + +/-- +This is my docstring +-/ +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_of_mk_eq_aleph0 hM + have := countable_of_mk_eq_aleph0 hN + apply iso_of_countable_dense + +end DLO --end + +end FirstOrder.Language.Order --end diff --git a/FormalTextbookModelTheory/ForMathlib2/Matrix.lean b/FormalTextbookModelTheory/ForMathlib2/Matrix.lean new file mode 100644 index 0000000..817b50e --- /dev/null +++ b/FormalTextbookModelTheory/ForMathlib2/Matrix.lean @@ -0,0 +1,25 @@ +import Mathlib.Data.Fin.VecNotation +import Mathlib.Logic.Equiv.Fin + +namespace Matrix + +variable {α β: Type*} + +lemma Vector_eq_VecNotation₂ (v : Fin 2 → α) : v = ![v 0, v 1] := by + simp only [vecCons] + induction (‹_› : Fin _ → α) using Fin.consCases + simp only [Fin.cons_eq_cons] + induction (‹_› : Fin _ → α) using Fin.consCases + simp only [Fin.cons_eq_cons] + simp only [Fin.cons_zero, Fin.cons_one, true_and] + apply (by infer_instance : Subsingleton (Fin 0 → α)).allEq + +@[simp] +lemma comp_VecNotation₂ (f : α → β) (x y : α) : f ∘ ![x, y] = ![f x, f y] := by + ext x + rcases x with ⟨i, h⟩ + match i with + | 0 => rfl + | 1 => rfl + +end Matrix diff --git a/blueprint/lean_decls b/blueprint/lean_decls index 7273999..5a7a444 100644 --- a/blueprint/lean_decls +++ b/blueprint/lean_decls @@ -1 +1,30 @@ -aleph0_categorical_of_dlo \ No newline at end of file +Matrix.Vector_eq_VecNotation₂ +FirstOrder.Language.Order.linearOrderTheory_subset_dlo +FirstOrder.Language.Order.reflexive_in_linearOrderTheory +FirstOrder.Language.Order.transitive_in_linearOrderTheory +FirstOrder.Language.Order.antisymmetric_in_linearOrderTheory +FirstOrder.Language.Order.total_in_linearOrderTheory +FirstOrder.Language.Order.realize_reflexive_of_model_linearOrderTheory +FirstOrder.Language.Order.realize_transitive_of_model_linearOrderTheory +FirstOrder.Language.Order.realize_antisymmetric_of_model_linearOrderTheory +FirstOrder.Language.Order.realize_total_of_model_linearOrderTheory +FirstOrder.Language.Order.reflexive_in_dlo +FirstOrder.Language.Order.transitive_in_dlo +FirstOrder.Language.Order.antisymmetric_in_dlo +FirstOrder.Language.Order.total_in_dlo +FirstOrder.Language.Order.realize_reflexive_of_model_dlo +FirstOrder.Language.Order.realize_transitive_of_model_dlo +FirstOrder.Language.Order.realize_antisymmetric_of_model_dlo +FirstOrder.Language.Order.realize_total_of_model_dlo +FirstOrder.Language.Order.model_linearOrderTheory_of_model_dlo +FirstOrder.Language.Order.inst_LE_of_IsOrdered +FirstOrder.Language.Order.inst_Preorder_of_dlo +FirstOrder.Language.Order.inst_LinearOrder_of_dlo +FirstOrder.Language.IsRelational₂ +FirstOrder.Language.Order.instIsRelational₂ +FirstOrder.Language.Structure.funMap_eq_funMap_of_relational +FirstOrder.Language.Structure.structure_eq_structure_of_relational_iff +FirstOrder.Language.Structure.RelMap_eq_RelMap_of_relational₂ +FirstOrder.Language.Structure.structure_eq_of_structure_of_relational₂_iff +FirstOrder.Language.Order.orderStructure_of_LE_of_structure +FirstOrder.Language.Order.aleph0_categorical_of_dlo \ No newline at end of file diff --git a/blueprint/print/print.aux b/blueprint/print/print.aux index f7ac61a..6e454d2 100644 --- a/blueprint/print/print.aux +++ b/blueprint/print/print.aux @@ -3,5 +3,44 @@ \providecommand*\HyPL@Entry[1]{} \HyPL@Entry{0<>} \HyPL@Entry{1<>} -\newlabel{thm:aleph0_categorical_of_dlo}{{0.0.1}{1}{Cantor 1874}{theorem.0.0.1}{}} -\gdef \@abspage@last{2} +\@writefile{toc}{\contentsline {chapter}{\numberline {1}Basic Definitions and Lemmas}{1}{chapter.1}\protected@file@percent } +\@writefile{lof}{\addvspace {10\p@ }} +\@writefile{lot}{\addvspace {10\p@ }} +\@writefile{toc}{\contentsline {section}{\numberline {1.1}Vectors}{1}{section.1.1}\protected@file@percent } +\newlabel{lem:two-vector-notation}{{1.1.1}{1}{}{theorem.1.1.1}{}} +\@writefile{toc}{\contentsline {section}{\numberline {1.2}Theories}{1}{section.1.2}\protected@file@percent } +\newlabel{lem:linear-order-theory-in-dlo}{{1.2.1}{1}{}{theorem.1.2.1}{}} +\newlabel{lem:reflexive-in-linear-order-theory}{{1.2.2}{1}{}{theorem.1.2.2}{}} +\newlabel{lem:transitive-in-linear-order-theory}{{1.2.3}{1}{}{theorem.1.2.3}{}} +\newlabel{lem:antisymmetric-in-linear-order-theory}{{1.2.4}{1}{}{theorem.1.2.4}{}} +\newlabel{lem:total-in-linear-order-theory}{{1.2.5}{1}{}{theorem.1.2.5}{}} +\newlabel{lem:models-of-linearOrderTheory-realize-reflexive}{{1.2.6}{1}{}{theorem.1.2.6}{}} +\newlabel{lem:models-of-linearOrderTheory-realize-transitive}{{1.2.7}{1}{}{theorem.1.2.7}{}} +\newlabel{lem:models-of-linearOrderTheory-realize-antisymmetric}{{1.2.8}{1}{}{theorem.1.2.8}{}} +\newlabel{lem:models-of-linearOrderTheory-realize-total}{{1.2.9}{2}{}{theorem.1.2.9}{}} +\newlabel{lem:reflexive-in-dlo}{{1.2.10}{2}{}{theorem.1.2.10}{}} +\newlabel{lem:transitive-in-dlo}{{1.2.11}{2}{}{theorem.1.2.11}{}} +\newlabel{lem:antisymmetric-in-dlo}{{1.2.12}{2}{}{theorem.1.2.12}{}} +\newlabel{lem:total-in-dlo}{{1.2.13}{2}{}{theorem.1.2.13}{}} +\newlabel{lem:models-of-dlo-realize-reflexivity}{{1.2.14}{2}{}{theorem.1.2.14}{}} +\newlabel{lem:models-of-dlo-realize-transitivity}{{1.2.15}{2}{}{theorem.1.2.15}{}} +\newlabel{lem:models-of-dlo-realize-antisymmetric}{{1.2.16}{2}{}{theorem.1.2.16}{}} +\newlabel{lem:models-of-dlo-realize-total}{{1.2.17}{2}{}{theorem.1.2.17}{}} +\newlabel{lem:models-of-dlo-models-of-linear-order-theory}{{1.2.18}{2}{}{theorem.1.2.18}{}} +\@writefile{toc}{\contentsline {section}{\numberline {1.3}Instances}{2}{section.1.3}\protected@file@percent } +\newlabel{def:le-instance-ordered-language}{{1.3.1}{2}{}{theorem.1.3.1}{}} +\newlabel{def:preorder-instance-models-of-dlo}{{1.3.2}{2}{}{theorem.1.3.2}{}} +\newlabel{def:linear-order-instance-models-of-dlo}{{1.3.3}{2}{}{theorem.1.3.3}{}} +\newlabel{def:binary-relational-language}{{1.3.4}{2}{}{theorem.1.3.4}{}} +\newlabel{lem:canonical-ordered-language-binary-relational}{{1.3.5}{2}{}{theorem.1.3.5}{}} +\@writefile{toc}{\contentsline {section}{\numberline {1.4}Structures}{3}{section.1.4}\protected@file@percent } +\newlabel{lem:structure-funmap-relational-language}{{1.4.1}{3}{}{theorem.1.4.1}{}} +\newlabel{lem:equality-of-structures-relational-language}{{1.4.2}{3}{}{theorem.1.4.2}{}} +\newlabel{lem:structure-relmap-binary-relational-language}{{1.4.3}{3}{}{theorem.1.4.3}{}} +\newlabel{lem:equality-of-structures-binary-relational-language}{{1.4.4}{3}{}{theorem.1.4.4}{}} +\newlabel{lem:orders-coincide-for-ordered-structures}{{1.4.5}{3}{}{theorem.1.4.5}{}} +\@writefile{toc}{\contentsline {chapter}{\numberline {2}Main Results}{4}{chapter.2}\protected@file@percent } +\@writefile{lof}{\addvspace {10\p@ }} +\@writefile{lot}{\addvspace {10\p@ }} +\newlabel{thm:dlo-aleph0-categorical}{{2.0.1}{4}{}{theorem.2.0.1}{}} +\gdef \@abspage@last{5} diff --git a/blueprint/print/print.fdb_latexmk b/blueprint/print/print.fdb_latexmk index 3ac2e9b..ac84b00 100644 --- a/blueprint/print/print.fdb_latexmk +++ b/blueprint/print/print.fdb_latexmk @@ -1,7 +1,7 @@ # Fdb version 4 -["pdflatex"] 1722426513.46275 "print.tex" "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.pdf" "print" 1722426514.32728 0 - "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.aux" 1722426514.12015 234 44cfa93580110f5bdc2c3c0199a36f3e "pdflatex" - "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.out" 1722426513.93115 0 d41d8cd98f00b204e9800998ecf8427e "pdflatex" +["pdflatex"] 1722842215.45552 "print.tex" "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.pdf" "print" 1722842216.35635 0 + "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.aux" 1722842216.13454 3389 9986f5bb805a7d456894f1ab84f2a2a4 "pdflatex" + "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.out" 1722842216.13454 684 cd11907768ebb096d11426bf84b99804 "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,10 +83,12 @@ "/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 "" - "content.tex" 1722426507.36388 1013 127fde10c82afc237f22f137d2d5379f "" - "macros/common.tex" 1722424368.23936 548 4554adb8a1b3c5da12b67499d6b2b610 "" + "chapters/basics.tex" 1722842210.89455 9444 d7c98278eb22bd3c0fd530b347cabe4f "" + "chapters/main.tex" 1722838314.15515 270 abcdeb6fca3851372d9a5ff1023c4753 "" + "content.tex" 1722838307.94514 917 7d022bbdd7c27336a23d62a729ff0c4b "" + "macros/common.tex" 1722759673.52174 604 ca3e9443483cfefd693019fb112f2d18 "" "macros/print.tex" 1722422546.45932 1101 87627b2ec24fef68edc71c13f43f7bab "" - "print.tex" 1722422546.45932 1131 bf5d368546e76888c21bf562766212eb "" + "print.tex" 1722837065.5925 1131 bf5d368546e76888c21bf562766212eb "" (generated) "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.aux" "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.log" diff --git a/blueprint/print/print.fls b/blueprint/print/print.fls index 24ca36e..d7313d4 100644 --- a/blueprint/print/print.fls +++ b/blueprint/print/print.fls @@ -183,12 +183,18 @@ INPUT ./content.tex INPUT ./content.tex INPUT ./content.tex INPUT content.tex +INPUT ./chapters/basics.tex +INPUT ./chapters/basics.tex +INPUT chapters/basics.tex INPUT /usr/local/texlive/2024/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm INPUT /usr/local/texlive/2024/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam7.tfm INPUT /usr/local/texlive/2024/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam5.tfm INPUT /usr/local/texlive/2024/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm INPUT /usr/local/texlive/2024/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm7.tfm INPUT /usr/local/texlive/2024/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm5.tfm +INPUT ./chapters/main.tex +INPUT ./chapters/main.tex +INPUT chapters/main.tex INPUT /home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.aux INPUT /home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.out INPUT /home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.out diff --git a/blueprint/print/print.log b/blueprint/print/print.log index fd830b1..6524026 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) 31 JUL 2024 14:48 +This is XeTeX, Version 3.141592653-2.6-0.999996 (TeX Live 2024) (preloaded format=xelatex 2024.7.31) 5 AUG 2024 10:16 entering extended mode restricted \write18 enabled. %&-line parsing enabled. @@ -669,37 +669,71 @@ File: umsb.fd 2013/01/14 v3.01 AMS symbols B [1 ] (./content.tex +Chapter 1. +(./chapters/basics.tex LaTeX Font Info: Font shape `TU/latinmodern-math.otf(2)/m/n' will be -(Font) scaled to size 10.00107pt on input line 28. +(Font) scaled to size 10.00107pt on input line 9. LaTeX Font Info: Font shape `TU/latinmodern-math.otf(2)/m/n' will be -(Font) scaled to size 7.00075pt on input line 28. +(Font) scaled to size 7.00075pt on input line 9. LaTeX Font Info: Font shape `TU/latinmodern-math.otf(2)/m/n' will be -(Font) scaled to size 5.00053pt on input line 28. +(Font) scaled to size 5.00053pt on input line 9. LaTeX Font Info: Font shape `TU/latinmodern-math.otf(3)/m/n' will be -(Font) scaled to size 9.99893pt on input line 28. +(Font) scaled to size 9.99893pt on input line 9. LaTeX Font Info: Font shape `TU/latinmodern-math.otf(3)/m/n' will be -(Font) scaled to size 6.99925pt on input line 28. +(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 28. -) +(Font) scaled to size 4.99947pt on input line 9. + + +LaTeX Warning: Reference `lem:reflexive-in-linearOrderTheory' on page 1 undefin +ed on input line 78. + + +LaTeX Warning: Reference `lem:transitive-in-linearOrderTheory' on page 1 undefi +ned on input line 89. + + +LaTeX Warning: Reference `lem:antisymmetric-in-linearOrderTheory' on page 1 und +efined on input line 100. + + +LaTeX Warning: Reference `lem:total-in-linearOrderTheory' on page 1 undefined o +n input line 111. + -[1] + +[1 + +] + +[2]) + +[3] +Chapter 2. +(./chapters/main.tex)) + +[4 + +] (/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.aux) *********** LaTeX2e <2024-06-01> patch level 2 L3 programming layer <2024-05-27> *********** + +LaTeX Warning: There were undefined references. + Package rerunfilecheck Info: File `print.out' has not changed. -(rerunfilecheck) Checksum: D41D8CD98F00B204E9800998ECF8427E;0. +(rerunfilecheck) Checksum: CD11907768EBB096D11426BF84B99804;684. ) Here is how much of TeX's memory you used: - 16728 strings out of 474240 - 307900 string characters out of 5742353 - 1920557 words of memory out of 5000000 - 39223 multiletter control sequences out of 15000+600000 - 563384 words of font info for 78 fonts, out of 8000000 for 9000 + 16803 strings out of 474240 + 310097 string characters out of 5742353 + 1932557 words of memory out of 5000000 + 39281 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,353s stack positions out of 10000i,1000n,20000p,200000b,200000s + 90i,6n,116p,542b,467s stack positions out of 10000i,1000n,20000p,200000b,200000s Output written on /home/metinersin/projects/FormalTextbookModelTheory/blueprint -/print/print.pdf (2 pages). +/print/print.pdf (5 pages). diff --git a/blueprint/print/print.out b/blueprint/print/print.out index e69de29..465edbd 100644 --- a/blueprint/print/print.out +++ b/blueprint/print/print.out @@ -0,0 +1,6 @@ +\BOOKMARK [0][-]{chapter.1}{\376\377\000B\000a\000s\000i\000c\000\040\000D\000e\000f\000i\000n\000i\000t\000i\000o\000n\000s\000\040\000a\000n\000d\000\040\000L\000e\000m\000m\000a\000s}{}% 1 +\BOOKMARK [1][-]{section.1.1}{\376\377\000V\000e\000c\000t\000o\000r\000s}{chapter.1}% 2 +\BOOKMARK [1][-]{section.1.2}{\376\377\000T\000h\000e\000o\000r\000i\000e\000s}{chapter.1}% 3 +\BOOKMARK [1][-]{section.1.3}{\376\377\000I\000n\000s\000t\000a\000n\000c\000e\000s}{chapter.1}% 4 +\BOOKMARK [1][-]{section.1.4}{\376\377\000S\000t\000r\000u\000c\000t\000u\000r\000e\000s}{chapter.1}% 5 +\BOOKMARK [0][-]{chapter.2}{\376\377\000M\000a\000i\000n\000\040\000R\000e\000s\000u\000l\000t\000s}{}% 6 diff --git a/blueprint/print/print.pdf b/blueprint/print/print.pdf index 298fac9..b9f8e31 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 c73a33a..9c8e33b 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 new file mode 100644 index 0000000..a2f8fc7 --- /dev/null +++ b/blueprint/src/chapters/basics.tex @@ -0,0 +1,336 @@ + +\section{Vectors} +%%% Really trivial stuff about numbers, vectors, etc. + +\begin{lemma} + \label{lem:two-vector-notation} + \lean{Matrix.Vector_eq_VecNotation₂} + \leanok + For any vector $v : \Fin 2 \to \bbn$, we have $v = ![v(0), v(1)]$. +\end{lemma} +\begin{proof} + \leanok +\end{proof} +%%% + +\section{Theories} +%%% Really trivial stuff about theories + +\begin{lemma} + \label{lem:linear-order-theory-in-dlo} + \lean{FirstOrder.Language.Order.linearOrderTheory_subset_dlo} + \leanok + The theory of linear orders is a subset of DLO. +\end{lemma} +\begin{proof} + \leanok +\end{proof} + +%%%% LinearOrder +\begin{lemma} + \label{lem:reflexive-in-linear-order-theory} + \lean{FirstOrder.Language.Order.reflexive_in_linearOrderTheory} + \leanok + The theory of linear orders contains the reflexivity sentence. +\end{lemma} +\begin{proof} + \leanok +\end{proof} + +\begin{lemma} + \label{lem:transitive-in-linear-order-theory} + \lean{FirstOrder.Language.Order.transitive_in_linearOrderTheory} + \leanok + The theory of linear orders contains the transitivity sentence. +\end{lemma} +\begin{proof} + \leanok +\end{proof} + +\begin{lemma} + \label{lem:antisymmetric-in-linear-order-theory} + \lean{FirstOrder.Language.Order.antisymmetric_in_linearOrderTheory} + \leanok + The theory of linear orders contains the antisymmetry sentence. +\end{lemma} +\begin{proof} + \leanok +\end{proof} + +\begin{lemma} + \label{lem:total-in-linear-order-theory} + \lean{FirstOrder.Language.Order.total_in_linearOrderTheory} + \leanok + The theory of linear orders contains the totality sentence. +\end{lemma} +\begin{proof} + \leanok +\end{proof} + +\begin{lemma} + \label{lem:models-of-linearOrderTheory-realize-reflexive} + \lean{FirstOrder.Language.Order.realize_reflexive_of_model_linearOrderTheory} + \leanok + Models of the theory of linear orders realize the reflexivity sentence. +\end{lemma} +\begin{proof} + \leanok + \uses{lem:reflexive-in-linearOrderTheory} +\end{proof} + +\begin{lemma} + \label{lem:models-of-linearOrderTheory-realize-transitive} + \lean{FirstOrder.Language.Order.realize_transitive_of_model_linearOrderTheory} + \leanok + Models of the theory of linear orders realize the transitivity sentence. +\end{lemma} +\begin{proof} + \leanok + \uses{lem:transitive-in-linearOrderTheory} +\end{proof} + +\begin{lemma} + \label{lem:models-of-linearOrderTheory-realize-antisymmetric} + \lean{FirstOrder.Language.Order.realize_antisymmetric_of_model_linearOrderTheory} + \leanok + Models of the theory of linear orders realize the antisymmetry sentence. +\end{lemma} +\begin{proof} + \leanok + \uses{lem:antisymmetric-in-linearOrderTheory} +\end{proof} + +\begin{lemma} + \label{lem:models-of-linearOrderTheory-realize-total} + \lean{FirstOrder.Language.Order.realize_total_of_model_linearOrderTheory} + \leanok + Models of the theory of linear orders realize the totality sentence. +\end{lemma} +\begin{proof} + \leanok + \uses{lem:total-in-linearOrderTheory} +\end{proof} + +%%%% + +%%%% DLO +\begin{lemma} + \label{lem:reflexive-in-dlo} + \lean{FirstOrder.Language.Order.reflexive_in_dlo} + \leanok + The theory DLO contains the reflexivity sentence. +\end{lemma} +\begin{proof} + \leanok + \uses{lem:linear-order-theory-in-dlo, lem:reflexive-in-linear-order-theory} +\end{proof} + +\begin{lemma} + \label{lem:transitive-in-dlo} + \lean{FirstOrder.Language.Order.transitive_in_dlo} + \leanok + The theory DLO contains the transitivity sentence +\end{lemma} +\begin{proof} + \leanok + \uses{lem:linear-order-theory-in-dlo, lem:transitive-in-linear-order-theory} +\end{proof} + +\begin{lemma} + \label{lem:antisymmetric-in-dlo} + \lean{FirstOrder.Language.Order.antisymmetric_in_dlo} + \leanok + The theory DLO contains the antisymmetry sentence. +\end{lemma} +\begin{proof} + \leanok + \uses{lem:linear-order-theory-in-dlo, lem:antisymmetric-in-linear-order-theory} +\end{proof} + +\begin{lemma} + \label{lem:total-in-dlo} + \lean{FirstOrder.Language.Order.total_in_dlo} + \leanok + The theory DLO contains the totality sentence. +\end{lemma} +\begin{proof} + \leanok + \uses{lem:linear-order-theory-in-dlo, lem:total-in-linear-order-theory} +\end{proof} + +\begin{lemma} + \label{lem:models-of-dlo-realize-reflexivity} + \lean{FirstOrder.Language.Order.realize_reflexive_of_model_dlo} + \leanok + Models of the theory DLO realize the reflexivity sentence. +\end{lemma} +\begin{proof} + \leanok + \uses{lem:reflexive-in-dlo} +\end{proof} + +\begin{lemma} + \label{lem:models-of-dlo-realize-transitivity} + \lean{FirstOrder.Language.Order.realize_transitive_of_model_dlo} + \leanok + Models of the theory DLO realize the transitivity sentence. +\end{lemma} +\begin{proof} + \leanok + \uses{lem:transitive-in-dlo} +\end{proof} + +\begin{lemma} + \label{lem:models-of-dlo-realize-antisymmetric} + \lean{FirstOrder.Language.Order.realize_antisymmetric_of_model_dlo} + \leanok + Models of the theory DLO realize the antisymmetry sentence. +\end{lemma} +\begin{proof} + \leanok + \uses{lem:antisymmetric-in-dlo} +\end{proof} + +\begin{lemma} + \label{lem:models-of-dlo-realize-total} + \lean{FirstOrder.Language.Order.realize_total_of_model_dlo} + \leanok + Models of the theory DLO realize the totality sentence. +\end{lemma} +\begin{proof} + \leanok + \uses{lem:total-in-dlo} +\end{proof} + +\begin{lemma} + \label{lem:models-of-dlo-models-of-linear-order-theory} + \lean{FirstOrder.Language.Order.model_linearOrderTheory_of_model_dlo} + \leanok + Models of DLO are also models of the theory of linear orders. +\end{lemma} +\begin{proof} + \leanok + \uses{lem:linear-order-theory-in-dlo} +\end{proof} + +%%%% + +%%% + +\section{Instances} +%%% Simple instances and instance chains + +\begin{definition} + \label{def:le-instance-ordered-language} + \lean{FirstOrder.Language.Order.inst_LE_of_IsOrdered} + \leanok + Any structure of an ordered language is an ordered set. +\end{definition} + +\begin{definition} + \label{def:preorder-instance-models-of-dlo} + \lean{FirstOrder.Language.Order.inst_Preorder_of_dlo} + \leanok + \uses{def:le-instance-ordered-language, lem:models-of-dlo-realize-reflexivity, lem:models-of-dlo-realize-transitivity} + statement of your definition +\end{definition} + +\begin{definition} + \label{def:linear-order-instance-models-of-dlo} + \lean{FirstOrder.Language.Order.inst_LinearOrder_of_dlo} + \leanok + \uses{def:preorder-instance-models-of-dlo, lem:models-of-dlo-realize-antisymmetric, lem:models-of-dlo-realize-total} + statement of your definition +\end{definition} + +\begin{definition} + \label{def:binary-relational-language} + \lean{FirstOrder.Language.IsRelational₂} + \leanok + A language is binary relational if it has onyl binary relation symbols. +\end{definition} + +\begin{lemma} + \label{lem:canonical-ordered-language-binary-relational} + \lean{FirstOrder.Language.Order.instIsRelational₂} + \leanok + \uses{def:binary-relational-language} + The canonical ordered language consisting of a single binary relation $\leq$ is a binary relational language. +\end{lemma} +\begin{proof} + \leanok +\end{proof} + +%%% + +\section{Structures} +%%% Equality of structures for relational languages + +\begin{lemma} + \label{lem:structure-funmap-relational-language} + \lean{FirstOrder.Language.Structure.funMap_eq_funMap_of_relational} + \leanok + Structures of a relational language have equal function maps. +\end{lemma} +\begin{proof} + \leanok +\end{proof} + +\begin{lemma} + \label{lem:equality-of-structures-relational-language} + \lean{FirstOrder.Language.Structure.structure_eq_structure_of_relational_iff} + \leanok + Two structures of a relational language are equal if and only if they agree on the + interpretation of all relation symbols. +\end{lemma} +\begin{proof} + \leanok + \uses{lem:structure-funmap-relational-language} +\end{proof} + +%%% + +%%% Equality of structures for binary relational languages + +\begin{lemma} + \label{lem:structure-relmap-binary-relational-language} + \lean{FirstOrder.Language.Structure.RelMap_eq_RelMap_of_relational₂} + \leanok + \uses{def:binary-relational-language} + Two structures of a binary relational language have equal relation maps if and only + if they agree on the interpretation of all binary relation symbols. +\end{lemma} +\begin{proof} + \leanok +\end{proof} + +\begin{lemma} + \label{lem:equality-of-structures-binary-relational-language} + \lean{FirstOrder.Language.Structure.structure_eq_of_structure_of_relational₂_iff} + \leanok + \uses{def:binary-relational-language} + Two structures of a binary relational language are equal if and only if they agree on the + interpretation of all binary relation symbols. +\end{lemma} +\begin{proof} + \leanok + \uses{lem:structure-relmap-binary-relational-language, lem:equality-of-structures-relational-language} +\end{proof} + +\begin{lemma} + \label{lem:orders-coincide-for-ordered-structures} + \lean{FirstOrder.Language.Order.orderStructure_of_LE_of_structure} + \leanok + \uses{def:le-instance-ordered-language} + statement of your lemma +\end{lemma} +\begin{proof} + \leanok + \uses{def:le-instance-ordered-language, + lem:canonical-ordered-language-binary-relational, + lem:equality-of-structures-binary-relational-language, + lem:two-vector-notation} +\end{proof} + +%%% + diff --git a/blueprint/src/chapters/main.tex b/blueprint/src/chapters/main.tex new file mode 100644 index 0000000..d49a292 --- /dev/null +++ b/blueprint/src/chapters/main.tex @@ -0,0 +1,10 @@ + +\begin{theorem} + \label{thm:dlo-aleph0-categorical} + \lean{FirstOrder.Language.Order.aleph0_categorical_of_dlo} + \notready + The theory of dense linear orders without endpoints is $\aleph_0$-categorical. +\end{theorem} +\begin{proof} + \notready +\end{proof} diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index dfb8a0c..523fdd8 100644 --- a/blueprint/src/content.tex +++ b/blueprint/src/content.tex @@ -16,14 +16,15 @@ % \end{theorem} % \begin{proof} -% \leanok +% \leanokcd % \uses{thm:open_ample, lem:open_ample_immersion} % This obviously follows from what we did so far. % \end -\begin{theorem}[Cantor 1874] - \label{thm:aleph0_categorical_of_dlo} - \lean{aleph0_categorical_of_dlo} - \leanok - The theory of dense linear orders without endpoints is $\aleph_0$-categorical. -\end{theorem} \ No newline at end of file +\chapter{Basic Definitions and Lemmas} + +\input{chapters/basics.tex} + +\chapter{Main Results} + +\input{chapters/main.tex} \ No newline at end of file diff --git a/blueprint/src/macros/common.tex b/blueprint/src/macros/common.tex index e71a23a..3403b28 100644 --- a/blueprint/src/macros/common.tex +++ b/blueprint/src/macros/common.tex @@ -9,6 +9,9 @@ \newcommand{\bbr}{\mathbb{R}} \newcommand{\bbc}{\mathbb{C}} +% Define math operator +\DeclareMathOperator{\Fin}{Fin} + % Define theorem-like environments \newtheorem{theorem}{Theorem}[section] \newtheorem{proposition}[theorem]{Proposition} diff --git a/blueprint/src/web.paux b/blueprint/src/web.paux index 5e5ffe2..f154504 100644 Binary files a/blueprint/src/web.paux and b/blueprint/src/web.paux differ diff --git a/blueprint/src/web.tex b/blueprint/src/web.tex index ffa79aa..522ff17 100644 --- a/blueprint/src/web.tex +++ b/blueprint/src/web.tex @@ -18,7 +18,7 @@ \github{https://github.com/metinersin/FormalTextbookModelTheory} \dochome{https://metinersin.github.io/FormalTextbookModelTheory/docs} -\title{My formalization project} +\title{Formal Textbook of Model Theory} \author{Metin Ersin Arıcan} \begin{document} diff --git a/blueprint/web/dep_graph_document.html b/blueprint/web/dep_graph_document.html index 2f9bd77..eade282 100644 --- a/blueprint/web/dep_graph_document.html +++ b/blueprint/web/dep_graph_document.html @@ -61,25 +61,895 @@

Dependencies

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