Documentation

TauCeti.ModelTheory.Syntax

First-order terms under relabelling, substitution and language maps #

Mathlib's FirstOrder.Language.Term.varFinsetLeft collects the variables of a term over α ⊕ β that come from the left summand α. This file characterizes it through the full variable set Term.varFinset, and computes it after Term.relabel and Term.subst. It also records that a language map commutes with relabelling the variables of a term. Constructor equations for BoundedFormula.constantsVarsEquiv describe abstraction of constants in finitary formulas.

Main results #

source
theorem FirstOrder.Language.Term.mem_varFinsetLeft_iff {L : Language} {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {t : L.Term (α ⊕ β)} {a : α} :
a ∈ t.varFinsetLeft ↔ Sum.inl a ∈ t.varFinset

A left variable of a term over α ⊕ β is a variable Sum.inl a of the term.

source
theorem FirstOrder.Language.Term.mem_varFinsetLeft_relabel {L : Language} {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [DecidableEq β] (f : α → β ⊕ γ) {t : L.Term α} {b : β} :
b ∈ (relabel f t).varFinsetLeft ↔ ∃ x ∈ t.varFinset, f x = Sum.inl b

The left variables of t.relabel f are the left values of f on the variables of t.

source
theorem FirstOrder.Language.Term.mem_varFinsetLeft_subst {L : Language} {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [DecidableEq β] (σ : α → L.Term (β ⊕ γ)) {t : L.Term α} {b : β} :
b ∈ (t.subst σ).varFinsetLeft ↔ ∃ x ∈ t.varFinset, b ∈ (σ x).varFinsetLeft

The left variables of t.subst σ are the left variables of σ x for the variables x of t.

source
theorem FirstOrder.Language.Term.exists_eq_var_of_isRelational {L : Language} {α : Type u_1} [L.IsRelational] (t : L.Term α) :
∃ (a : α), t = var a

In a relational language, every term is a variable.

source
theorem FirstOrder.Language.Term.exists_eq_var_inr_of_isRelational {L : Language} {α : Type u_1} {β : Type u_2} [L.IsRelational] [IsEmpty α] (t : L.Term (α ⊕ β)) :
∃ (b : β), t = var (Sum.inr b)

In a relational language, a term whose left variables range over an empty type is a right variable.

source
@[simp]
theorem FirstOrder.Language.LHom.onTerm_relabel {L : Language} {L' : Language} {β : Type u_1} {γ : Type u_2} (g : L →ᴸ L') (h : β → γ) (t : L.Term β) :
g.onTerm (Term.relabel h t) = Term.relabel h (g.onTerm t)

A language map commutes with relabelling the variables of a term.

source
@[simp]
theorem FirstOrder.Language.BoundedFormula.constantsVarsEquiv_falsum {L : Language} {α : Type u_1} {γ : Type u_2} {n : ℕ} :
constantsVarsEquiv falsum = falsum
source
@[simp]
theorem FirstOrder.Language.BoundedFormula.constantsVarsEquiv_equal {L : Language} {α : Type u_1} {γ : Type u_2} {n : ℕ} (t₁ t₂ : (L.withConstants γ).Term (α ⊕ Fin n)) :
constantsVarsEquiv (equal t₁ t₂) = equal (Term.constantsVarsEquivLeft t₁) (Term.constantsVarsEquivLeft t₂)
source
@[simp]
theorem FirstOrder.Language.BoundedFormula.constantsVarsEquiv_rel {L : Language} {α : Type u_1} {γ : Type u_2} {n l : ℕ} (R : (L.withConstants γ).Relations l) (ts : Fin l → (L.withConstants γ).Term (α ⊕ Fin n)) :
constantsVarsEquiv (rel R ts) = rel ((Equiv.sumEmpty (L.Relations l) ((constantsOn γ).Relations l)) R) fun (i : Fin l) => Term.constantsVarsEquivLeft (ts i)
source
@[simp]
theorem FirstOrder.Language.BoundedFormula.constantsVarsEquiv_imp {L : Language} {α : Type u_1} {γ : Type u_2} {n : ℕ} (φ ψ : (L.withConstants γ).BoundedFormula α n) :
constantsVarsEquiv (φ.imp ψ) = (constantsVarsEquiv φ).imp (constantsVarsEquiv ψ)
source
@[simp]
theorem FirstOrder.Language.BoundedFormula.constantsVarsEquiv_all {L : Language} {α : Type u_1} {γ : Type u_2} {n : ℕ} (φ : (L.withConstants γ).BoundedFormula α (n + 1)) :
constantsVarsEquiv φ.all = (constantsVarsEquiv φ).all