Solution (source code)

= Solution

An $L$-structure has a nonempty underlying <set> $A$. It assigns to each <constant symbol> $c_k$ an element $c_k^{\mathcal A}\in A$, to each $n$-ary <function symbol> $f_j$ a <function> $A^n\to A$, and to each $n$-ary <predicate symbol> $P_i$ a relation contained in $A^n$. <Logical equality>, when included as <logical equality>, is interpreted as actual identity.

The arities belong to the specification of the <first-order language>. An assignment of <logical variables> to elements of $A$ then evaluates <first-order terms> recursively and determines satisfaction of <logical formulas> through the <logical connectives> and <quantifiers>. A <first-order sentence> has no <free variables>, so its truth in the <first-order structure> is independent of the assignment.