Practical Foundations of Mathematics

Paul Taylor

6.2  Well Formed Formulae

In practice, additional side-conditions 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 operation-symbol, 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 wff-system 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 sub-terms, 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 l-terms are hereditarily l[(x)\vec].y[(u)\vec] ( ie each sub-term \termu_j is also normal, and of this form). We can regard this as a (finer) notion of well-formedness, 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 l-calculus 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 wff-system X (``syntax,'' with a well founded ``sub-expression'' 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.)

EXAMPLES 6.2.3

(a)

To solve Rubik's cube (Example 4.2.3) we must find a list of moves which restores a semantically given position to the home one. We need to split the surjection F = List(6) \twoheadrightarrow A, where A is the group.

(b)

The reflexive-transitive closure £ of a relation < is a subquotient of List( < ) (Exercise  3.60).

(c)

The finite powerset P_f(X) is a quotient of List(X) (Definition 6.6.9).

(d)

Let A be the free algebra for a finitary theory L and F the free algebra for the free theory which consists of the operation- symbols of L alone, forgetting the sorts and laws. We construct A in Section 7.4 as the quotient by the laws of the subset X Ì F of terms obeying the type discipline.

(e)

Let W be the rules of logic. The class Q of formulae is an W-algebra, of which the class A Ì Q of formulae true in some class of models is a subalgebra ( cf Remark  3.7.7 and Example  6.1.9). The free algebra F consists of proofs and the homomorphism F\rightharpoonup Q sends each proof to its conclusion. If F\twoheadrightarrow A then all true formulae are provable.

(f)

Let C be a cartesian closed category (Section  4.7) and Q = mor C. Let F be the class of raw l-terms in the canonical language of C (Section 7.6) and p:F \rightharpoonup Q the interpretation function. Its image A Ì Q is the class of l-definable functions.

(g)

The same, where F is the class of normal l-terms.

(h)

PERs (Exercise 5.10).

(i)

(Lothar Collatz, 1930s) Let f:N® N by

f(n) = omitted casearray environment

it is an open problem whether "n.$m.f^m(n) = 1.

Putting a(m) = 2m and b(m) = (2m-1)/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, operation-symbols 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:

(a)

Example 2.7.6(e) tests whether the name x is in the list G;

(b)

Exercise 6.50 chooses new names from a population G, providing the inexhaustible supply of variables needed for substitution under a l (Definition  1.1.9ff);

(c)

Simple type theory (Section 2.3) is the free algebra S for the theory with three operation-symbols (x, + and ® ) over the base types.

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 l-calculus 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 operation-symbols and generators.

Many-sorted theories   The type discipline is obeyed (globally) iff the (local) side-conditions on the formation of each operation-symbol 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 operation-symbols 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 Many-sorted 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 wff-system.

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 operation-symbol 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).

THEOREM 6.2.8

(a)

Every directed graph src,tgt:E \rightrightarrows O generates a free category.

(b)

Let C be any internal category and |C| its underlying graph. Then the internal graph homomorphism \qqdash names objects and arrows of C as types and unary operation-symbols of L(|C|), and hence as objects and arrows of \Clone_L(|C|). Conversely, the internal functor [[-]] interprets types and terms of L(|C |) back in C.

\CloneL(|C|) \twoheadrightarrow        p º [[-]]       \lInto \qqdash |C|