Language of first-order logic

This file defines the language of first-order logic.

• FFL.FirstOrder.Language.empty is the empty language.
• FFL.FirstOrder.Language.constant C is a language with only constants of the element C.
• FFL.FirstOrder.Language.oRing, ℒₒᵣ is the language of ordered ring.

structure FFL.FirstOrder.Language : Type (u + 1)

• Func : ℕ → Type u
• Rel : ℕ → Type u

class FFL.FirstOrder.Language.Relational (L : Language) : Prop

• func_empty (k : ℕ) : IsEmpty (L.Func k)

instance FFL.FirstOrder.Language.instIsEmptyFuncOfRelational {k : ℕ} {L : Language} [L.Relational] : IsEmpty (L.Func k)

class FFL.FirstOrder.Language.IsConstant (L : Language) : Prop

• func_empty (k : ℕ) : IsEmpty (L.Func (k + 1))
• rel_empty (k : ℕ) : IsEmpty (L.Rel k)

class FFL.FirstOrder.Language.ConstantInhabited (L : Language) extends Inhabited (L.Func 0) : Type u_1

• default : L.Func 0

@[instance_reducible]

instance FFL.FirstOrder.Language.instInhabitedFuncOfNatNatOfConstantInhabited {L : Language} [L.ConstantInhabited] : Inhabited (L.Func 0)

Equations

• FFL.FirstOrder.Language.instInhabitedFuncOfNatNatOfConstantInhabited = inferInstance

def FFL.FirstOrder.Language.empty : Language

Equations

• FFL.FirstOrder.Language.empty = { Func := fun (x : ℕ) => PEmpty.{?u.1 + 1}, Rel := fun (x : ℕ) => PEmpty.{?u.1 + 1} }

@[instance_reducible]

instance FFL.FirstOrder.Language.instInhabited : Inhabited Language

Equations

• FFL.FirstOrder.Language.instInhabited = { default := FFL.FirstOrder.Language.empty }

inductive FFL.FirstOrder.Language.GraphFunc : ℕ → Type

• start : GraphFunc 0
• terminal : GraphFunc 0

inductive FFL.FirstOrder.Language.GraphRel : ℕ → Type

• equal : GraphRel 2
• le : GraphRel 2

def FFL.FirstOrder.Language.graph : Language

Equations

• FFL.FirstOrder.Language.graph = { Func := FFL.FirstOrder.Language.GraphFunc, Rel := FFL.FirstOrder.Language.GraphRel }

inductive FFL.FirstOrder.Language.BinaryRel : ℕ → Type

• isone : BinaryRel 1
• equal : BinaryRel 2
• le : BinaryRel 2

def FFL.FirstOrder.Language.binary : Language

Equations

• FFL.FirstOrder.Language.binary = { Func := fun (x : ℕ) => Empty, Rel := FFL.FirstOrder.Language.BinaryRel }

inductive FFL.FirstOrder.Language.EqRel : ℕ → Type

• equal : EqRel 2

@[reducible]

def FFL.FirstOrder.Language.equal : Language

Equations

• FFL.FirstOrder.Language.equal = { Func := fun (x : ℕ) => Empty, Rel := FFL.FirstOrder.Language.EqRel }

@[instance_reducible]

instance FFL.FirstOrder.Language.instToStringFuncEqual (k : ℕ) : ToString (equal.Func k)

Equations

• FFL.FirstOrder.Language.instToStringFuncEqual k = { toString := fun (x : FFL.FirstOrder.Language.equal.Func k) => "" }

@[instance_reducible]

instance FFL.FirstOrder.Language.instToStringRelEqual (k : ℕ) : ToString (equal.Rel k)

Equations

• FFL.FirstOrder.Language.instToStringRelEqual k = { toString := fun (x : FFL.FirstOrder.Language.equal.Rel k) => "\\mathrm{Eq}" }

@[instance_reducible]

instance FFL.FirstOrder.Language.instDecidableEqFuncEqual (k : ℕ) : DecidableEq (equal.Func k)

Equations

• FFL.FirstOrder.Language.instDecidableEqFuncEqual k a b = Empty.casesOn (fun (x : FFL.FirstOrder.Language.equal.Func k) => Decidable (x = b)) a

@[instance_reducible]

instance FFL.FirstOrder.Language.instDecidableEqRelEqual (k : ℕ) : DecidableEq (equal.Rel k)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance FFL.FirstOrder.Language.instEncodableFuncEqual (k : ℕ) : Encodable (equal.Func k)

Equations

• FFL.FirstOrder.Language.instEncodableFuncEqual k = IsEmpty.toEncodable

inductive FFL.FirstOrder.Language.ORing.Func : ℕ → Type

• zero : Func 0
• one : Func 0
• add : Func 2
• mul : Func 2

inductive FFL.FirstOrder.Language.ORing.Rel : ℕ → Type

• eq : Rel 2
• lt : Rel 2

@[reducible]

def FFL.FirstOrder.Language.oRing : Language

Equations

• ℒₒᵣ = { Func := FFL.FirstOrder.Language.ORing.Func, Rel := FFL.FirstOrder.Language.ORing.Rel }

def FFL.FirstOrder.Language.termℒₒᵣ : Lean.ParserDescr

Equations

• FFL.FirstOrder.Language.termℒₒᵣ = Lean.ParserDescr.node `FFL.FirstOrder.Language.termℒₒᵣ 1024 (Lean.ParserDescr.symbol "ℒₒᵣ")

@[instance_reducible]

instance FFL.FirstOrder.Language.ORing.instToStringFuncORing (k : ℕ) : ToString (ℒₒᵣ.Func k)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance FFL.FirstOrder.Language.ORing.instToStringRelORing (k : ℕ) : ToString (ℒₒᵣ.Rel k)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance FFL.FirstOrder.Language.ORing.instDecidableEqFuncORing (k : ℕ) : DecidableEq (ℒₒᵣ.Func k)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance FFL.FirstOrder.Language.ORing.instDecidableEqRelORing (k : ℕ) : DecidableEq (ℒₒᵣ.Rel k)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance FFL.FirstOrder.Language.ORing.instEncodableFuncORing (k : ℕ) : Encodable (ℒₒᵣ.Func k)

Equations

• One or more equations did not get rendered due to their size.

instance FFL.FirstOrder.Language.ORing.Func1IsEmpty : IsEmpty (ℒₒᵣ.Func 1)

theorem FFL.FirstOrder.Language.ORing.FuncGe3IsEmpty (k : ℕ) : k ≥ 3 → IsEmpty (ℒₒᵣ.Func k)

@[instance_reducible]

instance FFL.FirstOrder.Language.ORing.instEncodableRelORing (k : ℕ) : Encodable (ℒₒᵣ.Rel k)

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Language.ORing.funcEquivFinFour : (k : ℕ) × ℒₒᵣ.Func k ≃ Fin 4

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Language.ORing.relEquivFinTwo : (k : ℕ) × ℒₒᵣ.Rel k ≃ Fin 2

Equations

• One or more equations did not get rendered due to their size.

inductive FFL.FirstOrder.Language.Constant.Func (C : Type u_1) : ℕ → Type u_1

• const {C : Type u_1} (c : C) : Func C 0

def FFL.FirstOrder.Language.constant (C : Type u_1) : Language

Equations

• FFL.FirstOrder.Language.constant C = { Func := FFL.FirstOrder.Language.Constant.Func C, Rel := fun (x : ℕ) => PEmpty.{?u.1 + 1} }

@[instance_reducible]

instance FFL.FirstOrder.Language.instCoeFuncConstantOfNatNat (C : Type u_1) : Coe C ((constant C).Func 0)

Equations

• FFL.FirstOrder.Language.instCoeFuncConstantOfNatNat C = { coe := FFL.FirstOrder.Language.Constant.Func.const }

instance FFL.FirstOrder.Language.instIsConstantConstant (C : Type u_1) : (constant C).IsConstant

@[reducible, inline]

abbrev FFL.FirstOrder.Language.unit : Language

Equations

• FFL.FirstOrder.Language.unit = FFL.FirstOrder.Language.constant PUnit.{?u.1 + 1}

def FFL.FirstOrder.Language.ofFunc (F : ℕ → Type v) : Language

Equations

• FFL.FirstOrder.Language.ofFunc F = { Func := F, Rel := fun (x : ℕ) => PEmpty.{?u.1 + 1} }

def FFL.FirstOrder.Language.add (L₁ : Language) (L₂ : Language) : Language

Equations

• L₁.add L₂ = { Func := fun (k : ℕ) => L₁.Func k ⊕ L₂.Func k, Rel := fun (k : ℕ) => L₁.Rel k ⊕ L₂.Rel k }

@[instance_reducible]

instance FFL.FirstOrder.Language.instAdd : Add Language

Equations

• FFL.FirstOrder.Language.instAdd = { add := FFL.FirstOrder.Language.add }

def FFL.FirstOrder.Language.sigma {ι : Type u_1} (L : ι → Language) : Language

Equations

• FFL.FirstOrder.Language.sigma L = { Func := fun (k : ℕ) => (i : ι) × (L i).Func k, Rel := fun (k : ℕ) => (i : ι) × (L i).Rel k }

class FFL.FirstOrder.Language.Eq (L : Language) : Type u_1

• eq : L.Rel 2

class FFL.FirstOrder.Language.LT (L : Language) : Type u_1

• lt : L.Rel 2

class FFL.FirstOrder.Language.Mem (L : Language) : Type u_1

• mem : L.Rel 2

class FFL.FirstOrder.Language.Zero (L : Language) : Type u_1

• zero : L.Func 0

class FFL.FirstOrder.Language.One (L : Language) : Type u_1

• one : L.Func 0

class FFL.FirstOrder.Language.Add (L : Language) : Type u_1

• add : L.Func 2

class FFL.FirstOrder.Language.Mul (L : Language) : Type u_1

• mul : L.Func 2

class FFL.FirstOrder.Language.Pow (L : Language) : Type u_1

• pow : L.Func 2

class FFL.FirstOrder.Language.Exp (L : Language) : Type u_1

• exp : L.Func 1

class FFL.FirstOrder.Language.Pairing (L : Language) : Type u_1

• pair : L.Func 2

class FFL.FirstOrder.Language.Star (L : Language) : Type u_1

• star : L.Func 0

class FFL.FirstOrder.Language.ORing (L : Language) extends L.Eq, L.LT, L.Zero, L.One, L.Add, L.Mul : Type u_1

• eq : L.Rel 2
• lt : L.Rel 2
• zero : L.Func 0
• one : L.Func 0
• add : L.Func 2
• mul : L.Func 2

@[instance_reducible]

instance FFL.FirstOrder.Language.instORingORing : ℒₒᵣ.ORing

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance FFL.FirstOrder.Language.instConstantInhabitedORing : ℒₒᵣ.ConstantInhabited

Equations

• FFL.FirstOrder.Language.instConstantInhabitedORing = { default := FFL.FirstOrder.Language.Zero.zero }

@[instance_reducible]

instance FFL.FirstOrder.Language.instStarUnit : unit.Star

Equations

• FFL.FirstOrder.Language.instStarUnit = { star := FFL.FirstOrder.Language.Constant.Func.const () }

@[instance_reducible]

instance FFL.FirstOrder.Language.instStarAdd (L : Language) (S : Language) [S.Star] : (L.add S).Star

Equations

• L.instStarAdd S = { star := Sum.inr FFL.FirstOrder.Language.Star.star }

@[instance_reducible]

instance FFL.FirstOrder.Language.instZeroAdd (L : Language) (S : Language) [L.Zero] : (L.add S).Zero

Equations

• L.instZeroAdd S = { zero := Sum.inl FFL.FirstOrder.Language.Zero.zero }

@[instance_reducible]

instance FFL.FirstOrder.Language.instOneAdd (L : Language) (S : Language) [L.One] : (L.add S).One

Equations

• L.instOneAdd S = { one := Sum.inl FFL.FirstOrder.Language.One.one }

@[instance_reducible]

instance FFL.FirstOrder.Language.instAddAdd (L : Language) (S : Language) [L.Add] : (L.add S).Add

Equations

• L.instAddAdd S = { add := Sum.inl FFL.FirstOrder.Language.Add.add }

@[instance_reducible]

instance FFL.FirstOrder.Language.instMulAdd (L : Language) (S : Language) [L.Mul] : (L.add S).Mul

Equations

• L.instMulAdd S = { mul := Sum.inl FFL.FirstOrder.Language.Mul.mul }

@[instance_reducible]

instance FFL.FirstOrder.Language.instEqAdd (L : Language) (S : Language) [L.Eq] : (L.add S).Eq

Equations

• L.instEqAdd S = { eq := Sum.inl FFL.FirstOrder.Language.Eq.eq }

@[instance_reducible]

instance FFL.FirstOrder.Language.instLTAdd (L : Language) (S : Language) [L.LT] : (L.add S).LT

Equations

• L.instLTAdd S = { lt := Sum.inl FFL.FirstOrder.Language.LT.lt }

structure FFL.FirstOrder.Language.Hom (L₁ : Language) (L₂ : Language) : Type (max u_1 u_2)

• func {k : ℕ} : L₁.Func k → L₂.Func k
• rel {k : ℕ} : L₁.Rel k → L₂.Rel k

theorem FFL.FirstOrder.Language.Hom.ext_iff {L₁ : Language} {L₂ : Language} {x y : L₁.Hom L₂} : x = y ↔ @func L₁ L₂ x = @func L₁ L₂ y ∧ @rel L₁ L₂ x = @rel L₁ L₂ y

theorem FFL.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

def FFL.FirstOrder.«term_→ᵥ_» : Lean.TrailingParserDescr

A structure for the homomorphisms (respecting function and relation symbols) between first-order languages.

Equations

• FFL.FirstOrder.«term_→ᵥ_» = Lean.ParserDescr.trailingNode `FFL.FirstOrder.«term_→ᵥ_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ᵥ ") (Lean.ParserDescr.cat `term 26))

def FFL.FirstOrder.Language.Hom.id (L : Language) : L.Hom L

Equations

• FFL.FirstOrder.Language.Hom.id L = { func := fun {k : ℕ} => id, rel := fun {k : ℕ} => id }

def FFL.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 FFL.FirstOrder.Language.Hom.add₁ (L₁ : Language) (L₂ : Language) : L₁.Hom (L₁.add L₂)

Equations

• FFL.FirstOrder.Language.Hom.add₁ L₁ L₂ = { func := fun {k : ℕ} => Sum.inl, rel := fun {k : ℕ} => Sum.inl }

def FFL.FirstOrder.Language.Hom.add₂ (L₁ : Language) (L₂ : Language) : L₂.Hom (L₁.add L₂)

Equations

• FFL.FirstOrder.Language.Hom.add₂ L₁ L₂ = { func := fun {k : ℕ} => Sum.inr, rel := fun {k : ℕ} => Sum.inr }

theorem FFL.FirstOrder.Language.Hom.func_add₁ {k : ℕ} (L₁ : Language) (L₂ : Language) (f : L₁.Func k) : (add₁ L₁ L₂).func f = Sum.inl f

theorem FFL.FirstOrder.Language.Hom.rel_add₁ {k : ℕ} (L₁ : Language) (L₂ : Language) (r : L₁.Rel k) : (add₁ L₁ L₂).rel r = Sum.inl r

theorem FFL.FirstOrder.Language.Hom.func_add₂ {k : ℕ} (L₁ : Language) (L₂ : Language) (f : L₂.Func k) : (add₂ L₁ L₂).func f = Sum.inr f

theorem FFL.FirstOrder.Language.Hom.rel_add₂ {k : ℕ} (L₁ : Language) (L₂ : Language) (r : L₂.Rel k) : (add₂ L₁ L₂).rel r = Sum.inr r

@[simp]

theorem FFL.FirstOrder.Language.Hom.add₂_star (L₁ : Language) (L₂ : Language) [L₂.Star] : (add₂ L₁ L₂).func Star.star = Star.star

@[simp]

theorem FFL.FirstOrder.Language.Hom.add₁_zero (L₁ : Language) (L₂ : Language) [L₁.Zero] : (add₁ L₁ L₂).func Zero.zero = Zero.zero

@[simp]

theorem FFL.FirstOrder.Language.Hom.add₁_one (L₁ : Language) (L₂ : Language) [L₁.One] : (add₁ L₁ L₂).func One.one = One.one

@[simp]

theorem FFL.FirstOrder.Language.Hom.add₁_add (L₁ : Language) (L₂ : Language) [L₁.Add] : (add₁ L₁ L₂).func Add.add = Add.add

@[simp]

theorem FFL.FirstOrder.Language.Hom.add₁_mul (L₁ : Language) (L₂ : Language) [L₁.Mul] : (add₁ L₁ L₂).func Mul.mul = Mul.mul

@[simp]

theorem FFL.FirstOrder.Language.Hom.add₁_eq (L₁ : Language) (L₂ : Language) [L₁.Eq] : (add₁ L₁ L₂).rel Eq.eq = Eq.eq

@[simp]

theorem FFL.FirstOrder.Language.Hom.add₁_lt (L₁ : Language) (L₂ : Language) [L₁.LT] : (add₁ L₁ L₂).rel LT.lt = LT.lt

def FFL.FirstOrder.Language.Hom.sigma {ι : Type u_1} (L : ι → Language) (i : ι) : (L i).Hom (Language.sigma L)

Equations

• FFL.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⟩ }

theorem FFL.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 FFL.FirstOrder.Language.Hom.rel_sigma {ι : Type u_1} {k : ℕ} (L : ι → Language) (i : ι) (r : (L i).Rel k) : (sigma L i).rel r = ⟨i, r⟩

def FFL.FirstOrder.Language.ORing.embedding (L : Language) [L.ORing] : ℒₒᵣ.Hom L

Equations

• One or more equations did not get rendered due to their size.

class FFL.FirstOrder.Language.DecidableEq (L : Language) : Type u_1

• func (k : ℕ) : DecidableEq (L.Func k)
• rel (k : ℕ) : DecidableEq (L.Rel k)

@[instance_reducible]

instance FFL.FirstOrder.instDecidableEqOfFuncOfDecidableEqRel (L : Language) [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] : L.DecidableEq

Equations

• FFL.FirstOrder.instDecidableEqOfFuncOfDecidableEqRel L = { func := fun (x : ℕ) => inferInstance, rel := fun (x : ℕ) => inferInstance }

@[instance_reducible]

instance FFL.FirstOrder.instDecidableEqFuncOfDecidableEq (L : Language) [L.DecidableEq] (k : ℕ) : DecidableEq (L.Func k)

Equations

• FFL.FirstOrder.instDecidableEqFuncOfDecidableEq L k = FFL.FirstOrder.Language.DecidableEq.func k

@[instance_reducible]

instance FFL.FirstOrder.instDecidableEqRelOfDecidableEq (L : Language) [L.DecidableEq] (k : ℕ) : DecidableEq (L.Rel k)

Equations

• FFL.FirstOrder.instDecidableEqRelOfDecidableEq L k = FFL.FirstOrder.Language.DecidableEq.rel k

@[instance_reducible]

instance FFL.FirstOrder.instDecidableEqRelOfDecidableEq_1 (L : Language) [L.DecidableEq] (k : ℕ) : DecidableEq (L.Rel k)

Equations

• FFL.FirstOrder.instDecidableEqRelOfDecidableEq_1 L k = FFL.FirstOrder.Language.DecidableEq.rel k

class FFL.FirstOrder.Language.Encodable (L : Language) : Type u_1

• func (k : ℕ) : Encodable (L.Func k)
• rel (k : ℕ) : Encodable (L.Rel k)

@[instance_reducible]

instance FFL.FirstOrder.instEncodableOfFuncOfEncodableRel (L : Language) [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] : L.Encodable

Equations

• FFL.FirstOrder.instEncodableOfFuncOfEncodableRel L = { func := fun (x : ℕ) => inferInstance, rel := fun (x : ℕ) => inferInstance }

@[instance_reducible]

instance FFL.FirstOrder.instEncodableFuncOfEncodable (L : Language) [L.Encodable] (k : ℕ) : Encodable (L.Func k)

Equations

• FFL.FirstOrder.instEncodableFuncOfEncodable L k = FFL.FirstOrder.Language.Encodable.func k

@[instance_reducible]

instance FFL.FirstOrder.instEncodableRelOfEncodable (L : Language) [L.Encodable] (k : ℕ) : Encodable (L.Rel k)

Equations

• FFL.FirstOrder.instEncodableRelOfEncodable L k = FFL.FirstOrder.Language.Encodable.rel k

@[instance_reducible]

instance FFL.FirstOrder.instEncodableRelOfEncodable_1 (L : Language) [L.Encodable] (k : ℕ) : Encodable (L.Rel k)

Equations

• FFL.FirstOrder.instEncodableRelOfEncodable_1 L k = FFL.FirstOrder.Language.Encodable.rel k

class FFL.FirstOrder.Language.Finite (L : Language) : Type u_1

• func : Fintype ((k : ℕ) × L.Func k)
• rel : Fintype ((k : ℕ) × L.Rel k)

@[instance_reducible]

instance FFL.FirstOrder.instFiniteORing : ℒₒᵣ.Finite

Equations

• One or more equations did not get rendered due to their size.