Language of first-order logic #
This file defines the language of first-order Foundation.
LO.FirstOrder.Language.empty
is the empty language.LO.FirstOrder.Language.constant C
is a language with only constants of the elementC
.LO.FirstOrder.Language.oRing
,ℒₒᵣ
is the language of ordered ring.
Instances
theorem
LO.FirstOrder.Language.IsRelational.func_empty
{L : LO.FirstOrder.Language}
[self : L.IsRelational]
(k : ℕ)
:
class
LO.FirstOrder.Language.IsConstant
(L : LO.FirstOrder.Language)
extends
LO.FirstOrder.Language.IsRelational
:
Instances
theorem
LO.FirstOrder.Language.IsConstant.rel_empty
{L : LO.FirstOrder.Language}
[self : L.IsConstant]
(k : ℕ)
:
IsEmpty (L.Rel k)
class
LO.FirstOrder.Language.ConstantInhabited
(L : LO.FirstOrder.Language)
extends
Inhabited
:
Type u_1
Instances
instance
LO.FirstOrder.Language.instInhabitedFuncOfNatNatOfConstantInhabited
{L : LO.FirstOrder.Language}
[L.ConstantInhabited]
:
Inhabited (L.Func 0)
Equations
- LO.FirstOrder.Language.instInhabitedFuncOfNatNatOfConstantInhabited = inferInstance
Equations
- LO.FirstOrder.Language.empty = { Func := fun (x : ℕ) => PEmpty.{u_1 + 1} , Rel := fun (x : ℕ) => PEmpty.{u_1 + 1} }
Instances For
Equations
- LO.FirstOrder.Language.instInhabited = { default := LO.FirstOrder.Language.empty }
- start: LO.FirstOrder.Language.GraphFunc 0
- terminal: LO.FirstOrder.Language.GraphFunc 0
Instances For
Instances For
Equations
- LO.FirstOrder.Language.graph = { Func := LO.FirstOrder.Language.GraphFunc, Rel := LO.FirstOrder.Language.GraphRel }
Instances For
- isone: LO.FirstOrder.Language.BinaryRel 1
- equal: LO.FirstOrder.Language.BinaryRel 2
- le: LO.FirstOrder.Language.BinaryRel 2
Instances For
Equations
- LO.FirstOrder.Language.binary = { Func := fun (x : ℕ) => Empty, Rel := LO.FirstOrder.Language.BinaryRel }
Instances For
- equal: LO.FirstOrder.Language.EqRel 2
Instances For
@[reducible]
Equations
- LO.FirstOrder.Language.equal = { Func := fun (x : ℕ) => Empty, Rel := LO.FirstOrder.Language.EqRel }
Instances For
instance
LO.FirstOrder.Language.instToStringFuncEqual
(k : ℕ)
:
ToString (LO.FirstOrder.Language.equal.Func k)
Equations
- LO.FirstOrder.Language.instToStringFuncEqual k = { toString := fun (x : LO.FirstOrder.Language.equal.Func k) => "" }
instance
LO.FirstOrder.Language.instToStringRelEqual
(k : ℕ)
:
ToString (LO.FirstOrder.Language.equal.Rel k)
Equations
- LO.FirstOrder.Language.instToStringRelEqual k = { toString := fun (x : LO.FirstOrder.Language.equal.Rel k) => "\\mathrm{Eq}" }
instance
LO.FirstOrder.Language.instDecidableEqFuncEqual
(k : ℕ)
:
DecidableEq (LO.FirstOrder.Language.equal.Func k)
Equations
- LO.FirstOrder.Language.instDecidableEqFuncEqual k a b = Empty.casesOn (fun (x : LO.FirstOrder.Language.equal.Func k) => Decidable (x = b)) a
Equations
- One or more equations did not get rendered due to their size.
instance
LO.FirstOrder.Language.instEncodableFuncEqual
(k : ℕ)
:
Encodable (LO.FirstOrder.Language.equal.Func k)
Equations
- LO.FirstOrder.Language.instEncodableFuncEqual k = IsEmpty.toEncodable
Equations
- One or more equations did not get rendered due to their size.
- zero: LO.FirstOrder.Language.ORing.Func 0
- one: LO.FirstOrder.Language.ORing.Func 0
- add: LO.FirstOrder.Language.ORing.Func 2
- mul: LO.FirstOrder.Language.ORing.Func 2
Instances For
Instances For
@[reducible]
Equations
- ℒₒᵣ = { Func := LO.FirstOrder.Language.ORing.Func, Rel := LO.FirstOrder.Language.ORing.Rel }
Instances For
Equations
- LO.FirstOrder.Language.termℒₒᵣ = Lean.ParserDescr.node `LO.FirstOrder.Language.termℒₒᵣ 1024 (Lean.ParserDescr.symbol "ℒₒᵣ")
Instances For
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.
- zero: LO.FirstOrder.Language.ORingExp.Func 0
- one: LO.FirstOrder.Language.ORingExp.Func 0
- exp: LO.FirstOrder.Language.ORingExp.Func 1
- add: LO.FirstOrder.Language.ORingExp.Func 2
- mul: LO.FirstOrder.Language.ORingExp.Func 2
Instances For
Instances For
@[reducible]
Equations
- ℒₒᵣ(exp) = { Func := LO.FirstOrder.Language.ORingExp.Func, Rel := LO.FirstOrder.Language.ORingExp.Rel }
Instances For
Equations
- LO.FirstOrder.Language.«termℒₒᵣ(exp)» = Lean.ParserDescr.node `LO.FirstOrder.Language.termℒₒᵣ(exp) 1024 (Lean.ParserDescr.symbol "ℒₒᵣ(exp)")
Instances For
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.
instance
LO.FirstOrder.Language.ORingExp.instDecidableEqFuncORingExp
(k : ℕ)
:
DecidableEq (ℒₒᵣ(exp).Func k)
Equations
- One or more equations did not get rendered due to their size.
instance
LO.FirstOrder.Language.ORingExp.instDecidableEqRelORingExp
(k : ℕ)
:
DecidableEq (ℒₒᵣ(exp).Rel k)
Equations
- One or more equations did not get rendered due to their size.
- const: {C : Type u_1} → C → LO.FirstOrder.Language.Constant.Func C 0
Instances For
Equations
- LO.FirstOrder.Language.constant C = { Func := LO.FirstOrder.Language.Constant.Func C, Rel := fun (x : ℕ) => PEmpty.{u_1 + 1} }
Instances For
instance
LO.FirstOrder.Language.instCoeFuncConstantOfNatNat
(C : Type u_1)
:
Coe C ((LO.FirstOrder.Language.constant C).Func 0)
Equations
- LO.FirstOrder.Language.instCoeFuncConstantOfNatNat C = { coe := LO.FirstOrder.Language.Constant.Func.const }
instance
LO.FirstOrder.Language.instIsConstantConstant
(C : Type u_1)
:
(LO.FirstOrder.Language.constant C).IsConstant
@[reducible, inline]
Instances For
Equations
- LO.FirstOrder.Language.ofFunc F = { Func := F, Rel := fun (x : ℕ) => PEmpty.{v + 1} }
Instances For
Equations
Instances For
Equations
Equations
- LO.FirstOrder.Language.sigma L = { Func := fun (k : ℕ) => (i : ι) × (L i).Func k, Rel := fun (k : ℕ) => (i : ι) × (L i).Rel k }
Instances For
- 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
- LO.FirstOrder.Language.instORingORing = LO.FirstOrder.Language.ORing.mk
Equations
- LO.FirstOrder.Language.instConstantInhabitedORing = LO.FirstOrder.Language.ConstantInhabited.mk
Equations
- LO.FirstOrder.Language.instORingORingExp = LO.FirstOrder.Language.ORing.mk
Equations
Equations
instance
LO.FirstOrder.Language.instStarAdd
(L : LO.FirstOrder.Language)
(S : LO.FirstOrder.Language)
[S.Star]
:
(L.add S).Star
instance
LO.FirstOrder.Language.instZeroAdd
(L : LO.FirstOrder.Language)
(S : LO.FirstOrder.Language)
[L.Zero]
:
(L.add S).Zero
instance
LO.FirstOrder.Language.instOneAdd
(L : LO.FirstOrder.Language)
(S : LO.FirstOrder.Language)
[L.One]
:
(L.add S).One
instance
LO.FirstOrder.Language.instAddAdd
(L : LO.FirstOrder.Language)
(S : LO.FirstOrder.Language)
[L.Add]
:
(L.add S).Add
instance
LO.FirstOrder.Language.instMulAdd
(L : LO.FirstOrder.Language)
(S : LO.FirstOrder.Language)
[L.Mul]
:
(L.add S).Mul
instance
LO.FirstOrder.Language.instEqAdd
(L : LO.FirstOrder.Language)
(S : LO.FirstOrder.Language)
[L.Eq]
:
(L.add S).Eq
instance
LO.FirstOrder.Language.instLTAdd
(L : LO.FirstOrder.Language)
(S : LO.FirstOrder.Language)
[L.LT]
:
(L.add S).LT
theorem
LO.FirstOrder.Language.Hom.ext_iff
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
(x : L₁.Hom L₂)
(y : L₁.Hom L₂)
:
x = y ↔ @LO.FirstOrder.Language.Hom.func L₁ L₂ x = @LO.FirstOrder.Language.Hom.func L₁ L₂ y ∧ @LO.FirstOrder.Language.Hom.rel L₁ L₂ x = @LO.FirstOrder.Language.Hom.rel L₁ L₂ y
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
structure
LO.FirstOrder.Language.Hom
(L₁ : LO.FirstOrder.Language)
(L₂ : LO.FirstOrder.Language)
:
Type (max u_1 u_2)
Instances For
Equations
- LO.FirstOrder.«term_→ᵥ_» = Lean.ParserDescr.trailingNode `LO.FirstOrder.term_→ᵥ_ 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ᵥ ") (Lean.ParserDescr.cat `term 26))
Instances For
Equations
- LO.FirstOrder.Language.Hom.id L = { func := fun {k : ℕ} => id, rel := fun {k : ℕ} => id }
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₃
Instances For
def
LO.FirstOrder.Language.Hom.add₁
(L₁ : LO.FirstOrder.Language)
(L₂ : LO.FirstOrder.Language)
:
L₁.Hom (L₁.add L₂)
Equations
- LO.FirstOrder.Language.Hom.add₁ L₁ L₂ = { func := fun {k : ℕ} => Sum.inl, rel := fun {k : ℕ} => Sum.inl }
Instances For
def
LO.FirstOrder.Language.Hom.add₂
(L₁ : LO.FirstOrder.Language)
(L₂ : LO.FirstOrder.Language)
:
L₂.Hom (L₁.add L₂)
Equations
- LO.FirstOrder.Language.Hom.add₂ L₁ L₂ = { func := fun {k : ℕ} => Sum.inr, rel := fun {k : ℕ} => Sum.inr }
Instances For
theorem
LO.FirstOrder.Language.Hom.func_add₁
{k : ℕ}
(L₁ : LO.FirstOrder.Language)
(L₂ : LO.FirstOrder.Language)
(f : L₁.Func k)
:
(LO.FirstOrder.Language.Hom.add₁ L₁ L₂).func f = Sum.inl f
theorem
LO.FirstOrder.Language.Hom.rel_add₁
{k : ℕ}
(L₁ : LO.FirstOrder.Language)
(L₂ : LO.FirstOrder.Language)
(r : L₁.Rel k)
:
(LO.FirstOrder.Language.Hom.add₁ L₁ L₂).rel r = Sum.inl r
theorem
LO.FirstOrder.Language.Hom.func_add₂
{k : ℕ}
(L₁ : LO.FirstOrder.Language)
(L₂ : LO.FirstOrder.Language)
(f : L₂.Func k)
:
(LO.FirstOrder.Language.Hom.add₂ L₁ L₂).func f = Sum.inr f
theorem
LO.FirstOrder.Language.Hom.rel_add₂
{k : ℕ}
(L₁ : LO.FirstOrder.Language)
(L₂ : LO.FirstOrder.Language)
(r : L₂.Rel k)
:
(LO.FirstOrder.Language.Hom.add₂ L₁ L₂).rel r = Sum.inr r
@[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
def
LO.FirstOrder.Language.Hom.sigma
{ι : Type u_1}
(L : ι → LO.FirstOrder.Language)
(i : ι)
:
(L i).Hom (LO.FirstOrder.Language.sigma L)
Equations
- LO.FirstOrder.Language.Hom.sigma L i = { func := fun {k : ℕ} (f : (L i).Func k) => ⟨i, f⟩, rel := fun {k : ℕ} (r : (L i).Rel k) => ⟨i, r⟩ }
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.