Documentation

Foundation.FirstOrder.Basic.Syntax.Language

Language of first-order logic #

This file defines the language of first-order Foundation.

structure LO.FirstOrder.Language :
Type (u + 1)
Instances For
    Instances
      theorem LO.FirstOrder.Language.IsRelational.func_empty {L : LO.FirstOrder.Language} [self : L.IsRelational] (k : ) :
      IsEmpty (L.Func (k + 1))
      Instances
        theorem LO.FirstOrder.Language.IsConstant.rel_empty {L : LO.FirstOrder.Language} [self : L.IsConstant] (k : ) :
        IsEmpty (L.Rel k)
        Equations
        • LO.FirstOrder.Language.instInhabitedFuncOfNatNatOfConstantInhabited = inferInstance
        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.
        Equations
        • =
        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
        Instances For
          Equations
          Equations
          Instances For
            Equations
            • L₁.add L₂ = { Func := fun (k : ) => L₁.Func k L₂.Func k, Rel := fun (k : ) => L₁.Rel k L₂.Rel k }
            Instances For
              Equations
              Instances For
                • eq : L.Rel 2
                Instances
                  • lt : L.Rel 2
                  Instances
                    • zero : L.Func 0
                    Instances
                      • one : L.Func 0
                      Instances
                        • add : L.Func 2
                        Instances
                          • mul : L.Func 2
                          Instances
                            • pow : L.Func 2
                            Instances
                              • exp : L.Func 1
                              Instances
                                • pair : L.Func 2
                                Instances
                                  • star : L.Func 0
                                  Instances
                                    Equations
                                    Equations
                                    • L.instStarAdd S = { star := Sum.inr LO.FirstOrder.Language.Star.star }
                                    Equations
                                    • L.instZeroAdd S = { zero := Sum.inl LO.FirstOrder.Language.Zero.zero }
                                    Equations
                                    • L.instOneAdd S = { one := Sum.inl LO.FirstOrder.Language.One.one }
                                    Equations
                                    • L.instAddAdd S = { add := Sum.inl LO.FirstOrder.Language.Add.add }
                                    Equations
                                    • L.instMulAdd S = { mul := Sum.inl LO.FirstOrder.Language.Mul.mul }
                                    Equations
                                    • L.instEqAdd S = { eq := Sum.inl LO.FirstOrder.Language.Eq.eq }
                                    Equations
                                    • L.instLTAdd S = { lt := Sum.inl LO.FirstOrder.Language.LT.lt }
                                    theorem LO.FirstOrder.Language.Hom.ext {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} (x : L₁.Hom L₂) (y : L₁.Hom L₂) (func : @LO.FirstOrder.Language.Hom.func L₁ L₂ x = @LO.FirstOrder.Language.Hom.func L₁ L₂ y) (rel : @LO.FirstOrder.Language.Hom.rel L₁ L₂ x = @LO.FirstOrder.Language.Hom.rel L₁ L₂ y) :
                                    x = y
                                    • func : {k : } → L₁.Func kL₂.Func k
                                    • rel : {k : } → L₁.Rel kL₂.Rel k
                                    Instances For
                                      Equations
                                      Instances For
                                        def LO.FirstOrder.Language.Hom.comp {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {L₃ : LO.FirstOrder.Language} (Ψ : L₂.Hom L₃) (Φ : L₁.Hom L₂) :
                                        L₁.Hom L₃
                                        Equations
                                        • Ψ.comp Φ = { func := fun {k : } => Ψ.func Φ.func, rel := fun {k : } => Ψ.rel Φ.rel }
                                        Instances For
                                          Equations
                                          Instances For
                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem LO.FirstOrder.Language.Hom.add₂_star (L₁ : LO.FirstOrder.Language) (L₂ : LO.FirstOrder.Language) [L₂.Star] :
                                              (LO.FirstOrder.Language.Hom.add₂ L₁ L₂).func LO.FirstOrder.Language.Star.star = LO.FirstOrder.Language.Star.star
                                              @[simp]
                                              theorem LO.FirstOrder.Language.Hom.add₁_zero (L₁ : LO.FirstOrder.Language) (L₂ : LO.FirstOrder.Language) [L₁.Zero] :
                                              (LO.FirstOrder.Language.Hom.add₁ L₁ L₂).func LO.FirstOrder.Language.Zero.zero = LO.FirstOrder.Language.Zero.zero
                                              @[simp]
                                              theorem LO.FirstOrder.Language.Hom.add₁_one (L₁ : LO.FirstOrder.Language) (L₂ : LO.FirstOrder.Language) [L₁.One] :
                                              (LO.FirstOrder.Language.Hom.add₁ L₁ L₂).func LO.FirstOrder.Language.One.one = LO.FirstOrder.Language.One.one
                                              @[simp]
                                              theorem LO.FirstOrder.Language.Hom.add₁_add (L₁ : LO.FirstOrder.Language) (L₂ : LO.FirstOrder.Language) [L₁.Add] :
                                              (LO.FirstOrder.Language.Hom.add₁ L₁ L₂).func LO.FirstOrder.Language.Add.add = LO.FirstOrder.Language.Add.add
                                              @[simp]
                                              theorem LO.FirstOrder.Language.Hom.add₁_mul (L₁ : LO.FirstOrder.Language) (L₂ : LO.FirstOrder.Language) [L₁.Mul] :
                                              (LO.FirstOrder.Language.Hom.add₁ L₁ L₂).func LO.FirstOrder.Language.Mul.mul = LO.FirstOrder.Language.Mul.mul
                                              @[simp]
                                              theorem LO.FirstOrder.Language.Hom.add₁_eq (L₁ : LO.FirstOrder.Language) (L₂ : LO.FirstOrder.Language) [L₁.Eq] :
                                              (LO.FirstOrder.Language.Hom.add₁ L₁ L₂).rel LO.FirstOrder.Language.Eq.eq = LO.FirstOrder.Language.Eq.eq
                                              @[simp]
                                              theorem LO.FirstOrder.Language.Hom.add₁_lt (L₁ : LO.FirstOrder.Language) (L₂ : LO.FirstOrder.Language) [L₁.LT] :
                                              (LO.FirstOrder.Language.Hom.add₁ L₁ L₂).rel LO.FirstOrder.Language.LT.lt = LO.FirstOrder.Language.LT.lt
                                              Equations
                                              Instances For
                                                theorem LO.FirstOrder.Language.Hom.func_sigma {ι : Type u_1} {k : } (L : ιLO.FirstOrder.Language) (i : ι) (f : (L i).Func k) :
                                                (LO.FirstOrder.Language.Hom.sigma L i).func f = i, f
                                                theorem LO.FirstOrder.Language.Hom.rel_sigma {ι : Type u_1} {k : } (L : ιLO.FirstOrder.Language) (i : ι) (r : (L i).Rel k) :
                                                (LO.FirstOrder.Language.Hom.sigma L i).rel r = i, r
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For