# Structures

### From Learning Logic for Computer Science

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.