First-order syntax

DefinitionLeaf count of a first-order term#✓fully proved

The number of leaves of a first-order term.

Variables and nullary function applications are leaves. A nonnullary function application has the sum of the leaf counts of its arguments.

def leafCount {L : FirstOrder.Language.{u, v}} {V : Type w} : L.Term V → Nat
  | .var _ => 1
  | .func (l := n) _ terms => if n = 0 then 1 else ∑ i, leafCount (terms i)

Used by 1

Used byRelabeling variables preserves the leaf count

TheoremRelabeling variables preserves the leaf count#✓fully proved

Relabeling variables does not change the number of leaves.

@[simp]
theorem leafCount_relabel {L : FirstOrder.Language.{u, v}} {V : Type w} {W : Type w'}
    (g : V → W)
    (t : L.Term V) : (t.relabel g).leafCount = t.leafCount

Uses 1

Statement usesLeaf count of a first-order term

DefinitionSymbols of a term#✓fully proved

The set of symbols of a first-order language \(L\) that occur in a term \(t\) (with free variables and possibly bound variables), defined by recursion on \(t\): a variable contributes no symbols, and \(f(t_1, \dots, t_k)\) contributes the function symbol \(f\) together with the symbols of the terms \(t_i\). The result lies in the set of all symbols of \(L\), but only function symbols can occur in a term.

def termSymbols {n : ℕ} : L.Term (α ⊕ Fin n) → Set L.Symbols
  | .var _ => ∅
  | .func f ts => {Sum.inl ⟨_, f⟩} ∪ ⋃ i, termSymbols (ts i)

Used by 1

Used bySymbols of a formula

DefinitionSymbols of a formula#✓fully proved

The set of function and relation symbols of a first-order language \(L\) that occur in a formula \(\varphi\) (with free variables and possibly bound variables), defined by recursion on \(\varphi\): falsum \(\bot\) contributes no symbols, an equation \(t_1 = t_2\) contributes the symbols of the terms \(t_1\) and \(t_2\), an atomic formula \(R(t_1, \dots, t_k)\) contributes \(R\) together with the symbols of the terms \(t_i\), an implication \(\varphi \to \psi\) contributes the symbols of \(\varphi\) and of \(\psi\), and \(\forall x\, \varphi\) contributes the symbols of \(\varphi\). Variables and the equality sign contribute nothing.

def formulaSymbols {n : ℕ} : L.BoundedFormula α n → Set L.Symbols
  | .falsum => ∅
  | .equal t₁ t₂ => termSymbols t₁ ∪ termSymbols t₂
  | .rel R ts => {Sum.inr ⟨_, R⟩} ∪ ⋃ i, termSymbols (ts i)
  | .imp φ ψ => formulaSymbols φ ∪ formulaSymbols ψ
  | .all φ => formulaSymbols φ

Uses 1

Statement usesSymbols of a term

DefinitionInstantiating the outermost bound variable of a term#✓fully proved

Let \(L\) be a first-order language, \(t\) an \(L\)-term with free variables in \(\alpha\), and \(s\) an \(L\)-term with free variables in \(\alpha\) and \(m + 1\) bound variables \(0, \dots, m\). The instantiation of \(t\) in \(s\) is the term with free variables in \(\alpha\) and \(m\) bound variables obtained from \(s\) by substituting \(t\) for the bound variable \(0\), replacing each other bound variable \(i + 1\) by \(i\), and leaving the free variables unchanged.

def instantiateTerm (t : L.Term α) {m : ℕ} (s : L.Term (α ⊕ Fin (m + 1))) :
    L.Term (α ⊕ Fin m) :=
  s.subst (Sum.elim (fun a ↦ Term.var (Sum.inl a))
    (Fin.cases (t.relabel Sum.inl) fun i ↦ Term.var (Sum.inr i)))

Used by 17

Used byExistential introduction · Weakening · Injective renaming preserves derivability · Symmetry of equality in natural deduction · Transitivity of equality in natural deduction · Instantiating the outermost bound variable of a formula · Instantiation commutes with the universal quantifier · Instantiation shifts the remaining bound variables down · Instantiation at the outermost bound variable · Truth of an instance · Free variables of an instance · Congruence for function symbols in a maximal consistent set · Language homomorphisms commute with instantiation in formulas · Language homomorphisms commute with instantiation in terms · Truth lemma for the first-order term model · Replacing an argument of a relation symbol by an equal term · Renaming free variables along an arbitrary map preserves derivability

DefinitionInstantiating the outermost bound variable of a formula#✓fully proved

Let \(L\) be a first-order language, \(t\) an \(L\)-term with free variables in \(\alpha\), and \(\varphi\) a bounded \(L\)-formula with free variables in \(\alpha\) and \(m + 1\) bound variables \(0, \dots, m\). The instantiation of \(t\) in \(\varphi\) is the bounded formula with free variables in \(\alpha\) and \(m\) bound variables obtained from \(\varphi\) by instantiating \(t\) in every term of its atomic subformulas: in each term, \(t\) is substituted for the bound variable \(0\) and each other bound variable \(i + 1\) is replaced by \(i\). Falsum, implication and universal quantification are kept, the quantifier being passed through unchanged since bound variables are de Bruijn levels.

def instantiate (t : L.Term α) : ∀ {m : ℕ}, L.BoundedFormula α (m + 1) → L.BoundedFormula α m
  | _, .falsum => .falsum
  | _, .equal t₁ t₂ => .equal (instantiateTerm t t₁) (instantiateTerm t t₂)
  | _, .rel R ts => .rel R fun i ↦ instantiateTerm t (ts i)
  | _, .imp φ ψ => .imp (instantiate t φ) (instantiate t ψ)
  | _, .all φ => .all (instantiate t φ)

Uses 1 · Used by 23

Statement usesInstantiating the outermost bound variable of a term

Used byNatural deduction · Existential introduction · Weakening · Injective renaming preserves derivability · Soundness of first-order natural deduction · Symmetry of equality in natural deduction · Transitivity of equality in natural deduction · Instantiation commutes with the universal quantifier · Truth of an instance · Universal formulas from Henkin witnesses · Henkin extension of a consistent set · Model existence for first-order logic · Free variables of an instance · Congruence for function symbols in a maximal consistent set · Henkin axiom · Adding a Henkin axiom preserves consistency · Universal instantiation in maximal consistent sets · Substitution of equals in maximal consistent sets · Derivations survive language homomorphisms · Language homomorphisms commute with instantiation in formulas · Truth lemma for the first-order term model · Replacing an argument of a relation symbol by an equal term · Renaming free variables along an arbitrary map preserves derivability

TheoremInstantiation at the outermost bound variable#✓fully proved

Let \(L\) be a first-order language, \(t\) an \(L\)-term with free variables in \(\alpha\), and \(m\) a natural number. Instantiating \(t\) in the term consisting of the bound variable \(0\) (a term with free variables in \(\alpha\) and \(m + 1\) bound variables) gives \(t\), regarded as a term with free variables in \(\alpha\) and \(m\) bound variables.

@[simp] theorem instantiateTerm_var_zero (t : L.Term α) {m : ℕ} :
    instantiateTerm (m := m) t (Term.var (Sum.inr 0)) = t.relabel Sum.inl

Uses 1

Statement usesInstantiating the outermost bound variable of a term

TheoremInstantiation shifts the remaining bound variables down#✓fully proved

Let \(L\) be a first-order language, \(t\) an \(L\)-term with free variables in \(\alpha\), and \(i < m\). Instantiating \(t\) in the term consisting of the bound variable \(i + 1\) (a term with free variables in \(\alpha\) and \(m + 1\) bound variables) gives the term consisting of the bound variable \(i\) (with \(m\) bound variables).

@[simp] theorem instantiateTerm_var_succ (t : L.Term α) {m : ℕ} (i : Fin m) :
    instantiateTerm t (Term.var (Sum.inr i.succ)) = Term.var (Sum.inr i)

Uses 1

Statement usesInstantiating the outermost bound variable of a term

TheoremInstantiation commutes with the universal quantifier#✓fully proved

Let \(L\) be a first-order language, \(t\) an \(L\)-term with free variables in \(\alpha\), and \(\varphi\) a bounded \(L\)-formula with free variables in \(\alpha\) and \(m + 2\) bound variables. Instantiating \(t\) in the universal formula \(\forall \varphi\) (which has \(m + 1\) bound variables) gives the universal quantification of the instantiation of \(t\) in \(\varphi\).

Under a quantifier the outermost bound variable is still index \(0\) (bound variables are de Bruijn levels), so instantiation passes through the quantifier unchanged.

@[simp] theorem instantiate_all (t : L.Term α) {m : ℕ} (φ : L.BoundedFormula α (m + 1 + 1)) :
    instantiate t φ.all = (instantiate t φ).all

Uses 2 · Used by 1

Statement usesInstantiating the outermost bound variable of a formula

Proof usesInstantiating the outermost bound variable of a term

Used byLanguage homomorphisms commute with instantiation in formulas

TheoremTruth of an instance#✓fully proved

Let \(L\) be a first-order language, \(M\) an \(L\)-structure, \(v : \alpha \to M\) an assignment of the free variables, \(t\) an \(L\)-term with free variables in \(\alpha\), and \(\varphi\) a bounded \(L\)-formula with free variables in \(\alpha\) and one bound variable. Then the instantiation of \(t\) in \(\varphi\), a formula with free variables in \(\alpha\), holds in \(M\) under \(v\) if and only if \(\varphi\) holds in \(M\) under \(v\) with its bound variable set to the value of \(t\) under \(v\).

theorem realize_instantiate_formula (t : L.Term α) (φ : L.BoundedFormula α 1) (v : α → M) :
    Formula.Realize (instantiate t φ) v ↔ φ.Realize v fun _ ↦ t.realize v

Uses 2 · Used by 2

Statement usesInstantiating the outermost bound variable of a formula

Proof usesInstantiating the outermost bound variable of a term

Used bySoundness of first-order natural deduction · Truth lemma for the first-order term model

TheoremTruth of a universal formula#✓fully proved

Let \(L\) be a first-order language, \(M\) an \(L\)-structure, \(v : \alpha \to M\) an assignment of the free variables, and \(\varphi\) a bounded \(L\)-formula with free variables in \(\alpha\) and one bound variable. Then the formula \(\forall \varphi\) holds in \(M\) under \(v\) if and only if, for every \(a \in M\), \(\varphi\) holds in \(M\) under \(v\) with its bound variable set to \(a\).

theorem realize_all_formula (φ : L.BoundedFormula α 1) (v : α → M) :
    Formula.Realize φ.all v ↔ ∀ a : M, φ.Realize v fun _ ↦ a

Used by 2

Used bySoundness of first-order natural deduction · Truth lemma for the first-order term model

TheoremTruth depends only on the free variables#✓fully proved

Let \(L\) be a first-order language, \(M\) an \(L\)-structure, and \(\varphi\) a bounded \(L\)-formula with free variables in \(\alpha\) and \(n\) bound variables. If two assignments \(v, v' : \alpha \to M\) agree on every free variable of \(\varphi\), then for every choice of values in \(M\) for the \(n\) bound variables, \(\varphi\) holds in \(M\) under \(v\) and these values if and only if it holds under \(v'\) and these values.

theorem realize_congr [DecidableEq α] {n : ℕ} {φ : L.BoundedFormula α n} {v v' : α → M}
    (h : ∀ a ∈ φ.freeVarFinset, v a = v' a) (xs : Fin n → M) :
    φ.Realize v xs ↔ φ.Realize v' xs

Used by 1

Used bySoundness of first-order natural deduction

DefinitionRenaming free variables of a term#✓fully proved

Given a map \(f : \alpha \to \beta\) and \(n \in \mathbb{N}\), a term of a first-order language over the variables \(\alpha \sqcup \mathrm{Fin}\,n\) (free variables from \(\alpha\), bound variables from \(\mathrm{Fin}\,n\)) becomes a term over \(\beta \sqcup \mathrm{Fin}\,n\) by replacing each free variable \(a\) with \(f(a)\) and leaving the bound variables unchanged.

def renameTerm (f : α → β) {n : ℕ} (t : L.Term (α ⊕ Fin n)) : L.Term (β ⊕ Fin n) :=
  t.relabel (Sum.map f id)

Used by 9

Used byWeakening · Injective renaming preserves derivability · Free variables of a renamed formula · Truth of a renamed formula · Renaming free variables of a formula · Renaming that fixes the free variables · Doubling the variables preserves consistency · Renaming free variables along an arbitrary map preserves derivability · Renaming depends only on the free variables

DefinitionRenaming free variables of a formula#✓fully proved

Given a map \(f : \alpha \to \beta\), a bounded formula \(\varphi\) of a first-order language \(L\) with free variables in \(\alpha\) and \(n\) bound variables becomes a bounded formula of \(L\) with free variables in \(\beta\) and the same \(n\) bound variables, by replacing each free variable \(a\) with \(f(a)\) in every term of \(\varphi\) and leaving the bound variables, the relation symbols and the logical connectives and quantifiers unchanged.

def rename (f : α → β) {n : ℕ} (φ : L.BoundedFormula α n) : L.BoundedFormula β n :=
  φ.mapTermRel (fun _ ↦ renameTerm f) (fun _ ↦ id) fun _ ↦ id

Uses 1 · Used by 12

Statement usesRenaming free variables of a term

Used byWeakening · Injective relabeling preserves derivability · Injective renaming preserves derivability · Relabelling a formula is renaming · Free variables of a renamed formula · Truth of a renamed formula · Relabeling along \(f\) agrees with renaming · Renaming that fixes the free variables · Model existence for first-order logic · Doubling the variables preserves consistency · Renaming free variables along an arbitrary map preserves derivability · Renaming depends only on the free variables

TheoremTruth of a renamed formula#✓fully proved

Let \(M\) be a structure for a first-order language \(L\), let \(f : \alpha \to \beta\), and let \(\varphi\) be a bounded formula of \(L\) with free variables in \(\alpha\) and \(n\) bound variables. For every assignment \(v : \beta \to M\) of the free variables and every assignment \(x : \mathrm{Fin}\,n \to M\) of the bound variables, the renaming of \(\varphi\) along \(f\) holds in \(M\) at \(v\) and \(x\) if and only if \(\varphi\) holds in \(M\) at \(v \circ f\) and \(x\).

theorem realize_rename {M : Type*} [L.Structure M] (f : α → β) {n : ℕ}
    (φ : L.BoundedFormula α n) (v : β → M) (xs : Fin n → M) :
    (rename f φ).Realize v xs ↔ φ.Realize (v ∘ f) xs

Uses 2

Statement usesRenaming free variables of a formula

Proof usesRenaming free variables of a term

TheoremRelabeling along \(f\) agrees with renaming#✓fully proved

Let \(f : \alpha \to \beta\) and let \(\varphi\) be a bounded formula of a first-order language with free variables in \(\alpha\) and \(k\) bound variables. Mathlib's relabeling of \(\varphi\) along the map \(\alpha \to \beta \sqcup \mathrm{Fin}\,0\) sending \(a\) to the free variable \(f(a)\) replaces each free variable \(a\) by \(f(a)\) and produces a formula with \(0 + k\) bound variables. This formula equals the renaming of \(\varphi\) along \(f\), regarded as a formula with \(0 + k\) bound variables through the inclusion \(k \le 0 + k\).

theorem relabel_inl_comp_eq_castLE_rename (f : α → β) {k : ℕ} (φ : L.BoundedFormula α k) :
    φ.relabel (Sum.inl ∘ f : α → β ⊕ Fin 0) = (rename f φ).castLE (Nat.zero_add k).ge

Uses 1 · Used by 1

Statement usesRenaming free variables of a formula

Used byRelabelling a formula is renaming

TheoremRelabelling a formula is renaming#✓fully proved

Let \(L\) be a first-order language and \(f : \alpha \to \beta\) a map. For every \(L\)-formula \(\varphi\) with free variables in \(\alpha\) (a bounded formula with no bound variables), Mathlib's relabelling of \(\varphi\) along \(f\) equals the renaming of the free variables of \(\varphi\) along \(f\).

theorem formula_relabel_eq_rename (f : α → β) (φ : L.Formula α) : φ.relabel f = rename f φ

Uses 2 · Used by 4

Statement usesRenaming free variables of a formula

Proof usesRelabeling along \(f\) agrees with renaming

Used byInjective relabeling preserves derivability · Model existence for first-order logic · Doubling the variables preserves consistency · Renaming free variables along an arbitrary map preserves derivability

TheoremRenaming that fixes the free variables#✓fully proved

If a map \(f : \alpha \to \alpha\) fixes every free variable of a bounded formula \(\varphi\), then renaming the free variables of \(\varphi\) along \(f\) leaves \(\varphi\) unchanged.

theorem rename_congr {f : α → α} {n : ℕ} {φ : L.BoundedFormula α n}
    (h : ∀ a ∈ φ.freeVarFinset, f a = a) : rename f φ = φ

Uses 2 · Used by 2

Statement usesRenaming free variables of a formula

Proof usesRenaming free variables of a term

Used byWeakening · Doubling the variables preserves consistency

TheoremFree variables of a renamed formula#✓fully proved

Let \(L\) be a first-order language and \(f : \alpha \to \beta\) a map. For every bounded \(L\)-formula \(\varphi\) with free variables in \(\alpha\) and \(n\) bound variables, the set of free variables of the renaming of \(\varphi\) along \(f\) is the image under \(f\) of the set of free variables of \(\varphi\).

theorem freeVarFinset_rename (f : α → β) {n : ℕ} (φ : L.BoundedFormula α n) :
    (rename f φ).freeVarFinset = φ.freeVarFinset.image f

Uses 2 · Used by 2

Statement usesRenaming free variables of a formula

Proof usesRenaming free variables of a term

Used byInjective renaming preserves derivability · Model existence for first-order logic

19 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.