Documentation

InfinitaryLogic.Lomega1omega.Embedding

Embeddings between Lω₁ω and L∞ω #

This file defines embeddings between Lω₁ω (countable infinitary logic) and L∞ω (arbitrary infinitary logic).

Main Definitions #

Main Results #

source
def FirstOrder.Language.BoundedFormulaω.toLinf {L : Language} {α : Type u'} {n : ℕ} :
L.BoundedFormulaω α n → L.BoundedFormulaInf α n

Embeds a Lω₁ω formula into L∞ω (uses ℕ as index type).

Equations
Instances For
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaω.realize_toLinf {L : Language} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {v : α → M} {xs : Fin n → M} (φ : L.BoundedFormulaω α n) :
    φ.toLinf.Realize v xs ↔ φ.Realize v xs
    source
    theorem FirstOrder.Language.BoundedFormulaω.toLinf_isCountable {L : Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormulaω α n) :
    φ.toLinf.IsCountable

    toLinf preserves the countable property.

    source
    def FirstOrder.Language.Formulaω.toLinf {L : Language} {α : Type u'} (φ : L.Formulaω α) :
    L.FormulaInf α

    Embeds a Lω₁ω formula into L∞ω.

    Equations
    Instances For
      source
      @[simp]
      theorem FirstOrder.Language.Formulaω.realize_toLinf {L : Language} {α : Type u'} {M : Type w} [L.Structure M] {v : α → M} (φ : L.Formulaω α) :
      φ.toLinf.Realize v ↔ φ.Realize v
      source
      def FirstOrder.Language.Sentenceω.toLinf {L : Language} (φ : L.Sentenceω) :
      L.SentenceInf

      Embeds a Lω₁ω sentence into L∞ω.

      Equations
      Instances For
        source
        @[simp]
        theorem FirstOrder.Language.Sentenceω.realize_toLinf {L : Language} {M : Type w} [L.Structure M] (φ : L.Sentenceω) :
        φ.toLinf.Realize M ↔ φ.Realize M
        source
        theorem FirstOrder.Language.BoundedFormulaInf.IsCountable.imp_left {L : Language} {α : Type u'} {n : ℕ} {φ ψ : L.BoundedFormulaInf α n} (h : (φ.imp ψ).IsCountable) :
        φ.IsCountable

        Extract the IsCountable proofs from an imp proof.

        source
        theorem FirstOrder.Language.BoundedFormulaInf.IsCountable.imp_right {L : Language} {α : Type u'} {n : ℕ} {φ ψ : L.BoundedFormulaInf α n} (h : (φ.imp ψ).IsCountable) :
        ψ.IsCountable

        Extract the IsCountable proofs from an imp proof.

        source
        theorem FirstOrder.Language.BoundedFormulaInf.IsCountable.all_inner {L : Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormulaInf α (n + 1)} (h : φ.all.IsCountable) :
        φ.IsCountable

        Extract the IsCountable proof from an all proof.

        source
        theorem FirstOrder.Language.BoundedFormulaInf.IsCountable.iSup_countable {L : Language} {α : Type u'} {n : ℕ} {ι : Type} {φs : ι → L.BoundedFormulaInf α n} (h : (BoundedFormulaInf.iSup φs).IsCountable) :
        Countable ι

        Extract Countable instance from an iSup IsCountable proof.

        source
        theorem FirstOrder.Language.BoundedFormulaInf.IsCountable.iSup_forall {L : Language} {α : Type u'} {n : ℕ} {ι : Type} {φs : ι → L.BoundedFormulaInf α n} (h : (BoundedFormulaInf.iSup φs).IsCountable) (i : ι) :
        (φs i).IsCountable

        Extract the IsCountable proofs from an iSup proof.

        source
        theorem FirstOrder.Language.BoundedFormulaInf.IsCountable.iInf_countable {L : Language} {α : Type u'} {n : ℕ} {ι : Type} {φs : ι → L.BoundedFormulaInf α n} (h : (BoundedFormulaInf.iInf φs).IsCountable) :
        Countable ι

        Extract Countable instance from an iInf IsCountable proof.

        source
        theorem FirstOrder.Language.BoundedFormulaInf.IsCountable.iInf_forall {L : Language} {α : Type u'} {n : ℕ} {ι : Type} {φs : ι → L.BoundedFormulaInf α n} (h : (BoundedFormulaInf.iInf φs).IsCountable) (i : ι) :
        (φs i).IsCountable

        Extract the IsCountable proofs from an iInf proof.

        source
        noncomputable def FirstOrder.Language.BoundedFormulaInf.ofCountable {L : Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormulaInf α n} :
        φ.IsCountable → L.BoundedFormulaω α n

        Converts a countable L∞ω formula back to Lω₁ω. Recurses on the IsCountable proof to extract Countable instances at iSup/iInf nodes.

        Equations
        Instances For
          source
          @[simp]
          theorem FirstOrder.Language.BoundedFormulaInf.realize_ofCountable {L : Language} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {v : α → M} {xs : Fin n → M} {φ : L.BoundedFormulaInf α n} (h : φ.IsCountable) :
          (ofCountable h).Realize v xs ↔ φ.Realize v xs

          Semantics is preserved by ofCountable conversion.

          source
          theorem FirstOrder.Language.BoundedFormulaInf.realize_ofCountable_irrel {L : Language} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {φ : L.BoundedFormulaInf α n} (h₁ h₂ : φ.IsCountable) (v : α → M) (xs : Fin n → M) :
          (ofCountable h₁).Realize v xs ↔ (ofCountable h₂).Realize v xs

          Encoding independence: different IsCountable proofs for the same formula yield semantically equivalent Lω₁ω formulas. The ofCountable function uses Encodable.ofCountable (a choice function) at each iSup/iInf node, so different proofs may produce syntactically different formulas, but their realizations agree.

          source
          noncomputable def FirstOrder.Language.FormulaInf.ofCountable {L : Language} {α : Type u'} {φ : L.FormulaInf α} (h : BoundedFormulaInf.IsCountable φ) :
          L.Formulaω α

          Converts a countable L∞ω formula to Lω₁ω.

          Equations
          Instances For
            source
            @[simp]
            theorem FirstOrder.Language.FormulaInf.realize_ofCountable {L : Language} {α : Type u'} {M : Type w} [L.Structure M] {v : α → M} {φ : L.FormulaInf α} (h : BoundedFormulaInf.IsCountable φ) :
            (ofCountable h).Realize v ↔ φ.Realize v
            source
            noncomputable def FirstOrder.Language.SentenceInf.ofCountable {L : Language} {φ : L.SentenceInf} (h : BoundedFormulaInf.IsCountable φ) :
            L.Sentenceω

            Converts a countable L∞ω sentence to Lω₁ω.

            Equations
            Instances For
              source
              @[simp]
              theorem FirstOrder.Language.SentenceInf.realize_ofCountable {L : Language} {M : Type w} [L.Structure M] {φ : L.SentenceInf} (h : BoundedFormulaInf.IsCountable φ) :
              (ofCountable h).Realize M ↔ φ.Realize M
              source
              theorem FirstOrder.Language.SentenceInf.realize_ofCountable_irrel {L : Language} {φ : L.SentenceInf} (h₁ h₂ : BoundedFormulaInf.IsCountable φ) (M : Type w) [L.Structure M] :
              (ofCountable h₁).Realize M ↔ (ofCountable h₂).Realize M

              Encoding independence at the sentence level.