Definition:Language of Predicate Logic/Formal Grammar/Term

This page is about Term in the context of Predicate Logic. For other uses, see Term.

Definition

Part of specifying the language of predicate logic $\LL_1$ is the introduction of terms.

The terms of $\LL_1$ are identified by the following bottom-up grammar:

$(\mathbf T \ \textrm {VAR})$

$:$

Any variable of $\LL_1$ is a term;

$(\mathbf T \ \FF_n)$

$:$

Given an $n$-ary function symbol $f \in \FF_n$ and terms $\tau_1, \ldots, \tau_n$:

$\map f {\tau_1, \ldots, \tau_n}$

is also a term.

Colloquially, we can think of a term as an expression signifying an object.