Section 4.2 proved statements about every natural
number. This section proves statements about every
formula in the same way, and with them answers the
question Section 4.1 left open, whether every formula is
read in only one way, and with it a second: does a
definition with one clause per connective define exactly
one thing? On the way it shows what goes wrong when an
object can be built in two ways.
Structural
induction
We return to formulas. The formation sequence of a
formula plays the part that “” plays for
numbers: every formula is reached from atoms and by finitely many
uses of the clauses. So a property of formulas can be
proved in the same two parts.
A property of formulas is a
statement about a
formula ,
true or false for each particular formula: “ has as many left
as right parentheses”, “ contains the atom
”.
If every atom and has a property, and
each way of building a formula passes the property from
the parts to the whole, then every formula has
it.
Theorem
4.3.1 (Structural Induction)
Let
be a property of formulas. Suppose that
- (i) holds for every atom
, and holds;
- (ii) for
every formula , if holds, then
holds;
- (iii) for
all formulas and
each binary connective , if and hold, then
holds.
Then
holds for every formula .
In words: (i) is the base case, one for each kind of
formula of length one. (ii) and (iii) are the inductive
steps, one for each building clause of Definition 4.1.1,
and inside them “ and ” is the induction
hypothesis, assumed for the immediate
parts of the formula being built. There are
seven cases in all (atoms, , , and the four binary
connectives); often the four binary ones are handled at
once, with
left unspecified.
Section 4.2’s checklist reads: objects, the formulas;
property, , with any
restriction inside it; base cases, every atom and ; steps, one for
and one for
each binary connective; principle, Theorem 4.3.1.
For example, take the property “ has as many left
as right parentheses”. Base cases: an atom and
have no
parentheses, none of either. Step for : if has of each, so has , since is not a
parenthesis. Step for : if has of each and has of each, then has
of each,
the outer pair adding one of each. By Theorem 4.3.1,
every formula has as many left as right parentheses.
This is part (a) of Lemma 4.3.2
below; its other parts need more care.
Idea. Take any formula and a
formation sequence ending in it. Walk along the
sequence: each entry is an atom or , which has the
property by (i), or is built from
earlier entries, which have it already,
by (ii) or (iii). “Earlier entries, any of them” is
exactly the shape of strong induction, applied to the
position in the list.
The property spreads from left to right. Each entry
gets its check mark from (i), or from entries to its
left that already have one.
The proof, in the fold below, makes “from left to
right” exact with strong induction on the position in
the list.
↺Second readingThe
proof of structural induction
Proof. Suppose (i)–(iii) hold, and
let be a
formula. By Definition 4.1.1
(F4) there is a formation sequence
with .
For , let
be the
property “if , then holds”. We
prove for
every by
Theorem 4.2.2.
Let ,
and suppose
holds for every with . If or , then holds vacuously. So
let .
By the definition of a formation sequence, one of three
things is true.
- is an
atom or . Then
holds by
(i).
- for some . Then , and gives . The entry
is a formula
(every entry of a formation sequence is one, Section
4.1), so (ii) applies and gives .
- for some and a binary connective . Then , and
and give and , both entries
are formulas, and (iii) gives .
So holds.
By Theorem 4.2.2,
holds for
every ; in
particular
gives ,
that is, .
Since was an
arbitrary formula, this proves the theorem.
The proof uses strong induction,
because an entry of a formation sequence may be built
from any earlier entries, not only from the one just
before it.
Warning. A structural induction
must cover every clause, the base case
and the step
for included.
Try to prove “every formula contains an atom”: it holds
for atoms, and the steps for and for keep
it, since the atoms of the parts are atoms of the whole.
But the case
fails, and so does the claim: , and contain
no atom. A proof that “forgets” proves something
false.
Quick check. Which clause of Definition 4.1.1
makes step (ii) of Theorem 4.3.1
necessary? Give a property of formulas that holds for
every atom and for , passes from and to for
every binary connective, and yet fails for some
formula.
Solution. Clause (F2), which builds
from
: step (ii)
is the step for that clause. Without it, the formulas
made by (F2) would be missed.
One such property: “ is an atom, or is
, or begins
with ”. Atoms and
have it, and
every formula begins with , whatever its parts
are. But
does not have it. So (i) and (iii) alone do not prove a
property of every formula; the property fails exactly at
a formula made by the forgotten clause.
↺Second readingSets
built from a base
Section 4.1 called the formulas the
smallest collection of strings closed
under (F1)–(F3). Here is that sentence made exact.
Call a collection of strings
closed if it contains every atom and
, contains
whenever it
contains , and
contains whenever it contains and , for each binary
connective .
The collection of all strings is closed, and closed
collections can be much larger than we want.
(i) Every
closed collection
contains every formula. Given a formula and a
formation sequence ending in it, show “if , then ” for every
by Theorem 4.2.2,
case by case as in the proof of Theorem 4.3.1:
each entry is an atom or , or is built by one
clause from earlier entries, which are in already. The last entry
is the formula.
(ii) The
formulas form a closed collection, by
(F1)–(F3).
So the formulas are the smallest closed collection:
contained in every closed collection, and one of them.
Structural induction is (i) applied to one particular
collection. If a property satisfies (i)–(iii) of
Theorem 4.3.1,
the collection of formulas that have is closed: it contains
every atom and
by (i), and the formulas built from members of it are
formulas with , by
(ii) and (iii). So it contains every formula. The
top-down description (“the smallest closed collection”)
and the bottom-up one (“whatever a formation sequence
reaches”) pick out the same strings. The word
“collection” keeps its everyday sense here.
Counting
parentheses: the depth profile
Section 4.1 met the string , which
can be read as or as . With and false and true, the first reading
is true and the second false. Section 4.4 defines the
truth value of a formula one clause per connective, and
the clause to use is decided by the main connective. A
string with two main connectives would get two values.
Formulas carry parentheses, and the parentheses are
meant to settle the reading. This subsection and the
next prove that they do, for every formula. The tool is
a count.
Read a formula from left to right, keeping a running
count: add one at each , subtract one at each
. The count just
before a symbol is its depth: how many
pairs of parentheses are open around it.
The depth profile of . It starts at 0, stays at 1
or more strictly inside, comes back to 0 only after the
last symbol, and the only binary connective at depth 1
is the main connective.
For every formula of the form the
lemma below says the same: (a) the count returns to 0,
(b) it never goes below 0 and stays at 1 or more
strictly inside, (c) every binary connective is at depth
1 or more. The remark after the proof adds that only the
main connective is at depth exactly 1.
We count parentheses in strings, and for this some
words about strings.
An initial segment of a string is the string of the
first symbols of
, for some with the length of
. For it is the
empty string, with no symbols; for
equal to the
length it is
itself. An initial segment is proper if
it is shorter than . The
excess of a string is So a left parenthesis has excess , a right parenthesis
, and any other
symbol ; and the
excess of a string written as two strings one after the
other is the sum of their excesses, since the counts
add. For example, : after reading we are
inside two pairs of parentheses that have not yet
closed. That is the picture to keep: the excess of an
initial segment is the depth we are at
when we have read that far. So the depth of a symbol is
the excess of the initial segment that ends just before
it.
Lemma
4.3.2 (Parenthesis Count)
Let be a
formula.
- (a) :
has as many left as right parentheses.
- (b) Every initial
segment of has . If moreover has the form and
is proper and
non-empty, then .
- (c) For every
occurrence of a binary connective in , the initial segment
of that ends
just before that occurrence has excess at least .
In words: (a) is balance. (b) says that reading a
formula from the left, we never close more parentheses
than we have opened, and that inside a formula we
stay at depth at least until the very last
symbol. (c) says that no binary connective lies outside
all parentheses. Part (a) is the balance proved above,
repeated in the proof because (b) and (c) need it for
the parts; (c), with (a), is what the unique readability
theorem needs, and (b), with (a), is the key to showing
that no proper initial segment of a formula is a formula
(Exercise C1). The steps for (b) and (c) use (a) for the
parts, so the three are proved together. Part (b)’s
second sentence, alone, does not pass through the step;
that is why the lemma proves more, as Example (Prove more to prove less)
did (fold below).
Idea. Induction on the shape of a
formula, all three parts at once. For , the extra
changes no
count. For , list its initial segments by where they
stop: before anything, inside , at the
connective, inside , at the end. Each is
“” followed by
pieces whose excess the induction hypothesis
controls.
↺Second readingThe
proof of the parenthesis count
Proof. We prove, by Theorem 4.3.1,
that every formula has the property
: “(a), (b),
and (c) hold for ”.
Atoms and . The formula is
one symbol, not a parenthesis. (a) Its excess is . (b) Its initial
segments are the empty string and the formula itself,
both of excess ;
and it does not have the form ,
which has length at least . (c) It contains no
binary connective.
Negation. Let be a formula with
; we show
. (a)
, by (a) for
. (b) An
initial segment of is either
empty, of excess ,
or followed by
an initial segment of , of excess by (b) for . The formula
begins
with , so it
does not have the form , and the second sentence of (b) says
nothing about it. (c) A binary connective in lies in , and the initial
segment of before it is
followed by
the initial segment of before it, whose
excess is at least by (c) for .
Binary connectives. Let be formulas
with and
, let be a binary
connective, and let .
(a) , by (a) for and for .
(b) Every initial segment of is of exactly one of
the following five kinds, and its excess is as
shown:
- the empty string: excess ;
- followed by
an initial segment of : excess , by (b) for ;
- : excess
, by (a) for
;
-
followed by a non-empty initial segment of : excess , by (a) for and (b) for ;
- itself:
excess , by (a)
for .
All five have excess at least . The proper non-empty
ones are those of the middle three kinds, and they have
excess at least .
(c) An occurrence of a binary connective in
is the
connective
between and
, or lies in
, or lies in
. Before stands , of excess . Before an occurrence
in stands
followed by the
initial segment of before it, of
excess at least by (c) for . Before an
occurrence in
stands followed
by the initial segment of before it, of excess
at least by (a) for and (c) for . In all three cases
the excess is at least .
So
holds. By Theorem 4.3.1,
every formula has the property , which proves the
lemma.
The three parts were proved together for a reason.
The second sentence of (b), alone, cannot be proved by
structural induction. For , the initial segment is followed by the initial
segment of
the formula , and its excess is ; to know that this is
at least , we need
, a fact about an initial segment of a
negation, which the second sentence of
(b) does not cover. The first sentence of (b) does. A
property that is too weak to pass through the induction
must be strengthened until it does, and here the
strengthening is (b)’s first sentence, as the
strengthening of Example (Prove more to prove less)
was .
The proof (in the fold) gives a little more than (c)
states, and the next proof uses the extra. In a formula
, the initial segment before the
connective
has excess exactly , and the initial
segment before any other binary
connective has excess at least . In the language of
depth: the main connective is the only binary connective
at depth one. That is the recipe of Section 4.1 for
finding the root of a parse tree.
Quick check. Write down the depth
of each symbol of . Which binary connective is at
depth 1?
Solution. 0, 1, 1, 1, 2, 2, 2, 2, 1, and 0 after the last
symbol. The
is at depth 1, and it is the main connective. Compare
the figure, whose main connective was the .
Unique
readability
We can now prove what Section 4.1 promised: a formula
can be built in only one way.
Theorem
4.3.3 (Unique Readability)
Let be a
formula that is neither an atom nor . Then
exactly one of the following holds:
- (i) for a
formula ;
- (ii) for formulas and a
binary connective .
In case (i), is
uniquely determined by ; in case (ii), , and are uniquely
determined by .
In words: every compound formula has one main
connective, and one way of being split into its
immediate parts. This is the precise form of Chapter 1’s
claim that a statement built from letters by connectives
can be read in only one way. Existence is the easy half;
the content is uniqueness. The danger
it excludes is a string such as , which,
if it were a formula, could be split at or at .
Idea. Some form holds, by looking
at the last step (Section 4.1); the first symbol tells
the two forms apart. For case (ii), suppose . By the
remark after Lemma 4.3.2,
each main connective is the only binary connective at
depth one; so both sit at the same position of the
string, and everything else is forced.
Proof. By Section 4.1 (looking at
the last step), is an atom, , for a formula
, or for
formulas ; by hypothesis it is one of the last two.
It cannot be both, since a string of the form begins with
and one of the
form begins with .
Case (i). If , removing the first symbol
gives .
Case (ii). Let . Before the connective stands the initial
segment ,
of excess by Lemma 4.3.2
(a). Before a binary connective inside stands followed by an initial
segment of
of excess at least , by Lemma 4.3.2
(c); so the excess is at least . Before a binary
connective inside stands followed
by an initial segment of of excess at least
, by (c) for and (a) for ; so again at
least . Hence the
position of
in is
the only position of a binary
connective in
whose initial segment before it has excess , and this description
mentions only the string .
Now suppose also for
formulas and a binary connective . By the same
argument, the position of is the only
position with that description. So and stand at the
same position of , and . That
position is the one just after and , and also the one
just after and
, so
and have the
same length; both are the string of symbols of between the first
symbol and that position, so .
Likewise and
are both
the string of symbols between that position and the last
symbol, so . This proves the theorem.
The theorem settles the question Section 4.1 left
open about parse trees.
Every formula has exactly one parse
tree. We know it has one. That it has only one
is proved by structural induction. By (T4) of Definition 4.1.2,
every parse tree is made by one of (T1)–(T3). An atom or
has only the
one-node tree, since a tree made by (T2) or (T3) of Definition 4.1.2
is a tree for a string beginning with or . A parse tree for must have
been made by (T2), from a parse tree for some with ; so ,
and by the induction hypothesis the tree below the root
is the one parse tree of . A parse tree for
must have been made by (T3), from parse
trees for some and a connective with ; by Theorem 4.3.3,
,
and , and by
the induction hypothesis the two subtrees are the parse
trees of
and . From now
on we speak of the parse tree of a
formula.
With one parse tree for each formula, a measurement
of that tree is a measurement of the formula.
Definition
4.3.1 (Height)
The height of a formula , written , is the
number of nodes on a longest branch of
its parse tree.
Atoms and
have height :
their tree is one node, and its only branch has one
node. (Some books count edges instead of nodes and give
atoms height ;
with nodes, every formula has height at least .) In Example (Three parse trees),
(b) has height ,
along the branch , and (c) has height too, along or along .
Warning. The height counts the
nodes on the longest branch, not the
symbols of the formula. The formula has
seven symbols, , , , , , , , and height ; the formula has thirteen symbols and height only . Parentheses never
count towards the height, and a wide tree can be
shallow.
Definition
by recursion
Height, the set of atoms, the number of connectives:
each is naturally defined one clause per way of
building a formula. The height of is one more
than that of ; the atoms of
are those of together with
those of . Such
a definition is called recursive: it
defines the value at a formula through the values at its
immediate parts. The question is whether it really
defines something. For a string that could be split in
two ways, the clauses might assign two different values,
and then they would define nothing. Unique readability
says this never happens.
We say function on formulas for a
rule that assigns to each formula exactly one value; the
values may be numbers, truth values, formulas, or
collections of atoms. Nothing here needs more than this
everyday sense of “function”.
Give a value for each atom and for , and say how to get
the value of a compound formula from its parts; then
exactly one function on formulas obeys these
clauses.
Theorem
4.3.4 (Structural Recursion)
Suppose we are given
- a value for
each atom , and a
value ;
- a rule
that produces a value from
any formula
and any value ;
- for each binary connective , a rule that produces a
value from any formulas and any
values .
Then there is exactly one function
on formulas such
that, for every atom , all formulas and every
binary connective ,
In words: the three lines are the
clauses of a recursive definition, one
for each clause of Definition 4.1.1.
The rules
and may
look at the immediate parts themselves as well as at
their values; most definitions use only the values, and
the list of subformulas below uses the parts. The
theorem says the clauses define a function
(existence) and only one
(uniqueness).
Idea. Build the function on short
formulas first. A formula with one symbol is an atom or
, and the first
clauses fix its value. A longer formula has immediate
parts that are shorter, whose values are already fixed,
and unique readability says which clause applies and to
which parts, with no choice left. So the value at each
formula is forced, length by length. Formally: an
ordinary induction on , proving that there is
exactly one function on the formulas of length at most
that obeys the
clauses.
↺Second readingThe
proof of structural recursion
Proof. For with , call a function
, defined on the
formulas of length at most , -good if it
obeys the three clauses at every formula of length at
most . This makes
sense: the immediate parts of a formula are shorter than
it, so the clauses at a formula of length at most mention values of only at formulas of
length at most .
Let be “there
is exactly one -good function”; we
prove for
every by Axiom 4.2.1,
started at
(“Starting from another number”, Section 4.2).
Base case. By the first-symbol test (Section
4.1), the formulas of length are the atoms and . A -good function must give
each atom the
value and the value , and the function
that does so is -good, since the other
two clauses concern no formula of length . So holds.
Inductive step. Let with , suppose , and let be the -good function. Define
on the formulas
of length at most as follows. At a formula of length at most
, let agree with . Let have length ; it is
neither an atom nor , so by Theorem 4.3.3
it is either for exactly
one formula ,
or for exactly one , , ; the parts have
length at most .
Let in the first case
and
in the second. Unique readability leaves no choice of
case or of parts, so this is one value. The function
is -good: at formulas
of length at most
it agrees with the -good , including at their
parts, and at formulas of length it obeys the
clauses by construction.
For uniqueness, let be any -good function.
Its restriction to the formulas of length at most is -good, so it is , by . At a formula of
length , the
clause for
gives ; at the same argument with gives .
So , and
holds. By
Axiom 4.2.1,
started at , holds for every
; let denote the -good function.
The function . If , the restriction
of to the
formulas of length at most is -good, so it is . For a formula of length , let ; then for
every . The
function obeys
the clauses: for of length , , and likewise for the other two
clauses. And it is the only one: a function on formulas
obeying the clauses restricts, for each , to an -good function, which is
; so for a formula of length . This proves the
theorem.
Unique readability was used at one place: to define
by exactly
one clause, applied to exactly one choice of parts.
Without it, the clauses could demand two different
values at one string, and then no function would obey
them.
What goes wrong without it. The
positive integers are built from by two steps, “add one”
and “double”; adding one alone reaches every positive
integer. Try to define a function one clause per
building step: , , . The
number is built
in two ways, as and as twice . The first clause gives
, the second , and no function obeys both. The
positive integers are not built freely
by these two steps: one number can come out of two
different steps, which is exactly what Theorem 4.3.3
rules out for formulas.
Quick check. Do the clauses , , define a function on the positive
integers?
Solution. No. At , the first step clause
gives and the second .
Example
(Four recursive definitions)
Each of the following is a function on formulas by Theorem 4.3.4.
- Height: ,
, and
- Atoms: ; has no
members; ; and consists of the members of together
with those of .
- Number of connectives: for atoms and ; one more than for
at ; one more
than the sum for and at .
- Subformulas: the list of
subformulas of is
, and of is ; of , the formula
followed by the subformulas of ; of , the
formula followed by the subformulas of and then those of
, each formula
kept only at its first appearance.
Compute all four for , and
also its length.
Solution. Work up from the leaves.
For the parts: , so ; . Hence The atoms of are
and , those of are just
( contributes none),
so . The connectives: and on the left, on the right, at the root, four in
all. The subformulas, in the order the clause lists
them: , , , , , , ; the second is dropped, being
already listed. The length is : the official formula
consists of the fourteen symbols
Two checks connect these definitions with the parse
trees. The recursive height agrees with the tree
height: the parse tree of is that of
with one
node on top, so each branch gains one node; the tree of
is a new root over the trees of and , so a longest branch
is the root followed by a longest branch of the taller
of the two. A structural induction whose cases are these
two sentences (and the one-node tree for atoms and ) shows the two
heights are equal. In the same way, the recursive list
of subformulas is the list of formulas at the nodes of
the parse tree (Definition 4.1.3):
the nodes of the tree of are its root,
carrying , and the
nodes of the tree of .
The length
of a formula , its number of
symbols, also satisfies clauses of this shape, by
counting symbols: a formula of length one for atoms and
, one more at
, and at
the lengths of and plus (two parentheses and
the connective). For above: has symbols, so
has ; has ; so has , as
counted.
Warning. A recursive definition
must have a clause for every way of
building a formula, and each clause may use only the
immediate parts. “Let be of the longest
subformula of plus one” is not
a recursive definition: at itself the
longest subformula is , and the
“definition” refers to the value it is trying to define.
The theorem applies only to clauses of the form it
states.
Exercises
A. Check your
understanding
Exercise
(A1)
- (a) Which kind of
induction fits “every formula contains an atom or ”? Write down its
base cases and the statements of its steps, without
proving them.
- (b) A reader proves
“every formula has at least one symbol that is not a
parenthesis” by structural induction. They check atoms,
the step for ,
and the step for . Which case is missing? Does the
claim hold there?
- (c) Write down,
without proving them, the base cases and the inductive
steps of a structural induction for: every formula has
exactly as many left parentheses as binary
connectives.
- (d) Which parts of
Lemma 4.3.2
does the proof of Theorem 4.3.3
use, and for which formulas?
- (e) Why does Theorem 4.3.4
not apply to the positive integers built from by “add one” and
“double”?
Solution. (a) Structural
induction. Base cases: an atom contains itself, and
contains . Steps: if contains an atom
or , so does
; if
and do, so does , for
each binary .
(Compare the warning in the section: with “an atom”
alone, the case fails.)
(b) The case is missing. The
claim holds there, since is itself such a
symbol. The proof is incomplete, though the claim is
true; compare the warning on “every formula contains an
atom”, where the missing case makes the claim false.
(c) Base cases: an atom and have none of either.
Step for : if
has as many
of each, so has , which adds
neither. Step for : if each of has as many
of each, the whole adds one left parenthesis and one
binary connective.
(d) Part (a) for , to get excess
before the main
connective and to get excess before the part
; part (c) for
and for
, to get excess
at least before
every other binary connective. Here is the formula being read. Part (b) is
not used in that proof.
(e) Its proof needs each compound object to
be built in exactly one way, which for formulas is
unique readability. The number is built as and as twice , so clauses can demand
two values at one number. Some clauses happen to agree
wherever a number is built twice: , , is obeyed by . But without
unique building nothing guarantees this in advance.
Exercise
(A2: Drill)
The parts run from naming the induction, through
computing depths, heights and recursive values, to
judging claims and definitions and running the
checklist.
- (a) Which kind of
induction proves “every formula has as many left as
right parentheses”?
- (b) Write down the
depth of each symbol of . Which
binary connective is at depth 1?
- (c) What is the
excess of the initial segment of ?
- (d) Find the main
connective of by depth.
- (e) What is the
height of ?
- (f) True or false:
every subformula of other than itself has
smaller height than .
- (g) Compute the
recursive height and the recursive list of subformulas
of .
- (h) Define by
recursion the number of occurrences
of in , and compute
.
- (i) Is “ for every formula ” a definition by
recursion?
- (j) “Every formula
has odd length or begins with .” Which case of a
structural induction fails, and on which formula does
the claim fail?
- (k) Do the clauses
,
, define a function on the positive
integers built by “add one” and “double”?
- (l) Run the
checklist on “every formula with no and no has odd
length”.
Solution.
(a) Structural
induction, or strong induction on the position in a
formation sequence, which is how structural induction is
proved.
(b) 0, 0, 1, 1, 1, 1, 1, and 0 after. The
is at depth 1:
it is the main connective of the part inside the
parentheses. The main connective of the whole formula is
the first .
(c) : three left
parentheses, no right one.
(d) The , the only binary
connective at depth 1; the and the are at depth
2.
(e) .
(f) True. A
subformula other than sits at a node
below the root, and the part of the tree below that node
is its parse tree. A longest branch of that part, with
the path from the root of ’s tree down to
the node added in front, is a branch of ’s tree with at
least one more node. So ’s tree has a
branch longer than every branch of the subformula’s
tree.
(g) Height (: 1, : 2, : 3).
List: , , ,
.
(h) for every atom
, , , . Value .
(i) No. It gives
no value at atoms or , and it defines the
value at
from the value at itself, not from
the immediate parts. No function obeys it, since no
number equals itself plus one.
(j) The step for
, whose length is : the hypothesis
allows a part that begins with and has even length.
The claim fails on , of length , beginning with .
(k) No: and by the first
step clause, and then by the first step clause but by
the second.
(l) Objects:
formulas. Property: “if contains no and no , then its length is
odd”, the restriction inside. Base cases: an atom
(length ), and
(vacuous).
Steps:
is vacuous; for without and , its parts satisfy
the restriction, so their lengths are odd, and odd odd is odd. Principle: Theorem 4.3.1.
(Compare (j): with allowed the claim
fails.)
B. Practice
Exercise
(B1)
Prove by structural induction that every formula has
at most as many distinct subformulas as it has symbols.
Use the recursive description of the subformulas in Example (Four recursive definitions)
and the clauses for the length given after it.
Solution. For a formula , write for the number
of distinct subformulas of . We prove by Theorem 4.3.1.
Atoms and . The only
subformula is the formula itself: .
Negation. Suppose . The subformulas of
are
and
those of ,
so there are at most of them (fewer if one repeats).
Hence .
Binary connectives. Suppose and . The subformulas of
are the formula itself and those of and of , so and the right side is .
By Theorem 4.3.1,
for every formula
. (The bound
is attained by ,
, , and every
formula built from an atom or by negations alone;
each binary connective adds three symbols but at most
one new subformula, so the inequality is strict for
every formula that contains a binary connective.)
Exercise
(B2)
The number of nodes of the parse tree of a formula is
given by the recursion , , . Prove that
every formula of height satisfies , and give a formula of height for which equality
holds.
Solution. We prove by Theorem 4.3.1,
using the recursive height of Example (Four recursive definitions).
Atoms and . .
Negation. Let and suppose . Then
and where the last step is .
Binary connectives. Let , , and
suppose the bound for both. Then , so and , and .
Hence
By Theorem 4.3.1,
the bound holds for every formula. Equality at height
: has nodes (a root, two nodes, and four
leaves). Equality needs every node above the bottom
level to have two children.
Exercise
(B3: The mirror image of a formula)
Define a function on formulas by
recursion:
for every atom ,
,
, and for each binary connective
.
- (a) Compute .
- (b) Prove that
for every formula .
- (c) Prove that for every formula .
- (d) Give a formula
, not an
atom or , with
.
Solution. (a) .
(b) By Theorem 4.3.1,
with :
“”. Atoms and : fixes them, so and .
Negation: if ,
then . Binary connectives: if
and , then
(c) By Theorem 4.3.1,
with the recursive height of Example (Four recursive definitions).
Atoms and : both sides are
.
Negation: . Binary connectives:
using the hypothesis for both parts.
(d) , or .
Marking scheme. (8 points)
- 1: (a).
- 3: (b), all four cases (atoms, , negation,
binary).
- 3: (c), a structural induction (on the recursive
height, or showing that the tree of mirrors that
of ) using
the hypothesis for both parts.
- 1: (d).
C. Going deeper
Exercise
(C1: Initial segments are not formulas)
- (a) Prove that no
proper initial segment of a formula is a formula.
- (b) Deduce, in a way
different from the proof in the text, the uniqueness
part of case (ii) of Theorem 4.3.3:
if for
formulas and binary connectives
,
then , and .
Solution (Hint 1). Structural
induction on the formula whose initial segments you
consider. Which part of Lemma 4.3.2
settles the case at once?
Solution (Hint 2). For (b): remove
the first symbol from both sides. Now both and are initial
segments of the same string.
Solution. (a) The empty
string is not a formula, since every formula has at
least one symbol. So it is enough to show that no proper
non-empty initial segment of a formula
is a formula.
We prove this by Theorem 4.3.1.
Atoms and . A formula of
length has no
proper non-empty initial segment.
Negation. Suppose no proper non-empty
initial segment of is a formula, and
let be a proper
non-empty initial segment of . Then is followed by a proper
initial segment of . Suppose, for a
contradiction, that is a formula. It begins
with , so it is
not an atom or
and not of the form ; by looking at the last step
(Section 4.1), for a formula , and
removing the first symbol gives . So is a formula,
hence non-empty, and it is a proper non-empty initial
segment of ,
contradicting the induction hypothesis.
Binary connectives. Let be a proper non-empty
initial segment of . By Lemma 4.3.2
(b), . If were a formula, Lemma 4.3.2
(a) would give .
So is not a
formula. (This case needs no induction hypothesis.)
By Theorem 4.3.1,
no formula has a proper non-empty initial segment that
is a formula, which proves (a).
(b) Suppose . Removing
the first symbol, the strings and
are equal. Both and are initial
segments of this string, so the shorter of the two is an
initial segment of the longer. If their lengths
differed, the shorter would be a proper initial segment
of the longer, and a formula, contradicting (a). So they
have the same length, and being initial segments of the
same string, . The next symbol is then on one side and
on the
other, so ; what remains is , and
removing the last symbol gives .
Marking scheme. (10 points)
- 1: reduces (a) to non-empty segments (the empty
string is not a formula).
- 2: sets up a structural induction (or a strong
induction on the length) with the property “no proper
non-empty initial segment is a formula”, with the atom
and case.
- 3: negation case: reads the segment as followed by a proper
initial segment of , and uses the
last step of a formula beginning with to reach a
contradiction with the hypothesis.
- 2: binary case: excess at least by Lemma 4.3.2
(b) against excess by (a).
- 2: (b): compares and as initial
segments of one string, concludes equal length by (a),
then reads off and .
Fatal errors (0 for the step): using Theorem 4.3.3
to prove (b); assuming the lengths of and are
equal.
Exercise
(C2: Find the error)
The following argument claims to prove that every
formula contains an even number of
parentheses.
- (1) We prove, by
strong induction on , that every formula
with symbols has
an even number of parentheses.
- (2) Let , let be a formula with
symbols, and
suppose that every formula with fewer than symbols has an even
number of parentheses.
- (3) If is an atom or , it has no
parentheses, and
is even.
- (4) If , then
is a
formula with
symbols, so by hypothesis it has an even number of
parentheses; and has the same
parentheses as .
- (5) If , remove the outer pair of parentheses.
The string has symbols, so by hypothesis it has an even
number of parentheses.
- (6) Putting the
outer pair back adds , so has an even number
of parentheses.
- (7) By Theorem 4.2.2,
every formula has an even number of parentheses.
- (a) Is the
conclusion true?
- (b) Which line
fails, and why?
- (c) Show that the
move made in that line is illegal by applying the same
move to a different property that every formula has, and
reaching a false statement.
- (d) Repair the
argument.
Solution. (a) Yes. By Lemma 4.3.2
(a), a formula has as many left as right parentheses,
say of each, so
in all.
(b) Line 5. The induction hypothesis of line
2 is about formulas with fewer than
symbols, and line
5 applies it to the string , which
is not a formula: for , it is , which fails
the first-symbol test of Section 4.1 (length , beginning with an
atom). The hypothesis says nothing about such strings.
Every other line is correct: line 4 applies the
hypothesis to the formula , and lines 1, 2,
3, 6 and 7 are a correct frame for a strong induction on
the length.
(c) Take the property of Lemma 4.3.2
(c), that no binary connective lies outside all
parentheses; every formula has it. Run the same argument
for it: in the case , line 5’s move applies the
hypothesis to the string and
asserts that no binary connective of lies
outside all parentheses. For this
asserts it of , whose lies outside all
parentheses. So the move leads from true hypotheses to a
false statement; it is not a valid step, even though in
the original argument its conclusion happens to be
true.
(d) In line 5, apply the hypothesis to the
formulas
and , each with
fewer than
symbols: they have and parentheses for some
integers , and has , which is
even. (Alternatively, prove the claim by Theorem 4.3.1,
with the same three cases.)
Marking scheme. (10 points)
- 2: (a), with Lemma 4.3.2
(a).
- 3: (b), naming line 5 and why it fails (the
hypothesis is about formulas, and is not
one).
- 3: (c), a property every formula has and a formula
on which the move leads to a false statement.
- 2: (d), the repair through the formulas and .
Fatal errors (0 for the step): locating the error in
line 4.
Exercise
(C3: Exit check: structural induction)
Say that a formula is a -formula
if its only connectives are and and it does not
contain .
Define, by Theorem 4.3.4,
the number of nodes of the parse tree and the number of
negations: with and , and the clauses for the other binary
connectives as for (these choices
play no part in what follows). Prove by structural
induction that every -formula satisfies .
Solution (Hint 1). Theorem 4.3.1
is about all formulas. Put the restriction to -formulas
inside the property.
Solution (Hint 2). Let be “if is a -formula, then
”. The immediate
parts of a -formula are
-formulas.
Solution. For a formula , let be: “if is a -formula, then
”. We prove for every
formula by
Theorem 4.3.1;
for a -formula it is
the claim.
The immediate parts of a -formula are
-formulas,
since every symbol of a part is a symbol of the
whole.
Atoms. .
, and
the connectives . The formulas and with
one of are not -formulas, so
for them holds
vacuously, whatever the clauses chosen for them.
Negation. Suppose , and let be a -formula. Then
is one, so
by , and adding
to both sides
gives .
Conjunction. Suppose and , and let be
a -formula. Then
and are, so and . Adding the two
inequalities and then , (Since the counts are integers, each
hypothesis gives at least to spare, so the left
side exceeds the right by at least .)
By Theorem 4.3.1,
holds
for every formula, which proves the claim.
Marking scheme. (10 points)
- 2: states the property for every formula, in a form
that covers exactly the -formulas, with
the recursive counts.
- 1: atom case.
- 2: negation case, from the hypothesis for , after checking
that is a
-formula.
- 3: conjunction case, using the hypotheses for
both parts.
- 2: names the induction principle and says why and the other
connectives are harmless (vacuous).
Fatal errors (0 for the step): applying the
hypothesis to the formula being proved; a conjunction
case that uses one part only and says “similarly” for
the other.
Exercise
(C4: Challenge: Inside the folded proofs)
These parts are about the proofs in the
second-reading folds of this section; read the folds
first.
- (a) In the proof of
Theorem 4.3.1,
on what is the strong induction performed?
- (b) Where in the
proof of Theorem 4.3.4
is Theorem 4.3.3
used, and why is it not needed for uniqueness?
- (c) In the fold
“Sets built from a base”, prove part (i).
Solution. (a) On the
position of an
entry in a formation sequence of
the given formula, with the property “if , then has ”. Not on the height,
which at that point is not yet known to be well
defined.
(b) In the inductive step, to define for a formula
of length
: unique
readability says which clause applies and to which
parts, so the clauses give exactly one value. That two
functions obeying the clauses agree needs no unique
readability: by Theorem 4.3.1,
if and both obey the
clauses, they agree at atoms and ; and if they agree
at (and
), then at
both
equal , and at both
equal , whichever way the string
may be split.
(c) Let be a closed collection,
a formula, and
a formation sequence with . We prove,
by Theorem 4.2.2
on , the property
“if ,
then ”.
Let and
suppose the property for every . If or , it holds
vacuously. Otherwise: an atom or is in ; if with
, then
by
hypothesis, so ; if with , then , so
. By Theorem 4.2.2
the property holds for every , and at it gives . Since every
formula is the last entry of some formation sequence,
every formula is in .
Marking scheme. (6 points)
- 2: (a).
- 2: (b).
- 2: (c): 1 for the strong induction set up on
positions, 1 for the three cases.
Exercise
(C5: Challenge: formulas without parentheses)
Write connectives in front of their parts and drop
all parentheses. The Polish formulas
are given by the clauses: every atom and is a Polish formula;
if is one,
so is ; if
and are, so are ,
,
and
(for ); and nothing else is. Give
each symbol a weight: for an atom or , for , for each of . The weight of a string is the sum of the
weights of its symbols.
- (a) Write
and as Polish formulas.
- (b) Prove that every
Polish formula has weight , and that every proper
initial segment of it (the empty one included) has
weight at most .
- (c) Deduce that if
and
are the same string, for Polish formulas , then
and .
- (d) Read
by the count, and write it in ordinary notation.
Solution (Hint 1).
- (b) is an induction
over the Polish clauses, set up as in the fold “Sets
built from a base”: the Polish formulas with the
property form a collection closed under the Polish
clauses. Use a strengthened property, as in Lemma 4.3.2.
Solution (Hint 2). (c): if ,
one of them is a proper initial segment of the
other.
Solution. (a)
and .
Read “nothing else is” as in the fold “Sets built
from a base”: the Polish formulas are the smallest
collection of strings that contains every atom and and is closed under
the Polish clauses. So if a property holds at atoms and
and passes
from the parts to the whole at each clause, the Polish
formulas with it form such a collection and include
every Polish formula. In the same way every Polish
formula is non-empty, and is an atom, , , or
,
,
,
for
Polish (the strings of these forms make such a
collection); (c) and (d) use this.
(b) By induction over the clauses, the
property being “weight , and every proper
initial segment has weight ”.
Atom or . Weight ; its only proper
initial segment is the empty string, of weight .
.
Weight . A
proper initial segment is empty (weight ), or followed by a
proper initial segment of (weight ).
(and likewise ). Weight . A proper
initial segment is of one of four kinds: empty (weight
); followed by an
initial segment
of other
than itself
(weight ); (weight
); or
followed by a proper non-empty initial segment of (weight ).
(c) Both and begin at the
second symbol. If they differ, the shorter is an initial
segment of the longer (both are initial segments of the
string after ), a proper
one, and non-empty, since every Polish formula has a
symbol. By (b) the shorter has weight , and as a proper
initial segment of the longer it has weight : impossible. So
, and , are both what
follows :
equal.
(d) Read from the symbol after : the running
weight is after
, after , and first reaches
after . By (b), a Polish
formula ends exactly where its running weight first
reaches , so the
first part of is and the
second is . (From the
first symbol the running weight is ,
reaching only at
the end.) In ordinary notation: .
Marking scheme. (10 points)
- 2: (a).
- 4: (b), with the induction set up over the clauses
and all three kinds of non-empty proper initial segment
of .
- 3: (c), with the non-emptiness of the shorter part
named.
- 1: (d).
Fatal errors (0 for the step): in (b), proving only
“weight ” (then
(c) has nothing to use: the strengthening is the point);
in (c), assuming the two parts have equal length.