σ-formulas. Each σ-formula is built up out of atomic formulas by means of logical connectives; atomic formulas are built from terms using predicate symbols. The formal definition of the set of σ-formulas proceeds in the other direction: first, terms are assembled from the constant and function symbols together with the variables. Then, terms can be combined into an atomic formula using a predicate symbol (relation symbol) from the signature or the special predicate symbol "=" for equality (see the section "Interpreting equality" below). Finally, the formulas of the language are assembled from atomic formulas using the logical connectives and quantifiers. Interpretations of a first-order language To ascribe meaning to all sentences of a first-order language, the following information is needed. A domain of discourse D, usually required to be non-empty (see below). For every constant symbol, an element of D as its interpretation. For every n-ary function symbol, an n-ary function from D to D as its interpretation (that is, a function Dn → D). For every n-ary predicate symbol, an n-ary relation on D as its interpretation (that is, a subset of Dn). An object carrying this information is known as a structure ( signature σ), or σ-structure, or L-structure (of language L), or as a "model". The information specified in the interpretation provides enough information to give a truth value to any atomic formula, after each of its free variables, if any, has been replaced by an element of the domain. The truth value of an arbitrary sentence is then defined inductively using the T-schema, which is a definition of first-order semantics developed by Alfred Tarski. The T-schema interprets the logical connectives using truth tables, as discussed above. Thus, for example, is satisfied if and only if both φ and ψ are satisfied. This leaves the issue of how to interpret formulas of the form and . The domain of discourse forms the range for these quantifiers. The idea is that the sentence is true under an interpretation exactly when every substitution instance of φ(x), where x is replaced by some element of the domain, is satisfied. The formula is satisfied if there is at least one element d of the domain such that φ(d) is satisfied. Strictly speaking, a substitution instance such as the formula φ(d) mentioned above is not a formula in the original formal language of φ, because d is an element of the domain.