First-order language

A first-order language specifies its constant, operation, and relation symbols, together with the arity of each nonconstant symbol.

Replace an $n$-ary function by an $(n+1)$-ary graph predicate asserted to have exactly one output for each input tuple. A constant can be replaced by a unary predicate selecting one element. Term-value formulas in relational coding translate arbitrary terms, and formulas translate recursively through the logical operations. The original structures correspond bijectively to relational structures satisfying the graph axioms on the same carrier. Truth and consequences are preserved; arbitrary relations not satisfying those axioms do not represent functions.

A predicate symbol of arity $k$ is interpreted as a subset of the $k$th Cartesian power of a structure's domain. Applying it to $k$ first-order terms gives an atomic formula. In a singleton domain there is only one possible argument tuple at each arity, but a predicate may still be interpreted as either the empty relation or the full relation.

A function symbol is part of the syntax of a first-order language, with a specified finite arity. In a first-order structure it is interpreted as a function from the corresponding finite power of the domain into the domain. Applying it to the appropriate number of first-order terms forms another term. The symbol itself is distinguished from its interpretation in a particular structure.

A constant symbol is a zero-ary function symbol. Its interpretation in a first-order structure names one fixed domain element, and the symbol is a closed term. A language can contain no constant symbols unless a construction explicitly adds them.

A signature specifies the sorts, operation symbols with their input and output sorts, and relation symbols with their input sorts. The logical connectives and quantifiers are supplied separately by the chosen logic. This separates the nonlogical vocabulary from the rules defining a coherent theory.

For coding arithmetic computations, the signature in use is $0,1,+,\times ,<,=$. Bounded remainder tests and polynomial equations use only these symbols. This is a statement about the language: interpretation in the natural numbers does not impose the axioms of a ring.

A first-order term is built recursively from variables and constant symbols by applying function symbols to existing terms. Evaluation in a first-order structure follows the same recursion. An atomic formula applies a relation to terms, or asserts their logical equality.

A first-order structure and an assignment determine the value of every term recursively: a variable has its assigned value, a constant has its interpreted value, and a compound function term is evaluated by applying the interpreted function to the recursively evaluated arguments. This operation supplies the input values for the satisfaction clauses of atomic formulas.

After replacing functions by graph predicates and constants by singleton predicates, $E_t(z)$ says that $z$ is the value of a term $t$. For a unary function graph $P$ and constant predicate $Q$, use $E_x(z)=(z=x)$, $E_c(z)=Q(z)$ and $E_{f(t)}(z)=\exists y(E_t(y)\wedge P(y,z))$. Fresh witnesses avoid variable capture. Totality and uniqueness axioms make each value formula have exactly one witness under every assignment.

A closed term contains no variables, so its value in a first-order structure does not depend on an assignment. In a language containing only relations and the constant zero, zero is the only closed term. A term-generated model has every element denoted by such a term.

A first-order term containing no variables. Constant symbols are ground terms; applying a function symbol to ground terms produces another ground term.

A finite set of formulas mentions only finitely many nonlogical symbols. This observation lets compactness reduce arguments in a language indexed by a large set to a finite sublanguage.