This web page puts a little more detail on
the syntactical nature of the definition of
the set of boolean terms over letters from ,
given in Chapter 6 of The Mathematics of Logic
.
We also give the unique readability theorem for such terms
and explain how definitions by induction can be made on
terms. Much of the material here consists of very precise
(almost pedantic) constructions concerning strings of
symbols, and the theorems proved here about them are
in some sense obvious
. The material here is aimed at
readers who really need or want to see the full story with
all the gory details.
In Definition 6.1 the set is defined. The essential ingredients of this definition are that
letterssuch as .) In the sequel we will always assume that this is the case.
Here then is the full definition of , making Definition 6.1 more precise.
Definition.
A string of symbols is in if there is a finite sequence of strings of symbols, such that is the string and for each we have one of the following holding.
Definition.
A finite sequence of strings of symbols such that for each one of the six conditions above hold is called a construction sequence for the boolean term .
Exercise.
Rewrite the above definitions so that it is given by a formal system (which you must specify), a boolean term over is a theorem of the system, and a construction sequence is essentially a proof in the formal system.
All syntactical definitions by induction in the book can be re-written more precisely in this sort of form, expressing the existence of a finite sequence of subexpressions, or by introducing other secondary formal systems.
We can use this formal definition now to prove statements that might have seemed obvious but nevertheless deserve a proof in a highly rigorous treatment.
Example.
Each construction sequence of length consists of a single string of a single symbol. That symbol may be , , or an element of .
Proposition.
Each is a string of finitely many symbols.
Proof.
By induction.
Subproof.
Our induction hypothesis is the statement that if is a construction sequence then is a string of finitely many symbols.
is true by the preceding example. If we could prove for all then we would have proved the proposition for if there is a construction sequence for it of some length si by there are finitely many symbols in .
The induction step, saying that if holds for all then holds, is proved by looking at the six individual clauses in the definition of construction sequence. Note that if is a construction sequence then for each , is also a construction sequence. So by for we may assume that each is finite. It follows by looking at the individual clauses that must be finite too.
Unique readability is the proposition that we chose a good method for encoding terms as strings. For example if we had omitted the brackets, writing instead as , and also writing instead as the encoding we would have would not satisfy unique readability as could be variously read as , , , , etc.
Thus unique readability is a theorem about correctness of encodings of a natural mathematical idea (terms and expressions) into the realm of strings of symbols. Most of the work is done by the following technical proposition.
Proposition.
Suppose and are boolean terms over a set and that is an initial part of , that is is the concatenation for some string . Then in fact and have the same length and are equal as strings.
Proof.
By induction on the length of construction sequences. We assume we are given with the property that whenever and are boolean terms over a set both with construction sequences of length at most and is an initial part of then . Observe that this is true when since in this case both and are , , or an element of , and so if is an initial part of and both have length then .
For the induction step we suppose we have that is an initial part of both having construction sequences of length at most . We look at the first symbol in , which is also, necessarily the first symbol in .
If this symbol is , or then both and are one-symbol strings, as the only clauses in the construction allowing these as the first symbol are the first three, and these construct single symbol strings. Thus in this case.
If the first symbol in is then for some with construction sequence of length at most as this is the only possible construction clause. Similarly for some with construction sequence of length at most . Also as is an initial part of , is also an initial part of , so by our induction hypothesis and hence .
If the first symbol in is an open parenthesis then there are two possibilities: either is or is . Similarly is where is or . This means that is an initial part of the string and hence either is an initial part of the string or is an initial part of the string . Therefore by our induction hypothesis . Now by looking at the rest of and how it is an initial part of we see that the operator is the same as the operator of alpha, i.e. is which is an initial part of . So is an initial part of and hence by the induction hypothesis they are equal. This shows .
Proposition.
Suppose . Then exactly one of the following holds.
Moreover, in the last three cases, the strings are uniquely determined from .
Proof.
Case-by-case, using the previous proposition.
The importance of unique readability is that it enables new definitions by induction on the way a boolean term is built up. One hugely important example of such a definition is given in chapter 7, page 80 where a valuation, a function is extended to a function . If a boolean term could be ambiguously read in two or more different ways, the definition given would not be sound and the whole theory collapse.
Exercise.
Let be a first order language. Assume that the symbols of , especially the variables, constant symbols, function symbols and relation symbols are all distinct. State and prove a unique readability theorem for terms of .
Exercise.
With as in the previous exercise, state and prove a unique readability theorem for formulas of .