Definition:Language of Predicate Logic/Formal Grammar/Term

From ProofWiki
Jump to navigation Jump to search

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


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.