diff --git a/Mathlib/ModelTheory/Basic.lean b/Mathlib/ModelTheory/Basic.lean index 90615f08fbf38a..3b118ac0d7aa99 100644 --- a/Mathlib/ModelTheory/Basic.lean +++ b/Mathlib/ModelTheory/Basic.lean @@ -29,16 +29,10 @@ structures. * A `FirstOrder.Language.Embedding`, denoted `M ↪[L] N`, is an embedding from the `L`-structure `M` to the `L`-structure `N` that commutes with the interpretations of functions, and which preserves the interpretations of relations in both directions. -* A `FirstOrder.Language.ElementaryEmbedding`, denoted `M ↪ₑ[L] N`, is an embedding from the - `L`-structure `M` to the `L`-structure `N` that commutes with the realizations of all formulas. * A `FirstOrder.Language.Equiv`, denoted `M ≃[L] N`, is an equivalence from the `L`-structure `M` to the `L`-structure `N` that commutes with the interpretations of functions, and which preserves the interpretations of relations in both directions. -## TODO - -Use `[Countable L.symbols]` instead of `[L.countable]`. - ## References For the Flypitch project: - [J. Han, F. van Doorn, *A formal proof of the independence of the continuum hypothesis*] @@ -980,12 +974,12 @@ instance (priority := 100) strongHomClassEmpty {F M N} [FunLike F M fun _ => N] ⟨fun _ _ f => Empty.elim f, fun _ _ r => Empty.elim r⟩ #align first_order.language.strong_hom_class_empty FirstOrder.Language.strongHomClassEmpty -/-- Makes a `Language.empty.hom` out of any function. -/ +/-- Makes a `Language.empty.Hom` out of any function. -/ @[simps] def _root_.Function.emptyHom (f : M → N) : M →[Language.empty] N where toFun := f #align function.empty_hom Function.emptyHom -/-- Makes a `Language.empty.embedding` out of any function. -/ +/-- Makes a `Language.empty.Embedding` out of any function. -/ --@[simps] Porting note: commented out and lemmas added manually def _root_.Embedding.empty (f : M ↪ N) : M ↪[Language.empty] N where toEmbedding := f #align embedding.empty Embedding.empty @@ -998,7 +992,7 @@ theorem toFun_embedding_empty (f : M ↪ N) : (Embedding.empty f : M → N) = f theorem toEmbedding_embedding_empty (f : M ↪ N) : (Embedding.empty f).toEmbedding = f := rfl -/-- Makes a `Language.empty.equiv` out of any function. -/ +/-- Makes a `Language.empty.Equiv` out of any function. -/ --@[simps] Porting note: commented out and lemmas added manually def _root_.Equiv.empty (f : M ≃ N) : M ≃[Language.empty] N where toEquiv := f #align equiv.empty Equiv.empty diff --git a/Mathlib/ModelTheory/Bundled.lean b/Mathlib/ModelTheory/Bundled.lean index bafc1778fa975c..1aa42b659e78d1 100644 --- a/Mathlib/ModelTheory/Bundled.lean +++ b/Mathlib/ModelTheory/Bundled.lean @@ -16,8 +16,8 @@ import Mathlib.CategoryTheory.ConcreteCategory.Bundled This file bundles types together with their first-order structure. ## Main Definitions -* `FirstOrder.language.Theory.ModelType` is the type of nonempty models of a particular theory. -* `FirstOrder.language.equivSetoid` is the isomorphism equivalence relation on bundled structures. +* `FirstOrder.Language.Theory.ModelType` is the type of nonempty models of a particular theory. +* `FirstOrder.Language.equivSetoid` is the isomorphism equivalence relation on bundled structures. ## TODO * Define category structures on bundled structures and models. diff --git a/Mathlib/ModelTheory/ElementaryMaps.lean b/Mathlib/ModelTheory/ElementaryMaps.lean index c70ac17b12bdb7..4902aa5cbc243e 100644 --- a/Mathlib/ModelTheory/ElementaryMaps.lean +++ b/Mathlib/ModelTheory/ElementaryMaps.lean @@ -415,7 +415,7 @@ theorem isElementary (S : L.ElementarySubstructure M) : (S : L.Substructure M).I S.is_elementary' #align first_order.language.elementary_substructure.is_elementary FirstOrder.Language.ElementarySubstructure.isElementary -/-- The natural embedding of an `L.substructure` of `M` into `M`. -/ +/-- The natural embedding of an `L.Substructure` of `M` into `M`. -/ def subtype (S : L.ElementarySubstructure M) : S ↪ₑ[L] M where toFun := (↑) map_formula' := S.isElementary diff --git a/Mathlib/ModelTheory/FinitelyGenerated.lean b/Mathlib/ModelTheory/FinitelyGenerated.lean index 37dc8afb2f9eae..081a7f05240858 100644 --- a/Mathlib/ModelTheory/FinitelyGenerated.lean +++ b/Mathlib/ModelTheory/FinitelyGenerated.lean @@ -16,10 +16,10 @@ This file defines what it means for a first-order (sub)structure to be finitely generated, similarly to other finitely-generated objects in the algebra library. ## Main Definitions -* `first_order.language.substructure.FG` indicates that a substructure is finitely generated. -* `first_order.language.Structure.FG` indicates that a structure is finitely generated. -* `first_order.language.substructure.CG` indicates that a substructure is countably generated. -* `first_order.language.Structure.CG` indicates that a structure is countably generated. +* `FirstOrder.Language.Substructure.FG` indicates that a substructure is finitely generated. +* `FirstOrder.Language.Structure.FG` indicates that a structure is finitely generated. +* `FirstOrder.Language.Substructure.CG` indicates that a substructure is countably generated. +* `FirstOrder.Language.Structure.CG` indicates that a structure is countably generated. ## TODO @@ -212,7 +212,7 @@ theorem fg_def : FG L M ↔ (⊤ : L.Substructure M).FG := ⟨fun h => h.1, fun h => ⟨h⟩⟩ #align first_order.language.Structure.fg_def FirstOrder.Language.Structure.fg_def -/-- An equivalent expression of `Structure.fg` in terms of `set.finite` instead of `finset`. -/ +/-- An equivalent expression of `Structure.fg` in terms of `Set.Finite` instead of `Finset`. -/ theorem fg_iff : FG L M ↔ ∃ S : Set M, S.Finite ∧ closure L S = (⊤ : L.Substructure M) := by rw [fg_def, Substructure.fg_def] #align first_order.language.Structure.fg_iff FirstOrder.Language.Structure.fg_iff diff --git a/Mathlib/ModelTheory/LanguageMap.lean b/Mathlib/ModelTheory/LanguageMap.lean index 7968f8ab498b16..21bb1761cc1144 100644 --- a/Mathlib/ModelTheory/LanguageMap.lean +++ b/Mathlib/ModelTheory/LanguageMap.lean @@ -55,6 +55,7 @@ structure LHom where #align first_order.language.Lhom FirstOrder.Language.LHom -- mathport name: «expr →ᴸ » +@[inherit_doc FirstOrder.Language.LHom] infixl:10 " →ᴸ " => LHom -- \^L @@ -453,6 +454,7 @@ def withConstants : Language.{max u w', v} := #align first_order.language.with_constants FirstOrder.Language.withConstants -- mathport name: language.with_constants +@[inherit_doc FirstOrder.Language.withConstants] scoped[FirstOrder] notation:95 L "[[" α "]]" => Language.withConstants L α @[simp] diff --git a/Mathlib/ModelTheory/Order.lean b/Mathlib/ModelTheory/Order.lean index 06f48cc2f72888..c09f437829f3b1 100644 --- a/Mathlib/ModelTheory/Order.lean +++ b/Mathlib/ModelTheory/Order.lean @@ -28,7 +28,7 @@ particularly useful example in model theory. ## Main Results * `PartialOrder`s model the theory of partial orders, `LinearOrder`s model the theory of -linear orders, and dense linear orders without endpoints model `Theory.DLO`. +linear orders, and dense linear orders without endpoints model `Language.dlo`. -/ diff --git a/Mathlib/ModelTheory/Semantics.lean b/Mathlib/ModelTheory/Semantics.lean index 019501b3c0a320..1062818b4833ba 100644 --- a/Mathlib/ModelTheory/Semantics.lean +++ b/Mathlib/ModelTheory/Semantics.lean @@ -19,27 +19,27 @@ in a style inspired by the [Flypitch project](https://flypitch.github.io/). ## Main Definitions * `FirstOrder.Language.Term.realize` is defined so that `t.realize v` is the term `t` evaluated at variables `v`. -* `FirstOrder.Language.BoundedFormula.Realize` is defined so that `φ.realize v xs` is the bounded +* `FirstOrder.Language.BoundedFormula.Realize` is defined so that `φ.Realize v xs` is the bounded formula `φ` evaluated at tuples of variables `v` and `xs`. -* `FirstOrder.Language.Formula.Realize` is defined so that `φ.realize v` is the formula `φ` +* `FirstOrder.Language.Formula.Realize` is defined so that `φ.Realize v` is the formula `φ` evaluated at variables `v`. -* `FirstOrder.Language.Sentence.Realize` is defined so that `φ.realize M` is the sentence `φ` +* `FirstOrder.Language.Sentence.Realize` is defined so that `φ.Realize M` is the sentence `φ` evaluated in the structure `M`. Also denoted `M ⊨ φ`. -* `FirstOrder.Language.Theory.Model` is defined so that `T.model M` is true if and only if every +* `FirstOrder.Language.Theory.Model` is defined so that `T.Model M` is true if and only if every sentence of `T` is realized in `M`. Also denoted `T ⊨ φ`. ## Main Results * `FirstOrder.Language.BoundedFormula.realize_toPrenex` shows that the prenex normal form of a formula has the same realization as the original formula. -* Several results in this file show that syntactic constructions such as `relabel`, `castLe`, -`lift_at`, `subst`, and the actions of language maps commute with realization of terms, formulas, +* Several results in this file show that syntactic constructions such as `relabel`, `castLE`, +`liftAt`, `subst`, and the actions of language maps commute with realization of terms, formulas, sentences, and theories. ## Implementation Notes -* Formulas use a modified version of de Bruijn variables. Specifically, a `L.boundedFormula α n` +* Formulas use a modified version of de Bruijn variables. Specifically, a `L.BoundedFormula α n` is a formula with some variables indexed by a type `α`, which cannot be quantified over, and some -indexed by `Fin n`, which can. For any `φ : L.boundedFormula α (n + 1)`, we define the formula -`∀' φ : L.boundedFormula α n` by universally quantifying over the variable indexed by +indexed by `Fin n`, which can. For any `φ : L.BoundedFormula α (n + 1)`, we define the formula +`∀' φ : L.BoundedFormula α n` by universally quantifying over the variable indexed by `n : Fin (n + 1)`. ## References diff --git a/Mathlib/ModelTheory/Substructures.lean b/Mathlib/ModelTheory/Substructures.lean index 919d9a8c68b610..f669c9abbae2ac 100644 --- a/Mathlib/ModelTheory/Substructures.lean +++ b/Mathlib/ModelTheory/Substructures.lean @@ -26,7 +26,7 @@ the least substructure of `M` containing `s`. substructure `s` under the homomorphism `f`, as a substructure. * `FirstOrder.Language.Substructure.map` is defined so that `s.map f` is the image of the substructure `s` under the homomorphism `f`, as a substructure. -* `FirstOrder.Language.Hom.range` is defined so that `f.map` is the range of the +* `FirstOrder.Language.Hom.range` is defined so that `f.range` is the range of the the homomorphism `f`, as a substructure. * `FirstOrder.Language.Hom.domRestrict` and `FirstOrder.Language.Hom.codRestrict` restrict the domain and codomain respectively of first-order homomorphisms to substructures. @@ -663,7 +663,7 @@ instance inducedStructure {S : L.Substructure M} : L.Structure S where set_option linter.uppercaseLean3 false in #align first_order.language.substructure.induced_Structure FirstOrder.Language.Substructure.inducedStructure -/-- The natural embedding of an `L.substructure` of `M` into `M`. -/ +/-- The natural embedding of an `L.Substructure` of `M` into `M`. -/ def subtype (S : L.Substructure M) : S ↪[L] M where toFun := (↑) inj' := Subtype.coe_injective diff --git a/Mathlib/ModelTheory/Syntax.lean b/Mathlib/ModelTheory/Syntax.lean index 23371b8bb55698..c5adddcaa29fc8 100644 --- a/Mathlib/ModelTheory/Syntax.lean +++ b/Mathlib/ModelTheory/Syntax.lean @@ -21,7 +21,7 @@ This file defines first-order terms, formulas, sentences, and theories in a styl ## Main Definitions * A `FirstOrder.Language.Term` is defined so that `L.Term α` is the type of `L`-terms with free variables indexed by `α`. -* A `FirstOrder.Language.Formula` is defined so that `L.formula α` is the type of `L`-formulas with +* A `FirstOrder.Language.Formula` is defined so that `L.Formula α` is the type of `L`-formulas with free variables indexed by `α`. * A `FirstOrder.Language.Sentence` is a formula with no free variables. * A `FirstOrder.Language.Theory` is a set of sentences. @@ -41,10 +41,10 @@ variables with given terms. constants in the language and having extra variables indexed by the same type. ## Implementation Notes -* Formulas use a modified version of de Bruijn variables. Specifically, a `L.boundedFormula α n` +* Formulas use a modified version of de Bruijn variables. Specifically, a `L.BoundedFormula α n` is a formula with some variables indexed by a type `α`, which cannot be quantified over, and some -indexed by `Fin n`, which can. For any `φ : L.boundedFormula α (n + 1)`, we define the formula -`∀' φ : L.boundedFormula α n` by universally quantifying over the variable indexed by +indexed by `Fin n`, which can. For any `φ : L.BoundedFormula α (n + 1)`, we define the formula +`∀' φ : L.BoundedFormula α n` by universally quantifying over the variable indexed by `n : Fin (n + 1)`. ## References @@ -792,7 +792,7 @@ theorem IsPrenex.liftAt {k m : ℕ} (h : IsPrenex φ) : (φ.liftAt k m).IsPrenex --Porting note: universes in different order /-- An auxiliary operation to `FirstOrder.Language.BoundedFormula.toPrenex`. - If `φ` is quantifier-free and `ψ` is in prenex normal form, then `φ.to_prenex_imp_right ψ` + If `φ` is quantifier-free and `ψ` is in prenex normal form, then `φ.toPrenexImpRight ψ` is a prenex normal form for `φ.imp ψ`. -/ def toPrenexImpRight : ∀ {n}, L.BoundedFormula α n → L.BoundedFormula α n → L.BoundedFormula α n | n, φ, BoundedFormula.ex ψ => ((φ.liftAt 1 n).toPrenexImpRight ψ).ex @@ -822,7 +822,7 @@ theorem isPrenex_toPrenexImpRight {φ ψ : L.BoundedFormula α n} (hφ : IsQF φ --Porting note: universes in different order /-- An auxiliary operation to `FirstOrder.Language.BoundedFormula.toPrenex`. - If `φ` and `ψ` are in prenex normal form, then `φ.to_prenex_imp ψ` + If `φ` and `ψ` are in prenex normal form, then `φ.toPrenexImp ψ` is a prenex normal form for `φ.imp ψ`. -/ def toPrenexImp : ∀ {n}, L.BoundedFormula α n → L.BoundedFormula α n → L.BoundedFormula α n | n, BoundedFormula.ex φ, ψ => (φ.toPrenexImp (ψ.liftAt 1 n)).all