Documentation

TauCeti.ModelTheory.Infinitary.Theory

Theories of L_{ω₁ω} sentences #

An L_{ω₁ω} theory is a set of L_{ω₁ω} sentences, and a structure is a model of it when it satisfies every member. A countable theory can be replaced by a single sentence: its members, enumerated into the carrier ℕ along IndexCoding.ofEncodableWith, form one countable conjunction, which a structure satisfies exactly when it is a model of the theory. Indices that code no member carry ⊤, so the conjunction of the empty theory holds in every structure.

Theories move along language homomorphisms, sentence by sentence; along an expansion a structure is a model of the image of a theory exactly when it is a model of the theory.

Main definitions #

Main results #

References #

source
@[reducible, inline]
abbrev FirstOrder.Language.Theoryω (L : Language) :
Type (max u v)

An L_{ω₁ω} theory: a set of L_{ω₁ω} sentences.

Instances For
    source
    def FirstOrder.Language.Theoryω.Model {L : Language} (T : L.Theoryω) (M : Type w) [L.Structure M] :
    Prop

    A structure is a model of an L_{ω₁ω} theory when it satisfies every sentence of the theory.

    Instances For
      source
      theorem FirstOrder.Language.Theoryω.model_iff {L : Language} {T : L.Theoryω} {M : Type w} [L.Structure M] :
      T.Model M ↔ ∀ φ ∈ T, SentenceInf.Realize φ M

      Unfolding lemma for Theoryω.Model.

      source
      theorem FirstOrder.Language.Theoryω.Model.realize_of_mem {L : Language} {T : L.Theoryω} {M : Type w} [L.Structure M] (h : T.Model M) {φ : L.Sentenceω} (hφ : φ ∈ T) :
      SentenceInf.Realize φ M

      A model of a theory satisfies each of its sentences.

      source
      theorem FirstOrder.Language.Theoryω.Model.mono {L : Language} {T T' : L.Theoryω} {M : Type w} [L.Structure M] (h : T'.Model M) (hT : T ⊆ T') :
      T.Model M

      A model of a theory is a model of every subtheory.

      source
      @[simp]
      theorem FirstOrder.Language.Theoryω.model_empty {L : Language} {M : Type w} [L.Structure M] :
      ∅.Model M

      Every structure is a model of the empty theory.

      source
      @[simp]
      theorem FirstOrder.Language.Theoryω.model_union_iff {L : Language} {T T' : L.Theoryω} {M : Type w} [L.Structure M] :
      (T ∪ T').Model M ↔ T.Model M ∧ T'.Model M

      A structure is a model of a union exactly when it is a model of both theories.

      source
      @[simp]
      theorem FirstOrder.Language.Theoryω.model_insert_iff {L : Language} {T : L.Theoryω} {M : Type w} [L.Structure M] {φ : L.Sentenceω} :
      (insert φ T).Model M ↔ SentenceInf.Realize φ M ∧ T.Model M

      A structure is a model of insert φ T exactly when it satisfies φ and is a model of T.

      source
      @[simp]
      theorem FirstOrder.Language.Theoryω.model_singleton_iff {L : Language} {M : Type w} [L.Structure M] {φ : L.Sentenceω} :
      {φ}.Model M ↔ SentenceInf.Realize φ M

      A structure is a model of {φ} exactly when it satisfies φ.

      source
      @[simp]
      theorem FirstOrder.Language.Theoryω.model_image_toOmega_iff {L : Language} {M : Type w} [L.Structure M] {T : L.Theory} :
      Model (BoundedFormula.toOmega '' T) M ↔ M ⊨ T

      A structure is a model of the image of a first-order theory in L_{ω₁ω} exactly when it is a model of the first-order theory.

      Sentences of a theory with a model #

      In a model of T, the components of a compound sentence of T that a consistency property adds are true.

      source
      theorem FirstOrder.Language.Theoryω.Model.bot_notMem {L : Language} {T : L.Theoryω} {M : Type w} [L.Structure M] (h : T.Model M) :
      ⊥ ∉ T

      A theory with a model does not contain ⊥.

      source
      theorem FirstOrder.Language.Theoryω.Model.not_notMem {L : Language} {T : L.Theoryω} {M : Type w} [L.Structure M] (h : T.Model M) {φ : L.Sentenceω} (hφ : φ ∈ T) :
      BoundedFormulaInf.not φ ∉ T

      A theory with a model does not contain a sentence together with its negation.

      source
      theorem FirstOrder.Language.Theoryω.Model.realize_of_imp_mem {L : Language} {T : L.Theoryω} {M : Type w} [L.Structure M] (h : T.Model M) {φ ψ : L.Sentenceω} (hφψ : BoundedFormulaInf.imp φ ψ ∈ T) :
      SentenceInf.Realize (BoundedFormulaInf.not φ) M ∨ SentenceInf.Realize ψ M

      In a model of T, an implication in T has a false hypothesis or a true conclusion.

      source
      theorem FirstOrder.Language.Theoryω.Model.realize_of_not_imp_mem {L : Language} {T : L.Theoryω} {M : Type w} [L.Structure M] (h : T.Model M) {φ ψ : L.Sentenceω} (hφψ : (BoundedFormulaInf.imp φ ψ).not ∈ T) :
      SentenceInf.Realize φ M ∧ SentenceInf.Realize (BoundedFormulaInf.not ψ) M

      In a model of T, a negated implication in T has a true hypothesis and a false conclusion.

      source
      theorem FirstOrder.Language.Theoryω.Model.realize_of_not_iInf_mem {L : Language} {T : L.Theoryω} {M : Type w} [L.Structure M] (h : T.Model M) {φs : ℕ → L.Sentenceω} (hφs : (BoundedFormulaInf.iInf φs).not ∈ T) :
      ∃ (k : ℕ), SentenceInf.Realize (BoundedFormulaInf.not (φs k)) M

      In a model of T, a negated conjunction in T has a false conjunct.

      source
      theorem FirstOrder.Language.Theoryω.Model.realize_of_not_iSup_mem {L : Language} {T : L.Theoryω} {M : Type w} [L.Structure M] (h : T.Model M) {φs : ℕ → L.Sentenceω} (hφs : (BoundedFormulaInf.iSup φs).not ∈ T) (k : ℕ) :
      SentenceInf.Realize (BoundedFormulaInf.not (φs k)) M

      In a model of T, every disjunct of a negated disjunction in T is false.

      The conjunction of a countable theory #

      source
      noncomputable def FirstOrder.Language.Theoryω.conjunction {L : Language} (T : L.Theoryω) (hT : Set.Countable T) :
      L.Sentenceω

      The conjunction of a countable theory: its sentences, enumerated into the carrier ℕ along IndexCoding.ofEncodableWith, joined by one countable conjunction. Indices that code no sentence carry ⊤.

      Instances For
        source
        theorem FirstOrder.Language.Theoryω.conjunction_def {L : Language} (T : L.Theoryω) (hT : Set.Countable T) :
        T.conjunction hT = BoundedFormulaInf.iInfAlong (TauCeti.IndexCoding.ofEncodableWith hT.toEncodable) fun (φ : ↑T) => ↑φ

        The conjunction of a countable theory is the coded conjunction of its sentences.

        source
        @[simp]
        theorem FirstOrder.Language.Theoryω.realize_conjunction_iff {L : Language} {T : L.Theoryω} {M : Type w} [L.Structure M] (hT : Set.Countable T) :
        SentenceInf.Realize (T.conjunction hT) M ↔ T.Model M

        A countable theory is one sentence. A structure satisfies the conjunction of a countable theory exactly when it is a model of the theory.

        source
        theorem FirstOrder.Language.Theoryω.model_constantsOn_update_iff {L : Language} {γ : Type uγ} [DecidableEq γ] {M : Type w} [L.Structure M] (e : γ → M) {c : γ} (m : M) {T : (L.withConstants γ).Theoryω} (hc : ∀ φ ∈ T, c ∉ BoundedFormulaInf.constantSupport φ) :
        T.Model M ↔ T.Model M

        Reinterpreting a constant absent from every sentence of a theory preserves modelhood.

        Omitting types #

        source
        def FirstOrder.Language.OmitsType {L : Language} (M : Type w) [L.Structure M] {n : ℕ} (p : Set (L.BoundedFormulaω Empty n)) :
        Prop

        A structure omits a set p of L_{ω₁ω} formulas in n bound variables, a partial type, when no n-tuple of the structure realizes every member of p.

        Instances For
          source
          theorem FirstOrder.Language.omitsType_iff {L : Language} {M : Type w} [L.Structure M] {n : ℕ} {p : Set (L.BoundedFormulaω Empty n)} :
          OmitsType M p ↔ ∀ (a : Fin n → M), ∃ φ ∈ p, ¬BoundedFormulaInf.Realize φ Empty.elim a

          Unfolding lemma for OmitsType.

          source
          theorem FirstOrder.Language.not_omitsType_of_realize {L : Language} {M : Type w} [L.Structure M] {n : ℕ} {p : Set (L.BoundedFormulaω Empty n)} {φ : L.BoundedFormulaω Empty n} (hφ : SentenceInf.Realize (BoundedFormulaInf.exs φ) M) (hp : ∀ ψ ∈ p, SentenceInf.Realize (BoundedFormulaInf.imp φ ψ).alls M) :
          ¬OmitsType M p

          A structure satisfying φ.exs and every sentence (φ.imp ψ).alls with ψ ∈ p does not omit p: a tuple satisfying φ satisfies all of p.

          source
          def FirstOrder.Language.LHom.onTheoryω {L : Language} {L' : Language} (g : L →ᴸ L') (T : L.Theoryω) :
          L'.Theoryω

          The image of an L_{ω₁ω} theory under a language homomorphism: the images of its sentences.

          Instances For
            source
            theorem FirstOrder.Language.LHom.onTheoryω_def {L : Language} {L' : Language} (g : L →ᴸ L') (T : L.Theoryω) :
            g.onTheoryω T = g.onBoundedFormulaInf '' T

            The image of a theory is the image of its sentences.

            source
            @[simp]
            theorem FirstOrder.Language.LHom.mem_onTheoryω {L : Language} {L' : Language} {g : L →ᴸ L'} {T : L.Theoryω} {φ : L'.Sentenceω} :
            φ ∈ g.onTheoryω T ↔ ∃ φ₀ ∈ T, g.onBoundedFormulaInf φ₀ = φ

            Membership in the image of a theory.

            source
            @[simp]
            theorem FirstOrder.Language.LHom.onTheoryω_model {L : Language} {L' : Language} (g : L →ᴸ L') {M : Type w} [L.Structure M] [L'.Structure M] [g.IsExpansionOn M] (T : L.Theoryω) :
            (g.onTheoryω T).Model M ↔ T.Model M

            Modelhood along an expansion. If the L'-structure on M expands its L-structure along g, then M is a model of the image of T exactly when it is a model of T. No injectivity of g and no countability of T is needed. This is the infinitary form of Mathlib's LHom.onTheory_model.

            source
            theorem Set.Countable.onTheoryω {L : FirstOrder.Language} {L' : FirstOrder.Language} {T : L.Theoryω} (hT : Set.Countable T) (g : L →ᴸ L') :
            Set.Countable (g.onTheoryω T)

            The image of a countable theory under a language homomorphism is countable.

            source
            theorem FirstOrder.Language.StrongHomClass.theoryω_model_iff {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {F : Type u_1} [EquivLike F M N] [L.StrongHomClass F M N] (g : F) (T : L.Theoryω) :
            T.Model M ↔ T.Model N

            Isomorphic structures are models of the same L_{ω₁ω} theories.