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

source

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

Type (max u_1 u_2)

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

Instances For

source

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))

source

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))

source

@[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

source

@[reducible, inline]

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

Type u_1

Equations

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

Instances For

source

@[reducible, inline]

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

Type u_1

Equations

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

source

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 }

source

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)"

source

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 }

source

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 }

source

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 ⋯

source

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

source

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

Semiterm L ξ n → ℕ

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

source

@[simp]

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

(bvar x).complexity = 0

source

@[simp]

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

(fvar x).complexity = 0

source

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

source

@[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

source

@[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

source

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

Semiterm L ξ n → Finset (Fin n)

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

source

@[simp]

theorem LO.FirstOrder.Semiterm.bv_bvar {L : Language} {ξ : Type u_1} {n : ℕ} {x : Fin n} :

(bvar x).bv = {x}

source

@[simp]

theorem LO.FirstOrder.Semiterm.bv_fvar {L : Language} {ξ : Type u_1} {n : ℕ} {x : ξ} :

(fvar x).bv = ∅

source

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

source

@[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 = ∅

source

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

source

@[simp]

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

(bvar x).Positive ↔ 0 < x

source

@[simp]

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

(fvar x).Positive

source

@[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

source

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

t.bv = ∅

source

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

Semiterm L ξ n → Finset ξ

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

source

@[simp]

theorem LO.FirstOrder.Semiterm.freeVariables_bvar {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] {x : Fin n} :

(bvar x).freeVariables = ∅

source

@[simp]

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

(fvar x).freeVariables = {x}

source

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

source

@[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 = ∅

source

@[simp]

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

t.freeVariables = ∅

source

@[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)

source

@[simp]

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

¬(bvar x).FVar? z

source

@[simp]

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

(fvar x).FVar? z ↔ x = z

source

@[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

source

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

Semiterm L₁ ξ n → Semiterm L₂ ξ n

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)

source

@[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

source

@[simp]

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

lMap Φ (fvar x) = fvar x

source

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)

source

@[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

source

@[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

source

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 ![] }

source

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

default = func default ![]

Documentation

Foundation.Logic.Predicate.Term

Terms of first-order logic #