Documentation

LeanPool.Incompleteness.Foundation.FirstOrder.Basic.Model

Model #

source
structure LO.FirstOrder.Structure.Model (L : Language) (M : Type u_1) :
Type u_1

Imported declaration from the Incompleteness formalization.

  • intro : M

    Imported declaration from the Incompleteness formalization.

Instances For
    source
    def LO.FirstOrder.Structure.Model.equiv (L : Language) (M : Type u_1) :
    M ≃ Model L M

    Imported declaration from the Incompleteness formalization.

    Equations
    Instances For
      source
      @[instance_reducible]
      instance LO.FirstOrder.Structure.Model.inst {L : Language} {M : Type u_2} [Structure L M] :
      Structure L (Model L M)
      Equations
      source
      instance LO.FirstOrder.Structure.Model.instNonempty {L : Language} {M : Type u_1} [h : Nonempty M] :
      Nonempty (Model L M)
      source
      theorem LO.FirstOrder.Structure.Model.elementaryEquiv (L : Language) (M : Type u_1) [Nonempty M] [Structure L M] :
      M ≡ₑ[L] Model L M
      source
      @[instance_reducible]
      instance LO.FirstOrder.Structure.Model.instZeroOfZero {L : Language} {M : Type u_2} [Structure L M] [Semiterm.Operator.Zero L] :
      Zero (Model L M)
      Equations
      source
      instance LO.FirstOrder.Structure.Model.instZero {L : Language} {M : Type u_2} [Structure L M] [Semiterm.Operator.Zero L] :
      Structure.Zero L (Model L M)
      source
      @[instance_reducible]
      instance LO.FirstOrder.Structure.Model.instOneOfOne {L : Language} {M : Type u_2} [Structure L M] [Semiterm.Operator.One L] :
      One (Model L M)
      Equations
      source
      instance LO.FirstOrder.Structure.Model.instOne {L : Language} {M : Type u_2} [Structure L M] [Semiterm.Operator.One L] :
      Structure.One L (Model L M)
      source
      @[instance_reducible]
      instance LO.FirstOrder.Structure.Model.instAddOfAdd {L : Language} {M : Type u_2} [Structure L M] [Semiterm.Operator.Add L] :
      Add (Model L M)
      Equations
      source
      instance LO.FirstOrder.Structure.Model.instAdd {L : Language} {M : Type u_2} [Structure L M] [Semiterm.Operator.Add L] :
      Structure.Add L (Model L M)
      source
      @[instance_reducible]
      instance LO.FirstOrder.Structure.Model.instMulOfMul {L : Language} {M : Type u_2} [Structure L M] [Semiterm.Operator.Mul L] :
      Mul (Model L M)
      Equations
      source
      instance LO.FirstOrder.Structure.Model.instMul {L : Language} {M : Type u_2} [Structure L M] [Semiterm.Operator.Mul L] :
      Structure.Mul L (Model L M)
      source
      @[instance_reducible]
      instance LO.FirstOrder.Structure.Model.instExpOfExp {L : Language} {M : Type u_2} [Structure L M] [Semiterm.Operator.Exp L] :
      Exp (Model L M)
      Equations
      source
      instance LO.FirstOrder.Structure.Model.instExp {L : Language} {M : Type u_2} [Structure L M] [Semiterm.Operator.Exp L] :
      Structure.Exp L (Model L M)
      source
      instance LO.FirstOrder.Structure.Model.instEq {L : Language} {M : Type u_2} [Structure L M] [Semiformula.Operator.Eq L] [Structure.Eq L M] :
      Structure.Eq L (Model L M)
      source
      @[instance_reducible]
      instance LO.FirstOrder.Structure.Model.instLTOfLT {L : Language} {M : Type u_2} [Structure L M] [Semiformula.Operator.LT L] :
      LT (Model L M)
      Equations
      source
      instance LO.FirstOrder.Structure.Model.instLT {L : Language} {M : Type u_2} [Structure L M] [Semiformula.Operator.LT L] :
      Structure.LT L (Model L M)
      source
      @[instance_reducible]
      instance LO.FirstOrder.Structure.Model.instMembershipOfMem {L : Language} {M : Type u_2} [Structure L M] [Semiformula.Operator.Mem L] :
      Membership (Model L M) (Model L M)
      Equations
      source
      instance LO.FirstOrder.Structure.Model.instMem {L : Language} {M : Type u_2} [Structure L M] [Semiformula.Operator.Mem L] :
      Mem L (Model L M)
      source
      @[reducible]
      def LO.FirstOrder.Structure.ofFunc (F : ℕ → Type u_1) {M : Type u_2} (fF : {k : ℕ} → F k → (Fin k → M) → M) :
      Structure (Language.ofFunc F) M

      Imported declaration from the Incompleteness formalization.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem LO.FirstOrder.Structure.func_ofFunc (F : ℕ → Type u_1) {M : Type u_2} (fF : {k : ℕ} → F k → (Fin k → M) → M) {k : ℕ} (f : F k) (v : Fin k → M) :
        func f v = fF f v
        source
        @[instance_reducible]
        instance LO.FirstOrder.Structure.add (L₁ : Language) (L₂ : Language) (M : Type u_1) [str₁ : Structure L₁ M] [str₂ : Structure L₂ M] :
        Structure (L₁.add L₂) M
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[simp]
        theorem LO.FirstOrder.Structure.func_sigma_inl {L₁ : Language} {L₂ : Language} {M : Type u_1} [str₁ : Structure L₁ M] [str₂ : Structure L₂ M] {k : ℕ} (f : L₁.Func k) (v : Fin k → M) :
        func (Sum.inl f) v = func f v
        source
        @[simp]
        theorem LO.FirstOrder.Structure.func_sigma_inr {L₁ : Language} {L₂ : Language} {M : Type u_1} [str₁ : Structure L₁ M] [str₂ : Structure L₂ M] {k : ℕ} (f : L₂.Func k) (v : Fin k → M) :
        func (Sum.inr f) v = func f v
        source
        @[simp]
        theorem LO.FirstOrder.Structure.rel_sigma_inl {L₁ : Language} {L₂ : Language} {M : Type u_1} [str₁ : Structure L₁ M] [str₂ : Structure L₂ M] {k : ℕ} (r : L₁.Rel k) (v : Fin k → M) :
        rel (Sum.inl r) v ↔ rel r v
        source
        @[simp]
        theorem LO.FirstOrder.Structure.rel_sigma_inr {L₁ : Language} {L₂ : Language} {M : Type u_1} [str₁ : Structure L₁ M] [str₂ : Structure L₂ M] {k : ℕ} (r : L₂.Rel k) (v : Fin k → M) :
        rel (Sum.inr r) v ↔ rel r v
        source
        @[simp]
        theorem LO.FirstOrder.Structure.val_lMap_add₁ {L₁ : Language} {L₂ : Language} {M : Type u_1} [str₁ : Structure L₁ M] [str₂ : Structure L₂ M] {μ : Type u_2} {n : ℕ} (t : Semiterm L₁ μ n) (e : Fin n → M) (ε : μ → M) :
        Semiterm.val (add L₁ L₂ M) e ε (Semiterm.lMap (Language.Hom.add₁ L₁ L₂) t) = Semiterm.val str₁ e ε t
        source
        @[simp]
        theorem LO.FirstOrder.Structure.val_lMap_add₂ {L₁ : Language} {L₂ : Language} {M : Type u_1} [str₁ : Structure L₁ M] [str₂ : Structure L₂ M] {μ : Type u_2} {n : ℕ} (t : Semiterm L₂ μ n) (e : Fin n → M) (ε : μ → M) :
        Semiterm.val (add L₁ L₂ M) e ε (Semiterm.lMap (Language.Hom.add₂ L₁ L₂) t) = Semiterm.val str₂ e ε t
        source
        @[simp]
        theorem LO.FirstOrder.Structure.eval_lMap_add₁ {L₁ : Language} {L₂ : Language} {M : Type u_1} [str₁ : Structure L₁ M] [str₂ : Structure L₂ M] {μ : Type u_2} {n : ℕ} (φ : Semiformula L₁ μ n) (e : Fin n → M) (ε : μ → M) :
        (Semiformula.Eval (add L₁ L₂ M) e ε) ((Semiformula.lMap (Language.Hom.add₁ L₁ L₂)) φ) ↔ (Semiformula.Eval str₁ e ε) φ
        source
        @[simp]
        theorem LO.FirstOrder.Structure.eval_lMap_add₂ {L₁ : Language} {L₂ : Language} {M : Type u_1} [str₁ : Structure L₁ M] [str₂ : Structure L₂ M] {μ : Type u_2} {n : ℕ} (φ : Semiformula L₂ μ n) (e : Fin n → M) (ε : μ → M) :
        (Semiformula.Eval (add L₁ L₂ M) e ε) ((Semiformula.lMap (Language.Hom.add₂ L₁ L₂)) φ) ↔ (Semiformula.Eval str₂ e ε) φ
        source
        @[instance_reducible]
        instance LO.FirstOrder.Structure.sigma {ι : Type u_2} (L : ι → Language) (M : Type u_1) [str : (i : ι) → Structure (L i) M] :
        Structure (Language.sigma L) M
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[simp]
        theorem LO.FirstOrder.Structure.func_sigma {ι : Type u_3} (L : ι → Language) (M : Type u_1) [str : (i : ι) → Structure (L i) M] {i : ι} {k : ℕ} (f : (L i).Func k) (v : Fin k → M) :
        func ⟨i, f⟩ v = func f v
        source
        @[simp]
        theorem LO.FirstOrder.Structure.rel_sigma {ι : Type u_3} (L : ι → Language) (M : Type u_1) [str : (i : ι) → Structure (L i) M] {i : ι} {k : ℕ} (r : (L i).Rel k) (v : Fin k → M) :
        rel ⟨i, r⟩ v ↔ rel r v
        source
        @[simp]
        theorem LO.FirstOrder.Structure.val_lMap_sigma {ι : Type u_4} (L : ι → Language) (M : Type u_1) [str : (i : ι) → Structure (L i) M] {i : ι} {μ : Type u_2} {n : ℕ} (t : Semiterm (L i) μ n) (e : Fin n → M) (ε : μ → M) :
        Semiterm.val (sigma L M) e ε (Semiterm.lMap (Language.Hom.sigma L i) t) = Semiterm.val (str i) e ε t
        source
        @[simp]
        theorem LO.FirstOrder.Structure.eval_lMap_sigma {ι : Type u_4} (L : ι → Language) (M : Type u_1) [str : (i : ι) → Structure (L i) M] {i : ι} {μ : Type u_2} {n : ℕ} (φ : Semiformula (L i) μ n) (e : Fin n → M) (ε : μ → M) :
        (Semiformula.Eval (sigma L M) e ε) ((Semiformula.lMap (Language.Hom.sigma L i)) φ) ↔ (Semiformula.Eval (str i) e ε) φ
        source
        @[instance_reducible]
        instance LO.FirstOrder.instStructureULift {L : Language} {M : Type v} [Structure L M] :
        Structure L (ULift.{v', v} M)
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[simp]
        theorem LO.FirstOrder.Structure.func_uLift {L : Language} {M : Type v} [Structure L M] {k : ℕ} (f : L.Func k) (v : Fin k → ULift.{v', v} M) :
        func f v = { down := func f fun (i : Fin k) => (v i).down }
        source
        @[simp]
        theorem LO.FirstOrder.Structure.rel_uLift {L : Language} {M : Type v} [Structure L M] {k : ℕ} (r : L.Rel k) (v : Fin k → ULift.{v', v} M) :
        rel r v = rel r fun (i : Fin k) => (v i).down
        source
        theorem LO.FirstOrder.Semiterm.valm_uLift {L : Language} {M : Type v} [Structure L M] {n : ℕ} {ξ : Type u_1} {e : Fin n → ULift.{v', v} M} {ε : ξ → ULift.{v', v} M} {t : Semiterm L ξ n} :
        valm (ULift.{v', v} M) e ε t = { down := valm M (fun (i : Fin n) => (e i).down) (fun (i : ξ) => (ε i).down) t }
        source
        theorem LO.FirstOrder.Semiformula.evalm_uLift {L : Language} {M : Type v} [Structure L M] {n : ℕ} {ξ : Type u_1} {e : Fin n → ULift.{v', v} M} {ε : ξ → ULift.{v', v} M} {φ : Semiformula L ξ n} :
        (Evalm (ULift.{v', v} M) e ε) φ ↔ (Evalm M (fun (i : Fin n) => (e i).down) fun (i : ξ) => (ε i).down) φ
        source
        theorem LO.FirstOrder.uLift_elementaryEquiv (L : Language) (M : Type v) [Structure L M] [Nonempty M] :
        ULift.{v', v} M ≡ₑ[L] M