Documentation

Mathlib.ModelTheory.Basic

Basics on First-Order Structures #

This file defines first-order languages and structures in the style of the Flypitch project, as well as several important maps between structures.

Main Definitions #

References #

For the Flypitch project:

Languages and Structures #

structure FirstOrder.Language :
Type (max (u + 1) (v + 1))
  • Functions : Type u

    For every arity, a Type* of functions of that arity

  • Relations : Type v

    For every arity, a Type* of relations of that arity

A first-order language consists of a type of functions of every natural-number arity and a type of relations of every natural-number arity.

Instances For
    def FirstOrder.Sequence₂ (a₀ : Type u) (a₁ : Type u) (a₂ : Type u) :
    Type u

    Used to define FirstOrder.Language₂.

    Instances For
      instance FirstOrder.Sequence₂.inhabited₀ (a₀ : Type u) (a₁ : Type u) (a₂ : Type u) [h : Inhabited a₀] :
      instance FirstOrder.Sequence₂.inhabited₁ (a₀ : Type u) (a₁ : Type u) (a₂ : Type u) [h : Inhabited a₁] :
      instance FirstOrder.Sequence₂.inhabited₂ (a₀ : Type u) (a₁ : Type u) (a₂ : Type u) [h : Inhabited a₂] :
      @[simp]
      theorem FirstOrder.Sequence₂.sum_card (a₀ : Type u) (a₁ : Type u) (a₂ : Type u) :
      @[simp]
      theorem FirstOrder.Language.mk₂_Relations (c : Type u) (f₁ : Type u) (f₂ : Type u) (r₁ : Type v) (r₂ : Type v) :
      @[simp]
      theorem FirstOrder.Language.mk₂_Functions (c : Type u) (f₁ : Type u) (f₂ : Type u) (r₁ : Type v) (r₂ : Type v) :
      ∀ (a : ), FirstOrder.Language.Functions (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂) a = FirstOrder.Sequence₂ c f₁ f₂ a
      def FirstOrder.Language.mk₂ (c : Type u) (f₁ : Type u) (f₂ : Type u) (r₁ : Type v) (r₂ : Type v) :

      A constructor for languages with only constants, unary and binary functions, and unary and binary relations.

      Instances For

        The empty language has no symbols.

        Instances For

          The sum of two languages consists of the disjoint union of their symbols.

          Instances For

            The type of constants in a given language.

            Instances For
              @[simp]
              theorem FirstOrder.Language.constants_mk₂ (c : Type u) (f₁ : Type u) (f₂ : Type u) (r₁ : Type v) (r₂ : Type v) :

              The type of symbols in a given language.

              Instances For

                The cardinality of a language is the cardinality of its type of symbols.

                Instances For

                  A language is relational when it has no function symbols.

                  Instances

                    A language is algebraic when it has no relation symbols.

                    Instances
                      instance FirstOrder.Language.isRelational_of_empty_functions {symb : Type u_1} :
                      FirstOrder.Language.IsRelational { Functions := fun x => Empty, Relations := symb }
                      instance FirstOrder.Language.isAlgebraic_of_empty_relations {symb : Type u_1} :
                      FirstOrder.Language.IsAlgebraic { Functions := symb, Relations := fun x => Empty }
                      instance FirstOrder.Language.isRelational_mk₂ {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} [h0 : IsEmpty c] [h1 : IsEmpty f₁] [h2 : IsEmpty f₂] :
                      instance FirstOrder.Language.isAlgebraic_mk₂ {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} [h1 : IsEmpty r₁] [h2 : IsEmpty r₂] :
                      instance FirstOrder.Language.subsingleton_mk₂_functions {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} [h0 : Subsingleton c] [h1 : Subsingleton f₁] [h2 : Subsingleton f₂] {n : } :
                      instance FirstOrder.Language.subsingleton_mk₂_relations {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} [h1 : Subsingleton r₁] [h2 : Subsingleton r₂] {n : } :
                      class FirstOrder.Language.Structure (L : FirstOrder.Language) (M : Type w) :
                      Type (max (max u v) w)

                      A first-order structure on a type M consists of interpretations of all the symbols in a given language. Each function of arity n is interpreted as a function sending tuples of length n (modeled as (Fin n → M)) to M, and a relation of arity n is a function from tuples of length n to Prop.

                      Instances

                        Used for defining FirstOrder.Language.Theory.ModelType.instInhabited.

                        Instances For

                          Maps #

                          A homomorphism between first-order structures is a function that commutes with the interpretations of functions and maps tuples in one structure where a given relation is true to tuples in the second structure where that relation is still true.

                          Instances For

                            A homomorphism between first-order structures is a function that commutes with the interpretations of functions and maps tuples in one structure where a given relation is true to tuples in the second structure where that relation is still true.

                            Instances For

                              An embedding of first-order structures is an embedding that commutes with the interpretations of functions and relations.

                              Instances For

                                An embedding of first-order structures is an embedding that commutes with the interpretations of functions and relations.

                                Instances For

                                  An equivalence of first-order structures is an equivalence that commutes with the interpretations of functions and relations.

                                  Instances For

                                    An equivalence of first-order structures is an equivalence that commutes with the interpretations of functions and relations.

                                    Instances For

                                      Interpretation of a constant symbol

                                      Instances For

                                        Given a language with a nonempty type of constants, any structure will be nonempty. This cannot be a global instance, because L becomes a metavariable.

                                        def FirstOrder.Language.funMap₂ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} (c' : cM) (f₁' : f₁MM) (f₂' : f₂MMM) {n : } :
                                        FirstOrder.Language.Functions (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂) n(Fin nM) → M

                                        The function map for FirstOrder.Language.Structure₂.

                                        Instances For
                                          def FirstOrder.Language.RelMap₂ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} (r₁' : r₁Set M) (r₂' : r₂MMProp) {n : } :
                                          FirstOrder.Language.Relations (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂) n(Fin nM) → Prop

                                          The relation map for FirstOrder.Language.Structure₂.

                                          Instances For
                                            def FirstOrder.Language.Structure.mk₂ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} (c' : cM) (f₁' : f₁MM) (f₂' : f₂MMM) (r₁' : r₁Set M) (r₂' : r₂MMProp) :

                                            A structure constructor to match FirstOrder.Language₂.

                                            Instances For
                                              @[simp]
                                              theorem FirstOrder.Language.Structure.funMap_apply₀ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} {c' : cM} {f₁' : f₁MM} {f₂' : f₂MMM} {r₁' : r₁Set M} {r₂' : r₂MMProp} (c₀ : c) {x : Fin 0M} :
                                              @[simp]
                                              theorem FirstOrder.Language.Structure.funMap_apply₁ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} {c' : cM} {f₁' : f₁MM} {f₂' : f₂MMM} {r₁' : r₁Set M} {r₂' : r₂MMProp} (f : f₁) (x : M) :
                                              @[simp]
                                              theorem FirstOrder.Language.Structure.funMap_apply₂ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} {c' : cM} {f₁' : f₁MM} {f₂' : f₂MMM} {r₁' : r₁Set M} {r₂' : r₂MMProp} (f : f₂) (x : M) (y : M) :
                                              @[simp]
                                              theorem FirstOrder.Language.Structure.relMap_apply₁ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} {c' : cM} {f₁' : f₁MM} {f₂' : f₂MMM} {r₁' : r₁Set M} {r₂' : r₂MMProp} (r : r₁) (x : M) :
                                              @[simp]
                                              theorem FirstOrder.Language.Structure.relMap_apply₂ {M : Type w} {c : Type u} {f₁ : Type u} {f₂ : Type u} {r₁ : Type v} {r₂ : Type v} {c' : cM} {f₁' : f₁MM} {f₂' : f₂MMM} {r₁' : r₁Set M} {r₂' : r₂MMProp} (r : r₂) (x : M) (y : M) :

                                              HomClass L F M N states that F is a type of L-homomorphisms. You should extend this typeclass when you extend FirstOrder.Language.Hom.

                                              Instances

                                                StrongHomClass L F M N states that F is a type of L-homomorphisms which preserve relations in both directions.

                                                Instances
                                                  theorem FirstOrder.Language.Hom.ext {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] ⦃f : FirstOrder.Language.Hom L M N ⦃g : FirstOrder.Language.Hom L M N (h : ∀ (x : M), f x = g x) :
                                                  f = g

                                                  The identity map from a structure to itself.

                                                  Instances For

                                                    Composition of first-order homomorphisms.

                                                    Instances For

                                                      Any element of a HomClass can be realized as a first_order homomorphism.

                                                      Instances For

                                                        A first-order embedding is also a first-order homomorphism.

                                                        Instances For

                                                          In an algebraic language, any injective homomorphism is an embedding.

                                                          Instances For

                                                            The identity embedding from a structure to itself.

                                                            Instances For

                                                              Any element of an injective StrongHomClass can be realized as a first_order embedding.

                                                              Instances For

                                                                The inverse of a first-order equivalence is a first-order equivalence.

                                                                Instances For

                                                                  A first-order equivalence is also a first-order embedding.

                                                                  Instances For

                                                                    A first-order equivalence is also a first-order homomorphism.

                                                                    Instances For
                                                                      theorem FirstOrder.Language.Equiv.ext {L : FirstOrder.Language} {M : Type w} {N : Type w'} [FirstOrder.Language.Structure L M] [FirstOrder.Language.Structure L N] ⦃f : FirstOrder.Language.Equiv L M N ⦃g : FirstOrder.Language.Equiv L M N (h : ∀ (x : M), f x = g x) :
                                                                      f = g

                                                                      The identity equivalence from a structure to itself.

                                                                      Instances For

                                                                        Composition of first-order equivalences.

                                                                        Instances For

                                                                          Any element of a bijective StrongHomClass can be realized as a first_order isomorphism.

                                                                          Instances For
                                                                            @[simp]
                                                                            theorem Function.emptyHom_toFun {M : Type w} {N : Type w'} (f : MN) :
                                                                            ∀ (a : M), ↑(Function.emptyHom f) a = f a

                                                                            Makes a Language.empty.Hom out of any function.

                                                                            Instances For

                                                                              Makes a Language.empty.Embedding out of any function.

                                                                              Instances For
                                                                                @[simp]
                                                                                theorem FirstOrder.Language.toFun_embedding_empty {M : Type w} {N : Type w'} (f : M N) :
                                                                                ↑(Embedding.empty f) = f
                                                                                @[simp]
                                                                                theorem FirstOrder.Language.toEmbedding_embedding_empty {M : Type w} {N : Type w'} (f : M N) :
                                                                                (Embedding.empty f).toEmbedding = f

                                                                                Makes a Language.empty.Equiv out of any function.

                                                                                Instances For
                                                                                  @[simp]
                                                                                  theorem FirstOrder.Language.toFun_equiv_empty {M : Type w} {N : Type w'} (f : M N) :
                                                                                  ↑(Equiv.empty f) = f
                                                                                  @[simp]
                                                                                  theorem FirstOrder.Language.toEquiv_equiv_empty {M : Type w} {N : Type w'} (f : M N) :
                                                                                  (Equiv.empty f).toEquiv = f

                                                                                  A structure induced by a bijection.

                                                                                  Instances For

                                                                                    A bijection as a first-order isomorphism with the induced structure on the codomain.

                                                                                    Instances For