In practice, additional sideconditions are required of the terms which are to be admitted to the language. Some of these, such as the number of arguments taken by each operationsymbol, can be enforced in advance, but others must be stated by simultaneous recursion together with the expressions themselves. The terms which do satisfy the conditions are traditionally known as wffs ( well formed formulae).
DEFINITION 6.2.1 A wffsystem is a set X of terms for a free theory (W,ar) such that if r([(u)\vec]) Î X then \termu_{j} Î X for all j:ar[r]. Therefore

Nonsense results if instead we admit expressions with ill formed subterms, for example the assertion that `` the unicorn is the author of the Principia'' (page 1.2.11). As with pred(0) (Remark 2.7.9), the cost of trying to make all operations total is a proliferation of exceptions to the rules of inference. These are easily overlooked in complex situations, leading to errors in programs which are extremely hard to track down.
Recursive covers Having enumerated the raw terms (wffs), we impose laws to equate them. When arguing inductively, the ideal situation is that the laws be oriented, ie presented as reduction rules, and these be confluent and strongly normalising. The surjection in Definition 6.2.2 then has a (canonical) splitting, the semantic values being identified with the class of normal forms. This class may itself have a recursive characterisation: for example Exercise 2.23 showed that normal lterms are hereditarily l[(x)\vec].y[(u)\vec] ( ie each subterm \termu_{j} is also normal, and of this form). We can regard this as a (finer) notion of wellformedness, with useful inductive consequences of its own ( eg Remark 7.6.12ff).
Failing this, finitary algebraic theories handle laws using quotients by congruences (Sections 5.6 and 7.4), whilst the properties of adjunctions take care of most of the infinitary theories of interest ( eg Lemma 5.6.14). These methods tend to interact notoriously badly with recursion.
Section 7.6 turns the construction of linguistic structures on its head, in the search for a language which exactly matches a given semantic structure, for example a lcalculus which is equivalent to a given cartesian closed category. New symbols such as \qq X are added to the language for each entity in the semantics, but then terms in the language have equal meanings because this is given in the semantics, rather than because there is a symbolic proof of this fact.
Either way round, the reason for considering raw terms is that they admit structural recursion.
DEFINITION 6.2.2 A recursive cover of a ``semantic'' set A is a wffsystem X (``syntax,'' with a well founded ``subexpression'' relation \prec ), together with a surjective function p:X\twoheadrightarrow A. (Since X Ì F, A is a subquotient of the free algebra F if the latter exists.)

Putting a(m) = 2m and b(m) = (2m1)/3 (defined only when m º 2 mod3), there is a partial function p:List({ a,b})\rightharpoonup N with p([ ]) = 1, p(cons(a, l)) = a(p(l)) and p(cons(b,l)) = b(p(l)). The Collatz problem asks whether p is surjective.
So both in the Collatz problem and in logic, the image of one recursive structure in another may be an intractably intricate maze, cf Gödel's Incompleteness Theorem 9.6.2.
The semantics inherits a weak induction principle from the syntax. (For a stronger result see Exercise 3.54.)
PROPOSITION 6.2.4 Let (X,\prec ) be well founded and let p:X\twoheadrightarrow A be a surjective partial function. Then for predicates f[a],

PROOF: The rule is simply the induction scheme for fop: from "t.f[p(t)] we deduce "a.f[a] by surjectivity. []
Variables At the lowest level of linguistic analysis, we use variables, operationsymbols and punctuation, and it must be decidable whether any two such things are the same. This is obvious for marks on the page or bits in a computer, but the development of Section 6.1 was intended also to apply to internal structures, where the alphabets such as W are themselves types, and to address the issues raised in Theorem 4.2.12.
EXAMPLE 6.2.5 The variable names (or generators, as we call them in this chapter) in a context have to be distinct, so they should come from a population G with decidable equality. Our convention is that they be explicit, but we need some elementary manipulations:
Then ob(Cn^{×}_{L}) Ì List(GxS), where the variables are not repeated. []
In the same fashion we can define the set FV(t) of free variables of a term in algebra, the lcalculus and logic and prove the Extended Substitution Lemma (Proposition 1.1.12). The unification algorithm (Section 6.5) also depends on parsing and the ability to distinguish between operationsymbols and generators.
Manysorted theories The type discipline is obeyed (globally) iff the (local) sideconditions on the formation of each operationsymbol are satisfied hereditarily (Definition 2.5.4). As the type of a term is that of its outermost symbol, the validity of the typing rules may be expressed by a function F® WxS, where S is the class of types. If the operationsymbols have finite arity and are distinguishable from one another, we may instead define F® S+{*} , the extra element being an error value.
PROPOSITION 6.2.6 Manysorted free theories have free models.
PROOF: Let (W,ar) be the corresponding untyped theory and F its free algebra. From the type discipline of Notation 1.3.3,
r([(u)\vec]) Î F is well formed and of sort V iff the operation r has arity Õ_{j Î ar[r]} \typeU_{j}\vdash V and for each j Î ar[r], \termu_{j} is well formed and of sort \typeU_{j}.
Then the carrier \typeF_{U} of the free typed algebra at sort U is the set of well formed terms of sort U. Also X = \coprod_{U}\typeF_{U} Ì F is a wffsystem.
If A is any algebra for the typed theory then Q = \coprod_{U}\typeA_{U} is a partial algebra for the untyped one, and then Theorem 6.3.13 gives the unique solution p:X\rightharpoonup Q of the recursion equation. By induction, if u:F is well formed and of type U then p(u) is defined and p(u) Î \A_{U} Ì Q. []
The notion of type in this result is just accountancy: it need not be semantic. For example it may simply be the number of terms in a list.
EXAMPLE 6.2.7 A word l Î List(W) is a well formed sequence of n terms over a finitary theory ar:W® N if
l = [ ] and n = 0; or l = cons(h,t) where (h is an operationsymbol and) t is a well formed sequence of n+ar[h]1 terms.
Those words which are single terms (n = 1) form the free algebra for the free finitary theory. This way of forming expressions, for example (1+2)x(3+4) is written [x,+,1,2,+,3,4], is called Polish notation; it is due to Jan Lukasiewicz (1920s). It is used by compilers in reversed form ( ie with operations after their arguments) for the evaluation of arithmetic expressions using a stack (Exercise 6.8).
