Unlike propositional logic, where every language is the same apart from a choice of a different set of propositional variables, there are many different first-order languages. Each first-order language is defined by a
signature. The signature consists of a set of non-logical symbols and an identification of each of these symbols as either a constant symbol, a function symbol, or a
predicate symbol. In the case of function and predicate symbols, a
natural number arity is also assigned. The alphabet for the formal language consists of logical constants, the equality relation symbol =, all the symbols from the signature, and an additional infinite set of symbols known as variables. For example, in the language of
rings, there are constant symbols 0 and 1, two binary function symbols + and ·, and no binary relation symbols. (Here the equality relation is taken as a logical constant.) Again, we might define a first-order language
L, as consisting of individual symbols a, b, and c; predicate symbols F, G, H, I and J; variables x, y, z; no function letters; no sentential symbols.
Formal languages for first-order logic Given a signature σ, the corresponding formal language is known as the set of σ-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. There are two ways of handling this technical issue. The first is to pass to a larger language in which each element of the domain is named by a constant symbol. The second is to add to the interpretation a function that assigns each variable to an element of the domain. Then the T-schema can quantify over variations of the original interpretation in which this variable assignment function is changed, instead of quantifying over substitution instances. Some authors also admit
propositional variables in first-order logic, which must then also be interpreted. A propositional variable can stand on its own as an atomic formula. The interpretation of a propositional variable is one of the two truth values
true and
false. Because the first-order interpretations described here are defined in
set theory, they do not associate each predicate symbol with a property (or relation), but rather with the extension of that property (or relation). In other words, these first-order interpretations are
extensional not
intensional.
Example of a first-order interpretation An example of interpretation \mathcal{I} of the language
L described above is as follows. • Domain: A chess set • Individual constants: a: The white King, b: The black Queen, c: The white King's pawn • F(x): x is a piece • G(x): x is a pawn • H(x): x is black • I(x): x is white • J(x, y): x can capture y In the interpretation \mathcal{I} of L: • the following are true sentences: F(a), G(c), H(b), I(a), J(b, c), • the following are false sentences: J(a, c), G(a).
Non-empty domain requirement As stated above, a first-order interpretation is usually required to specify a nonempty set as the domain of discourse. The reason for this requirement is to guarantee that equivalences such as (\phi \lor \exists x \psi) \leftrightarrow \exists x (\phi \lor \psi), where
x is not a free variable of φ, are logically valid. This equivalence holds in every interpretation with a nonempty domain, but does not always hold when empty domains are permitted. For example, the equivalence [\forall y (y = y) \lor \exists x ( x = x)] \equiv \exists x [ \forall y ( y = y) \lor x = x] fails in any structure with an empty domain. Thus the proof theory of first-order logic becomes more complicated when empty structures are permitted. However, the gain in allowing them is negligible, as both the intended interpretations and the interesting interpretations of the theories people study have non-empty domains. Empty relations do not cause any problem for first-order interpretations, because there is no similar notion of passing a relation symbol across a logical connective, enlarging its scope in the process. Thus it is acceptable for relation symbols to be interpreted as being identically false. However, the interpretation of a function symbol must always assign a well-defined and total function to the symbol.
Interpreting equality The equality relation is often treated specially in first order logic and other predicate logics. There are two general approaches. The first approach is to treat equality as no different than any other binary relation. In this case, if an equality symbol is included in the signature, it is usually necessary to add various axioms about equality to axiom systems (for example, the substitution axiom saying that if
a =
b and
R(
a) holds then
R(
b) holds as well). This approach to equality is most useful when studying signatures that do not include the equality relation, such as the signature for
set theory or the signature for
second-order arithmetic in which there is only an equality relation for numbers, but not an equality relation for set of numbers. The second approach is to treat the equality relation symbol as a logical constant that must be interpreted by the real equality relation in any interpretation. An interpretation that interprets equality this way is known as a
normal model, so this second approach is the same as only studying interpretations that happen to be normal models. The advantage of this approach is that the axioms related to equality are automatically satisfied by every normal model, and so they do not need to be explicitly included in first-order theories when equality is treated this way. This second approach is sometimes called
first order logic with equality, but many authors adopt it for the general study of first-order logic without comment. There are a few other reasons to restrict study of first-order logic to normal models. First, it is known that any first-order interpretation in which equality is interpreted by an
equivalence relation and satisfies the substitution axioms for equality can be cut down to an
elementarily equivalent interpretation on a subset of the original domain. Thus there is little additional generality in studying non-normal models. Second, if non-normal models are considered, then every consistent theory has an infinite model; this affects the statements of results such as the
Löwenheim–Skolem theorem, which are usually stated under the assumption that only normal models are considered.
Many-sorted first-order logic A generalization of first order logic considers languages with more than one
sort of variables. The idea is different sorts of variables represent different types of objects. Every sort of variable can be quantified; thus an interpretation for a many-sorted language has a separate domain for each of the sorts of variables to range over (there is an infinite collection of variables of each of the different sorts). Function and relation symbols, in addition to having arities, are specified so that each of their arguments must come from a certain sort. One example of many-sorted logic is for planar
Euclidean geometry. There are two sorts; points and lines. There is an equality relation symbol for points, an equality relation symbol for lines, and a binary incidence relation
E which takes one point variable and one line variable. The intended interpretation of this language has the point variables range over all points on the
Euclidean plane, the line variable range over all lines on the plane, and the incidence relation
E(
p,
l) holds if and only if point
p is on line
l. ==Higher-order predicate logics==