Functions Expressing generality
One of the most important properties that a relation R may have is that of being manyone. This means that for any object x from the domain of discourse there is at most one thing y such that Rxy. A manyone relation is sometimes also said to be functional. If R is both manyone and connected, then for any x there is exactly one y such that Rxy, which is to say that there exists such a thing as the Rrelative of x.
First order logic already has the resources to represent the logic of relations, and we can in principle sprinkle extra assertions about their functionality over arguments as needed, but this is cumbersome and tends to obscure rather than clarify the reasoning. Rather than write complicated and tedious quantified formulae everywhere, we shall follow standard practice and introduce function symbols into our formal language, and refer to the associated manyone relations as functions. A kary relation which is manyone with respect to its last argument place (that is, for any x_{1},...,x_{k−1} there exists at most one y such that Rx_{1},...,x_{k−1},y) is a k−1ary function, taking k−1 things as its arguments and delivering (at most) one thing as its value for those arguments. If for all arguments there is exactly one value, then the function is said to be total; otherwise (if it may have no value for certain arguments) it is partial.
Examples of unary (or monadic) functions: 'the father of...' in the domain of people; 'the successor of...' in the domain of whole numbers. Examples of binary (dyadic) functions: the standard operators of basic arithmetic, 'plus', 'minus', 'times', etc. In mathematics, of course, functions are everywhere. If you have used Logic for Fun to formalise problems in first order logic, you will know that functions are everywhere else as well. It is therefore very important that our logical system should have the resources to handle them properly.
We shall use lowercase letters, usually f, g, etc., as function symbols in our formal language. Following the same conventions as Logic for Fun, we shall write the arguments as a commaseparated list enclosed in parentheses, after the function symbol. Of course, where a binary function symbol like '+' is more familiar in infix position (between its arguments) we shall allow ourselves the freedom to write it in the usual way.
Having function symbols in the language, we have to complicate the syntax a little. A referring expression will now be called a term. Names can be recast as 0ary function symbols, since they do what function symbols do (refer to an object) but they do it without needing to be supplied with arguments. The set of terms may therefore be defined as the smallest set such that each term in it is an nary function symbol (for some n, zero or more) applied to n terms. The definition is not circular, since the inner terms (the ones to which the function symbol is applied) have to be provably terms by means of the definition, so they have to be shorter and simpler. Eventually, all terms have to start from function symbols without arguments, otherwise known as names. To illustrate, if a is a name (nullary function symbol), f a unary function symbol and g a binary one, then the following are terms:
a
f(a)
g(a,f(a))
g((g(a,f(a)),a)
Our notion of substitution of variables for names (and names for variables) in formulae also has to be extended to allow substitution for terms, and substitution of one term for another. The rules ALLE and SOMEI have to be amended slightly to allow for terms of arbitrary complexity in place of just names.^{1} Thus ALLE, for instance, allows the inference from ALLv A to A^{t}_{v}where the latter is the result of substituting the term t for the variable v. This makes sense: if A is true of everything then it is true in particular of whatever the term t picks out, however complex t may be. The rules ALLI and SOMEE, however, require arbitrary names in their premises, and the role of these names cannot in general be played by compound terms.


: Proof with function symbols Try it yourself 

fProof shows the amended rules in use. Notice that at line (5) we use ALLE substituting the compound term f(a) for the variable in line (1), but that the last line requires the term in line (7) to be a name rather than a compound.
Note that terms may substitute for subterms deep inside other terms. Substitution into terms is especially important in the case of equational reasoning (using the rule =E, to be introduced below) which allows substitution of equals for equals in arbitrary contexts. This form of reasoning is used everywhere in elementary mathematics to transform terms by rewriting them according to equations.
With function symbols in our language, we are able to formulate a great many interesting first order theories including arithmetic. Since numerals (0 , 1 , 2 ... ) are just names, while 'successor', 'plus' and 'times' are straightforward function symbols of one, two and two arguments respectively, the first order theory of arithmetic is reasonably simple to set up. Historically, the development of symbolic logic from the mid19th century on was partly driven by the need to provide rigorous foundations for mathematics, so it is very important that the language of logic should be sufficient to express such concepts.


^{2} The rules =I and =E governing the identity predicate (see below) also apply to general terms, not just to names. 