Terms of first-order logic

This file defines the terms of first-order Foundation.

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 : LO.FirstOrder.Language) (ξ : Type u_1) (n : ℕ) : Type (max u_1 u_2)

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

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

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

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 : LO.FirstOrder.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.SyntacticSemiterm (L : LO.FirstOrder.Language) (n : ℕ) : Type u_1

Equations

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

@[reducible, inline]

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

Equations

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

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

Equations

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

def LO.FirstOrder.Semiterm.toStr {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [(k : ℕ) → ToString (L.Func k)] [ToString ξ] : LO.FirstOrder.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)"

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

Equations

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

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

Equations

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

def LO.FirstOrder.Semiterm.hasDecEq {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [(k : ℕ) → DecidableEq (L.Func k)] [DecidableEq ξ] (t : LO.FirstOrder.Semiterm L ξ n) (u : LO.FirstOrder.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 ⋯

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

Equations

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

@[reducible, inline]

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

Equations

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

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

Equations

• (LO.FirstOrder.Semiterm.bvar x_1).bv = {x_1}
• (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 : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {x : Fin n} : (LO.FirstOrder.Semiterm.bvar x).bv = {x}

@[simp]

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

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

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

Equations

• (LO.FirstOrder.Semiterm.bvar x_1).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 : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (x : Fin n) : (LO.FirstOrder.Semiterm.bvar x).complexity = 0

@[simp]

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

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

@[simp]

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

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

Equations

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

@[reducible, inline]

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

Equations

• t.fvar? x = (x ∈ t.fvarList)

@[simp]

theorem LO.FirstOrder.Semiterm.fvarList_bvar {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {x : Fin n} : (LO.FirstOrder.Semiterm.bvar x).fvarList = []

@[simp]

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

@[simp]

theorem LO.FirstOrder.Semiterm.mem_fvarList_func {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {x : ξ} {k : ℕ} {f : L.Func k} {v : Fin k → LO.FirstOrder.Semiterm L ξ n} : x ∈ (LO.FirstOrder.Semiterm.func f v).fvarList ↔ ∃ (i : Fin k), x ∈ (v i).fvarList

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem LO.FirstOrder.Semiterm.fvarList_empty {L : LO.FirstOrder.Language} {n : ℕ} {o : Type u_6} [e : IsEmpty o] {t : LO.FirstOrder.Semiterm L o n} : t.fvarList = []

@[simp]

theorem LO.FirstOrder.Semiterm.fvarList_to_finset {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (t : LO.FirstOrder.Semiterm L ξ n) : t.fvarList.toFinset = t.fv

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

Equations

• LO.FirstOrder.Semiterm.lMap Φ (LO.FirstOrder.Semiterm.bvar x_1) = LO.FirstOrder.Semiterm.bvar x_1
• 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₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (Φ : L₁.Hom L₂) (x : Fin n) : LO.FirstOrder.Semiterm.lMap Φ (LO.FirstOrder.Semiterm.bvar x) = LO.FirstOrder.Semiterm.bvar x

@[simp]

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

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

@[simp]

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

@[simp]

theorem LO.FirstOrder.Semiterm.fvarList_lMap {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (Φ : L₁.Hom L₂) (t : LO.FirstOrder.Semiterm L₁ ξ n) : (LO.FirstOrder.Semiterm.lMap Φ t).fvarList = t.fvarList

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

Equations

• t.fvEnum a = List.indexOf a t.fvarList

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

Equations

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

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

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

Equations

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

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