Documentation

Foundation.Logic.Predicate.Language

Language of first-order logic #

This file defines the language of first-order logic.

Instances
    class LO.FirstOrder.Language.IsConstant (L : Language) extends L.IsRelational :
    Instances
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    inductive LO.FirstOrder.Language.Constant.Func (C : Type u_1) :
    Type u_1
    Equations
    def LO.FirstOrder.Language.sigma {ι : Type u_1} (L : ιLanguage) :
    Equations
    Instances For
    • pow : L.Func 2
    Instances
      • exp : L.Func 1
      Instances
        • pair : L.Func 2
        Instances
          class LO.FirstOrder.Language.ORing (L : Language) extends L.Eq, L.LT, L.Zero, L.One, L.Add, L.Mul :
          Type u_1
          Instances
          instance LO.FirstOrder.Language.instStarAdd (L : Language) (S : Language) [S.Star] :
          (L.add S).Star
          Equations
          instance LO.FirstOrder.Language.instZeroAdd (L : Language) (S : Language) [L.Zero] :
          (L.add S).Zero
          Equations
          instance LO.FirstOrder.Language.instOneAdd (L : Language) (S : Language) [L.One] :
          (L.add S).One
          Equations
          instance LO.FirstOrder.Language.instAddAdd (L : Language) (S : Language) [L.Add] :
          (L.add S).Add
          Equations
          instance LO.FirstOrder.Language.instMulAdd (L : Language) (S : Language) [L.Mul] :
          (L.add S).Mul
          Equations
          instance LO.FirstOrder.Language.instEqAdd (L : Language) (S : Language) [L.Eq] :
          (L.add S).Eq
          Equations
          instance LO.FirstOrder.Language.instLTAdd (L : Language) (S : Language) [L.LT] :
          (L.add S).LT
          Equations
          structure LO.FirstOrder.Language.Hom (L₁ : Language) (L₂ : Language) :
          Type (max u_1 u_2)
          • func {k : } : L₁.Func kL₂.Func k
          • rel {k : } : L₁.Rel kL₂.Rel k
          theorem LO.FirstOrder.Language.Hom.ext {L₁ : Language} {L₂ : Language} {x y : L₁.Hom L₂} (func : @func L₁ L₂ x = @func L₁ L₂ y) (rel : @rel L₁ L₂ x = @rel L₁ L₂ y) :
          x = y
          Equations
          def LO.FirstOrder.Language.Hom.comp {L₁ : Language} {L₂ : Language} {L₃ : Language} (Ψ : L₂.Hom L₃) (Φ : L₁.Hom L₂) :
          L₁.Hom L₃
          Equations
          • Ψ.comp Φ = { func := fun {k : } => Ψ.func Φ.func, rel := fun {k : } => Ψ.rel Φ.rel }
          def LO.FirstOrder.Language.Hom.add₁ (L₁ : Language) (L₂ : Language) :
          L₁.Hom (L₁.add L₂)
          Equations
          def LO.FirstOrder.Language.Hom.add₂ (L₁ : Language) (L₂ : Language) :
          L₂.Hom (L₁.add L₂)
          Equations
          theorem LO.FirstOrder.Language.Hom.func_add₁ {k : } (L₁ : Language) (L₂ : Language) (f : L₁.Func k) :
          (add₁ L₁ L₂).func f = Sum.inl f
          theorem LO.FirstOrder.Language.Hom.rel_add₁ {k : } (L₁ : Language) (L₂ : Language) (r : L₁.Rel k) :
          (add₁ L₁ L₂).rel r = Sum.inl r
          theorem LO.FirstOrder.Language.Hom.func_add₂ {k : } (L₁ : Language) (L₂ : Language) (f : L₂.Func k) :
          (add₂ L₁ L₂).func f = Sum.inr f
          theorem LO.FirstOrder.Language.Hom.rel_add₂ {k : } (L₁ : Language) (L₂ : Language) (r : L₂.Rel k) :
          (add₂ L₁ L₂).rel r = Sum.inr r
          @[simp]
          theorem LO.FirstOrder.Language.Hom.add₂_star (L₁ : Language) (L₂ : Language) [L₂.Star] :
          (add₂ L₁ L₂).func Star.star = Star.star
          @[simp]
          theorem LO.FirstOrder.Language.Hom.add₁_zero (L₁ : Language) (L₂ : Language) [L₁.Zero] :
          (add₁ L₁ L₂).func Zero.zero = Zero.zero
          @[simp]
          theorem LO.FirstOrder.Language.Hom.add₁_one (L₁ : Language) (L₂ : Language) [L₁.One] :
          (add₁ L₁ L₂).func One.one = One.one
          @[simp]
          theorem LO.FirstOrder.Language.Hom.add₁_add (L₁ : Language) (L₂ : Language) [L₁.Add] :
          (add₁ L₁ L₂).func Add.add = Add.add
          @[simp]
          theorem LO.FirstOrder.Language.Hom.add₁_mul (L₁ : Language) (L₂ : Language) [L₁.Mul] :
          (add₁ L₁ L₂).func Mul.mul = Mul.mul
          @[simp]
          theorem LO.FirstOrder.Language.Hom.add₁_eq (L₁ : Language) (L₂ : Language) [L₁.Eq] :
          (add₁ L₁ L₂).rel Eq.eq = Eq.eq
          @[simp]
          theorem LO.FirstOrder.Language.Hom.add₁_lt (L₁ : Language) (L₂ : Language) [L₁.LT] :
          (add₁ L₁ L₂).rel LT.lt = LT.lt
          def LO.FirstOrder.Language.Hom.sigma {ι : Type u_1} (L : ιLanguage) (i : ι) :
          (L i).Hom (Language.sigma L)
          Equations
          theorem LO.FirstOrder.Language.Hom.func_sigma {ι : Type u_1} {k : } (L : ιLanguage) (i : ι) (f : (L i).Func k) :
          (sigma L i).func f = i, f
          theorem LO.FirstOrder.Language.Hom.rel_sigma {ι : Type u_1} {k : } (L : ιLanguage) (i : ι) (r : (L i).Rel k) :
          (sigma L i).rel r = i, r
          Equations
          • One or more equations did not get rendered due to their size.
          instance LO.FirstOrder.instDecidableEqOfFuncOfDecidableEqRel (L : Language) [(k : ) → DecidableEq (L.Func k)] [(k : ) → DecidableEq (L.Rel k)] :
          L.DecidableEq
          Equations