Term (First-Order Logic)

first-order-logic

Definition

Term (First-Order Logic)

Let $(\mathcal{F},\mathcal{P})$ be a signature and $\mathcal{V}$ a set of variables. The set of terms over $(\mathcal{F},\mathcal{P})$ is defined inductively:

$$\begin{array}{rl}x\in \mathcal{V}& :x\text{ is a term}\\ f\in \mathcal{F},\mathrm{ar}(f)=0& :f\text{ is a term}\\ f\in \mathcal{F},\mathrm{ar}(f)=n>0,t_1,\dots ,t_n\text{ terms}& :f(t_1,\dots ,t_n)\text{ is a term}\end{array}$$

A function symbol of arity $0$ is a constant.

Interpretation

Under an interpretation $(\mathcal{M},\ell )$, a term $t$ is evaluated to an element $t^{(\mathcal{M},\ell )}$ of the domain:

$$\begin{array}{rl}t=x\in \mathcal{V}& :t^{(\mathcal{M},\ell )}=\ell (x)\\ t=f(t_1,\dots ,t_n)& :t^{(\mathcal{M},\ell )}=f^{\mathcal{M}}\left(t_1^{(\mathcal{M},\ell )},\dots ,t_n^{(\mathcal{M},\ell )}\right)\end{array}$$