Definition:Language of Predicate Logic/Formal Grammar/Term

From ProofWiki
Jump to navigation Jump to search

This page is about terms in the development of predicate logic. For other uses, see Definition:Term.


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

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

\((\mathbf T \ \textrm {VAR})\)   $:$   Any variable of $\mathcal L_1$ is a term;             
\((\mathbf T \ \mathcal F_n)\)   $:$   Given an $n$-ary function symbol $f \in \mathcal F_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.