Structures

A structure gives the frame for interpreting first-order formulas.

Given a signature $\mathcal S$, an $\mathcal S$-structure is something which gives meaning to all the symbol in the signature and provides a domain for quantification.

Example Let $\mathcal S = \{\text{zero}, \text{one}, \text{add}/\!/2, \text{mult}/\!/2, \text{Lt}/2\}$. Then a possible and natural way to give meaning to the symbols is to stipulate that

• the objects considered are natural numbers,
• $\text{zero}$ and $\text{one}$ are interpreted by $0$ and $1$, respectively,
• $\text{add}$ and $\text{mult}$ are interpreted by the operations $+$ and $\times$, as defined on the natural numbers, and
• $\text{Lt}$ is interpreted by the natural "less-than" relation on the natural numbers.

Formal definition

Let $\mathcal S$ be an arbitrary signature. An $\mathcal S$-structure $\mathcal A$ consists of

• a universe $A$, which is a non-empty set,
• for every constant symbol $c \in \mathcal S$ an interpretation $c^\mathcal A \in A$ of $c$,
• for every function symbol $f/\!/n \in \mathcal S$ an interpretation $f^\mathcal A \colon A^n \to A$, and
• for every relation symbol $R/n \in \mathcal S$ an interpretation $R^\mathcal A \subseteq A^n$.

Example The above example describes the $\mathcal S$-structure $\mathcal N$ given by: \begin{align} N & = \mathbf N \\ \text{zero}^\mathcal N & = 0\\ \text{one}^\mathcal N & = 1\\ \text{add}^\mathcal N & = {+}\\ \text{mult}^\mathcal N & = {\times}\\ \text{Lt}^\mathcal N & = {<} \end{align} The symbols $+$, $\times$, and $<$ denote the usual operations on the natural numbers.

Example A perfectly valid $\mathcal S$-structure $\mathcal A$ is given by: \begin{align} A & = \{0, 1, 2, 3\} \\ \text{zero}^\mathcal A & = 3\\ \text{one}^\mathcal A & = 2\\ \text{add}^\mathcal A(a,b) & = 0 && \text{for $a, b \in A$}\\ \text{mult}^\mathcal A(a,b) & = a + b \text{ rem } 4 && \text{for $a, b \in A$}\\ \text{Lt}^\mathcal N & = \{\langle a, a\rangle \colon a \in A\} \end{align} The function $\text{rem}$ is the remainder function.

Term structures

There is a simple way to define structures over a given signature: every term without free variables over the given signature stands for itself and relation symbols are interpreted arbitrarily.

Given a signature $\mathcal S$, we call the set of all possible $\mathcal S$-terms without free variables, a ground term. So ground terms are terms that only consists of function and constant symbols.

Definition Let $\mathcal S$ be a signature with at least one constant symbol. A term structure over $\mathcal S$, also called $\mathcal S$-term structure, is an $\mathcal S$-structure $\mathcal T$ such that

• $T$ is the set of $\mathcal S$-ground terms,
• $c^\mathcal T = c$ for every $c \in C$, and
• $f^\mathcal T(t_0, \dots, t_{n-1}) = f(t_0, \dots, t_{n-1})$ for every $f/\!/n \in \mathcal F$ and $\mathcal S$-ground terms $t_0, \dots, t_{n-1}$.

Example Let $\mathcal S = \{\text{zero}, \text{succ}/\!/1\}$. Then there is exactly one $\mathcal S$-term structure. Its elements are $\text{zero}, \text{succ}(\text{zero}), \text{succ}(\text{succ}(\text{zero})), \dots$.

The condition that there need to be constant symbols in the signature is a necessary and sufficient condition for the existence of ground terms.

Commonly used structures

There is a list of commonly used structures.