Terms of first-order logic

This file defines the terms of first-order logic.

The bounded variables are denoted by #x for x : Fin n, and free variables are denoted by &x for x : ξ. t : Semiterm L ξ n is a (semi-)term of language L with bounded variables of Fin n and free variables of ξ.

inductive LO.FirstOrder.Semiterm (L : Language) (ξ : Type u_1) (n : ℕ) : Type (max u_1 u_2)

A semiterm of language L, with bound variables indexed by Fin n and free variables indexed by ξ. In LO.FirstOrder.Semiformula, bound variables are de Bruijn indices with a separate type from free variables.

• bvar {L : Language} {ξ : Type u_1} {n : ℕ} : Fin n → Semiterm L ξ n
• fvar {L : Language} {ξ : Type u_1} {n : ℕ} : ξ → Semiterm L ξ n
• func {L : Language} {ξ : Type u_1} {n arity : ℕ} : L.Func arity → (Fin arity → Semiterm L ξ n) → Semiterm L ξ n

def LO.FirstOrder.«term&_» : Lean.ParserDescr

&x is the free variable indexed by the element x : ξ.

Equations

• LO.FirstOrder.«term&_» = Lean.ParserDescr.node `LO.FirstOrder.«term&_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "&") (Lean.ParserDescr.cat `term 1024))

def LO.FirstOrder.«term#_» : Lean.ParserDescr

#x is the bound variable with de Bruijn index x.

Equations

• LO.FirstOrder.«term#_» = Lean.ParserDescr.node `LO.FirstOrder.«term#_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#") (Lean.ParserDescr.cat `term 1024))

@[reducible, inline]

abbrev LO.FirstOrder.Term (L : Language) (ξ : Type u_1) : Type (max u_1 u_2)

Equations

• LO.FirstOrder.Term L ξ = LO.FirstOrder.Semiterm L ξ 0

@[reducible, inline]

abbrev LO.FirstOrder.ClosedSemiterm (L : Language) (n : ℕ) : Type u_1

Equations

• LO.FirstOrder.ClosedSemiterm L n = LO.FirstOrder.Semiterm L Empty n

@[reducible, inline]

abbrev LO.FirstOrder.ClosedTerm (L : Language) : Type u_1

Equations

• LO.FirstOrder.ClosedTerm L = LO.FirstOrder.Semiterm L Empty 0

@[reducible, inline]

abbrev LO.FirstOrder.SyntacticSemiterm (L : Language) (n : ℕ) : Type u_1

Equations

• LO.FirstOrder.SyntacticSemiterm L n = LO.FirstOrder.Semiterm L ℕ n

@[reducible, inline]

abbrev LO.FirstOrder.SyntacticTerm (L : Language) : Type u_1

Equations

• LO.FirstOrder.SyntacticTerm L = LO.FirstOrder.SyntacticSemiterm L 0

@[implicit_reducible]

instance LO.FirstOrder.Semiterm.instInhabited {L : Language} {ξ : Type u_1} {n : ℕ} [Inhabited ξ] : Inhabited (Semiterm L ξ n)

Equations

• LO.FirstOrder.Semiterm.instInhabited = { default := LO.FirstOrder.Semiterm.fvar default }

def LO.FirstOrder.Semiterm.toStr {L : Language} {ξ : Type u_1} {n : ℕ} [(k : ℕ) → ToString (L.Func k)] [ToString ξ] : Semiterm L ξ n → String

Equations

• (LO.FirstOrder.Semiterm.bvar x_1).toStr = "x_{" ++ toString (n - 1 - ↑x_1) ++ "}"
• (LO.FirstOrder.Semiterm.fvar x_1).toStr = "z_{" ++ toString x_1 ++ "}"
• (LO.FirstOrder.Semiterm.func c a).toStr = toString c
• (LO.FirstOrder.Semiterm.func f v).toStr = ("{" ++ toString f ++ "} \\left(" ++ String.vecToStr fun (i : Fin (n_1 + 1)) => (v i).toStr) ++ "\\right)"

@[implicit_reducible]

instance LO.FirstOrder.Semiterm.instRepr {L : Language} {ξ : Type u_1} {n : ℕ} [(k : ℕ) → ToString (L.Func k)] [ToString ξ] : Repr (Semiterm L ξ n)

Equations

• LO.FirstOrder.Semiterm.instRepr = { reprPrec := fun (t : LO.FirstOrder.Semiterm L ξ n) (x : ℕ) => Std.Format.text t.toStr }

@[implicit_reducible]

instance LO.FirstOrder.Semiterm.instToString {L : Language} {ξ : Type u_1} {n : ℕ} [(k : ℕ) → ToString (L.Func k)] [ToString ξ] : ToString (Semiterm L ξ n)

Equations

• LO.FirstOrder.Semiterm.instToString = { toString := LO.FirstOrder.Semiterm.toStr }

def LO.FirstOrder.Semiterm.hasDecEq {L : Language} {ξ : Type u_1} {n : ℕ} [(k : ℕ) → DecidableEq (L.Func k)] [DecidableEq ξ] (t u : Semiterm L ξ n) : Decidable (t = u)

Equations

• One or more equations did not get rendered due to their size.
• (LO.FirstOrder.Semiterm.bvar x_2).hasDecEq (LO.FirstOrder.Semiterm.bvar y) = ⋯.mpr (decEq x_2 y)
• (LO.FirstOrder.Semiterm.bvar a).hasDecEq (LO.FirstOrder.Semiterm.fvar a_1) = isFalse ⋯
• (LO.FirstOrder.Semiterm.bvar a).hasDecEq (LO.FirstOrder.Semiterm.func a_1 a_2) = isFalse ⋯
• (LO.FirstOrder.Semiterm.fvar a).hasDecEq (LO.FirstOrder.Semiterm.bvar a_1) = isFalse ⋯
• (LO.FirstOrder.Semiterm.fvar x_2).hasDecEq (LO.FirstOrder.Semiterm.fvar y) = ⋯.mpr (decEq x_2 y)
• (LO.FirstOrder.Semiterm.fvar a).hasDecEq (LO.FirstOrder.Semiterm.func a_1 a_2) = isFalse ⋯
• (LO.FirstOrder.Semiterm.func a a_1).hasDecEq (LO.FirstOrder.Semiterm.bvar a_2) = isFalse ⋯
• (LO.FirstOrder.Semiterm.func a a_1).hasDecEq (LO.FirstOrder.Semiterm.fvar a_2) = isFalse ⋯

@[implicit_reducible]

instance LO.FirstOrder.Semiterm.instDecidableEq {L : Language} {ξ : Type u_1} {n : ℕ} [(k : ℕ) → DecidableEq (L.Func k)] [DecidableEq ξ] : DecidableEq (Semiterm L ξ n)

Equations

• LO.FirstOrder.Semiterm.instDecidableEq = LO.FirstOrder.Semiterm.hasDecEq

def LO.FirstOrder.Semiterm.complexity {L : Language} {ξ : Type u_1} {n : ℕ} : Semiterm L ξ n → ℕ

The complexity of a semiterm, taking suprema at function symbols.

Equations

• (LO.FirstOrder.Semiterm.bvar a).complexity = 0
• (LO.FirstOrder.Semiterm.fvar a).complexity = 0
• (LO.FirstOrder.Semiterm.func a v).complexity = (Finset.univ.sup fun (i : Fin arity) => (v i).complexity) + 1

@[simp]

theorem LO.FirstOrder.Semiterm.complexity_bvar {L : Language} {ξ : Type u_1} {n : ℕ} (x : Fin n) : (bvar x).complexity = 0

@[simp]

theorem LO.FirstOrder.Semiterm.complexity_fvar {L : Language} {ξ : Type u_1} {n : ℕ} (x : ξ) : (fvar x).complexity = 0

theorem LO.FirstOrder.Semiterm.complexity_func {L : Language} {ξ : Type u_1} {n k : ℕ} (f : L.Func k) (v : Fin k → Semiterm L ξ n) : (func f v).complexity = (Finset.univ.sup fun (i : Fin k) => (v i).complexity) + 1

@[simp]

theorem LO.FirstOrder.Semiterm.complexity_func_lt {L : Language} {ξ : Type u_1} {n k : ℕ} (f : L.Func k) (v : Fin k → Semiterm L ξ n) (i : Fin k) : (v i).complexity < (func f v).complexity

@[reducible, inline]

abbrev LO.FirstOrder.Semiterm.func! {L : Language} {ξ : Type u_1} {n : ℕ} (k : ℕ) (f : L.Func k) (v : Fin k → Semiterm L ξ n) : Semiterm L ξ n

Equations

• LO.FirstOrder.Semiterm.func! k f v = LO.FirstOrder.Semiterm.func f v

def LO.FirstOrder.Semiterm.bv {L : Language} {ξ : Type u_1} {n : ℕ} : Semiterm L ξ n → Finset (Fin n)

The set of bound variables occurring in a semiterm.

Equations

• (LO.FirstOrder.Semiterm.bvar a).bv = {a}
• (LO.FirstOrder.Semiterm.fvar a).bv = ∅
• (LO.FirstOrder.Semiterm.func a v).bv = Finset.univ.biUnion fun (i : Fin arity) => (v i).bv

@[simp]

theorem LO.FirstOrder.Semiterm.bv_bvar {L : Language} {ξ : Type u_1} {n : ℕ} {x : Fin n} : (bvar x).bv = {x}

@[simp]

theorem LO.FirstOrder.Semiterm.bv_fvar {L : Language} {ξ : Type u_1} {n : ℕ} {x : ξ} : (fvar x).bv = ∅

theorem LO.FirstOrder.Semiterm.bv_func {L : Language} {ξ : Type u_1} {n k : ℕ} (f : L.Func k) (v : Fin k → Semiterm L ξ n) : (func f v).bv = Finset.univ.biUnion fun (i : Fin k) => (v i).bv

@[simp]

theorem LO.FirstOrder.Semiterm.bv_constant {L : Language} {ξ : Type u_1} {n : ℕ} (f : L.Func 0) (v : Fin 0 → Semiterm L ξ n) : (func f v).bv = ∅

def LO.FirstOrder.Semiterm.Positive {L : Language} {ξ : Type u_1} {n : ℕ} (t : Semiterm L ξ (n + 1)) : Prop

Equations

• t.Positive = ∀ x ∈ t.bv, 0 < x

@[simp]

theorem LO.FirstOrder.Semiterm.Positive.bvar {L : Language} {ξ : Type u_1} {n : ℕ} {x : Fin (n + 1)} : (bvar x).Positive ↔ 0 < x

@[simp]

theorem LO.FirstOrder.Semiterm.Positive.fvar {L : Language} {ξ : Type u_1} {n : ℕ} {x : ξ} : (fvar x).Positive

@[simp]

theorem LO.FirstOrder.Semiterm.Positive.func {L : Language} {ξ : Type u_1} {n k : ℕ} (f : L.Func k) (v : Fin k → Semiterm L ξ (n + 1)) : (func f v).Positive ↔ ∀ (i : Fin k), (v i).Positive

theorem LO.FirstOrder.Semiterm.bv_eq_empty_of_positive {L : Language} {ξ : Type u_1} {t : Semiterm L ξ 1} (ht : t.Positive) : t.bv = ∅

def LO.FirstOrder.Semiterm.freeVariables {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] : Semiterm L ξ n → Finset ξ

The set of free variables occuring in a semiterm.

Equations

• (LO.FirstOrder.Semiterm.bvar a).freeVariables = ∅
• (LO.FirstOrder.Semiterm.fvar a).freeVariables = {a}
• (LO.FirstOrder.Semiterm.func a v).freeVariables = Finset.univ.biUnion fun (i : Fin arity) => (v i).freeVariables

@[simp]

theorem LO.FirstOrder.Semiterm.freeVariables_bvar {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] {x : Fin n} : (bvar x).freeVariables = ∅

@[simp]

theorem LO.FirstOrder.Semiterm.freeVariables_fvar {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] {x : ξ} : (fvar x).freeVariables = {x}

theorem LO.FirstOrder.Semiterm.freeVariables_func {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] {k : ℕ} (f : L.Func k) (v : Fin k → Semiterm L ξ n) : (func f v).freeVariables = Finset.univ.biUnion fun (i : Fin k) => (v i).freeVariables

@[simp]

theorem LO.FirstOrder.Semiterm.freeVariables_constant {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (f : L.Func 0) (v : Fin 0 → Semiterm L ξ n) : (func f v).freeVariables = ∅

@[simp]

theorem LO.FirstOrder.Semiterm.freeVariables_empty {L : Language} {n : ℕ} {ο : Type u_6} [IsEmpty ο] {t : Semiterm L ο n} : t.freeVariables = ∅

@[reducible, inline]

abbrev LO.FirstOrder.Semiterm.FVar? {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (t : Semiterm L ξ n) (x : ξ) : Prop

Equations

• t.FVar? x = (x ∈ t.freeVariables)

@[simp]

theorem LO.FirstOrder.Semiterm.fvar?_bvar {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (x : Fin n) (z : ξ) : ¬(bvar x).FVar? z

@[simp]

theorem LO.FirstOrder.Semiterm.fvar?_fvar {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (x z : ξ) : (fvar x).FVar? z ↔ x = z

@[simp]

theorem LO.FirstOrder.Semiterm.fvar?_func {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (x : ξ) {k : ℕ} (f : L.Func k) (v : Fin k → Semiterm L ξ n) : (func f v).FVar? x ↔ ∃ (i : Fin k), (v i).FVar? x

def LO.FirstOrder.Semiterm.lMap {L₁ : Language} {L₂ : Language} {ξ : Type u_1} {n : ℕ} (Φ : L₁.Hom L₂) : Semiterm L₁ ξ n → Semiterm L₂ ξ n

The map on terms induced from a homomorphism between languages.

Equations

• LO.FirstOrder.Semiterm.lMap Φ (LO.FirstOrder.Semiterm.bvar a) = LO.FirstOrder.Semiterm.bvar a
• LO.FirstOrder.Semiterm.lMap Φ (LO.FirstOrder.Semiterm.fvar a) = LO.FirstOrder.Semiterm.fvar a
• LO.FirstOrder.Semiterm.lMap Φ (LO.FirstOrder.Semiterm.func a v) = LO.FirstOrder.Semiterm.func (Φ.func a) fun (i : Fin arity) => LO.FirstOrder.Semiterm.lMap Φ (v i)

@[simp]

theorem LO.FirstOrder.Semiterm.lMap_bvar {L₁ : Language} {L₂ : Language} {ξ : Type u_1} {n : ℕ} (Φ : L₁.Hom L₂) (x : Fin n) : lMap Φ (bvar x) = bvar x

@[simp]

theorem LO.FirstOrder.Semiterm.lMap_fvar {L₁ : Language} {L₂ : Language} {ξ : Type u_1} {n : ℕ} (Φ : L₁.Hom L₂) (x : ξ) : lMap Φ (fvar x) = fvar x

@[simp]

theorem LO.FirstOrder.Semiterm.lMap_func {L₁ : Language} {L₂ : Language} {ξ : Type u_1} {n : ℕ} (Φ : L₁.Hom L₂) {k : ℕ} (f : L₁.Func k) (v : Fin k → Semiterm L₁ ξ n) : lMap Φ (func f v) = func (Φ.func f) (lMap Φ ∘ v)

theorem LO.FirstOrder.Semiterm.lMap_func' {L₁ : Language} {L₂ : Language} {ξ : Type u_1} {n : ℕ} (Φ : L₁.Hom L₂) {k : ℕ} (f : L₁.Func k) (v : Fin k → Semiterm L₁ ξ n) : lMap Φ (func f v) = func (Φ.func f) fun (i : Fin k) => lMap Φ (v i)

@[simp]

theorem LO.FirstOrder.Semiterm.lMap_positive {L₁ : Language} {L₂ : Language} {ξ : Type u_1} {n : ℕ} (Φ : L₁.Hom L₂) (t : Semiterm L₁ ξ (n + 1)) : (lMap Φ t).Positive ↔ t.Positive

@[simp]

theorem LO.FirstOrder.Semiterm.freeVariables_lMap {L₁ : Language} {L₂ : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (Φ : L₁.Hom L₂) (t : Semiterm L₁ ξ n) : (lMap Φ t).freeVariables = t.freeVariables

@[implicit_reducible]

instance LO.FirstOrder.Semiterm.instInhabited_1 {L : Language} {ξ : Type u_1} {n : ℕ} [L.ConstantInhabited] : Inhabited (Semiterm L ξ n)

Equations

• LO.FirstOrder.Semiterm.instInhabited_1 = { default := LO.FirstOrder.Semiterm.func default ![] }

theorem LO.FirstOrder.Semiterm.default_def {L : Language} {ξ : Type u_1} {n : ℕ} [L.ConstantInhabited] : default = func default ![]

def LO.FirstOrder.Semiterm.fvarList {L : Language} {ξ : Type u_1} {n : ℕ} : Semiterm L ξ n → List ξ

Equations

• (LO.FirstOrder.Semiterm.bvar a).fvarList = []
• (LO.FirstOrder.Semiterm.fvar a).fvarList = [a]
• (LO.FirstOrder.Semiterm.func a v).fvarList = (Matrix.toList fun (i : Fin arity) => (v i).fvarList).flatten

def LO.FirstOrder.Semiterm.idxOfFVar {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (t : Semiterm L ξ n) : ξ → ℕ

Equations

• t.idxOfFVar a = List.idxOf a t.fvarList

def LO.FirstOrder.Semiterm.enumarateFVar {L : Language} {ξ : Type u_1} {n : ℕ} [Inhabited ξ] (t : Semiterm L ξ n) : ℕ → ξ

Equations

• t.enumarateFVar i = if hi : i < t.fvarList.length then t.fvarList.get ⟨i, hi⟩ else default

theorem LO.FirstOrder.Semiterm.enumarateFVar_idxOfFVar {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] [Inhabited ξ] {t : Semiterm L ξ n} {x : ξ} (hx : x ∈ t.fvarList) : t.enumarateFVar (t.idxOfFVar x) = x

theorem LO.FirstOrder.Semiterm.mem_fvarList_iff_fvar? {L : Language} {ξ : Type u_1} {n : ℕ} {x : ξ} [DecidableEq ξ] {t : Semiterm L ξ n} : x ∈ t.fvarList ↔ t.FVar? x