Documentation

Logic.FirstOrder.Basic.Syntax.Term

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 ξ.

@[reducible, inline]
abbrev LO.FirstOrder.Term (L : LO.FirstOrder.Language) (ξ : Type u_1) :
Type (max u_1 u_2)
Equations
Equations
def LO.FirstOrder.Semiterm.toStr {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [(k : ) → ToString (L.Func k)] [ToString ξ] :
Equations
instance LO.FirstOrder.Semiterm.instRepr {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [(k : ) → ToString (L.Func k)] [ToString ξ] :
Equations
instance LO.FirstOrder.Semiterm.instToString {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [(k : ) → ToString (L.Func k)] [ToString ξ] :
Equations
  • LO.FirstOrder.Semiterm.instToString = { toString := LO.FirstOrder.Semiterm.toStr }
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 kLO.FirstOrder.Semiterm L ξ n) :
Equations
Equations
@[simp]
theorem LO.FirstOrder.Semiterm.bv_func {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } {k : } (f : L.Func k) (v : Fin kLO.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 0LO.FirstOrder.Semiterm L ξ n) :
Equations
  • t.Positive = xt.bv, 0 < x
@[simp]
theorem LO.FirstOrder.Semiterm.Positive.bvar {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } {x : Fin (n + 1)} :
@[simp]
@[simp]
theorem LO.FirstOrder.Semiterm.Positive.func {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } {k : } (f : L.Func k) (v : Fin kLO.FirstOrder.Semiterm L ξ (n + 1)) :
(LO.FirstOrder.Semiterm.func f v).Positive ∀ (i : Fin k), (v i).Positive
Equations
@[simp]
theorem LO.FirstOrder.Semiterm.fv_func {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [DecidableEq ξ] {k : } (f : L.Func k) (v : Fin kLO.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 0LO.FirstOrder.Semiterm L ξ n) :
Equations
@[simp]
@[simp]
theorem LO.FirstOrder.Semiterm.complexity_func {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } {k : } (f : L.Func k) (v : Fin kLO.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 kLO.FirstOrder.Semiterm L ξ n) (i : Fin k) :
(v i).complexity < (LO.FirstOrder.Semiterm.func f v).complexity
Equations
@[reducible, inline]
abbrev LO.FirstOrder.Semiterm.fvar? {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (t : LO.FirstOrder.Semiterm L ξ n) (x : ξ) :
Equations
  • t.fvar? x = (x t.fvarList)
@[simp]
@[simp]
theorem LO.FirstOrder.Semiterm.fvarList_fvar {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } {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 kLO.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 : ξ) :
@[simp]
theorem LO.FirstOrder.Semiterm.fvar?_fvar {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } (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 kLO.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
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 kLO.FirstOrder.Semiterm L₁ ξ n) :
@[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
Equations
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] :
Equations
theorem LO.FirstOrder.Semiterm.default_def {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : } [L.ConstantInhabited] :
default = LO.FirstOrder.Semiterm.func default ![]