The calculus is now complete: Sections 5.3–5.7 gave a
rule for using and a rule for proving each quantifier,
and the two rules for equality. Before any of those
rules can act on a definition from analysis, the
definition has to be written as a formula, and written
correctly. The definitions of analysis have three or
four quantifiers stacked in a fixed order, most of them
carrying a bound such as or
, and every
bound costs extra lines in a derivation. This section
does three things. It translates the standard
definitions into formulas, by a procedure that works
from the outside in. It turns each quantifier rule into
a bounded rule that handles the bound
in the same step. And it collects the traps that make a
translation wrong, each with a reading that shows the
wrong formula wrong.
Four pieces
in one sentence
“The sequence converges to ” is written , and a first
course defines it in one breath: for every there
is such
that for all . The sentence has
three quantifiers, each with a bound (, , ), and a fourth
condition, ,
hidden in “for all ”, which will turn out to sit under an
implication. Each piece has a job, and a slip in any
piece changes the meaning:
- drop the bound , and
the challenger may choose ; then
is impossible, and no
sequence converges;
- swap “for every ” and “there
is ”, and one
must serve every
; then
only sequences that are eventually equal to converge;
- read “for all ” as “for all ”, and the first terms
must already be close to ; then converges to nothing.
So translation deserves a procedure, and the rules
deserve a form that handles bounds without fuss. We take
them in that order.
Translation
from the outside in
Find the outermost claim, name its quantifier and
its bound, then translate what it claims about each
object, in the same way.
The procedure, in three steps:
- Fix the domain. State what the
variables range over. The logic of this book has a
single domain for all the variables of a formula.
Mathematics often mixes kinds of objects in one
sentence: in “for every there
is an
such that for every , …”, the letter is a real
number, while and
are natural
numbers. The convention is: the domain is the
larger kind (here ), and the
smaller kind enters as a bound (, ). So
the sentence begins and
ranges over real numbers that happen to be required, by
the bound, to be natural numbers. A sequence becomes a function
symbol , with
, written , the -th term. Its values at
real numbers that are not natural numbers are never
used, because is
only ever applied to variables bounded by . Section 5.1
stated this convention in one sentence (“Mixing kinds of
number”); here it is in full, and every translation in
this chapter follows it.
- Find the outermost claim. Ask what
the sentence says first, before any detail: “every has a
property”, “there is an with a property”, “no
prime is largest”. That gives the outermost quantifier
(or connective) and its bound.
- Recurse. Translate the property,
which is a sentence about the object just quantified, by
the same two steps. Stop at atomic formulas: equations,
inequalities, membership, and predicate symbols such as
.
A bound is attached to its own quantifier with the
connective of Definition 5.1.1:
under , under . The bounded
notation , does this automatically, which is why
we use it.
A mixed stage. Halfway through, a
translation is part words and part symbols, and writing
that stage down catches most slips. Take “for every
positive , some element
of lies within
of
”. Each line below
translates one more quantifier and leaves the rest in
words, in square brackets, until no words are left:
Read the last line back, symbol by symbol,
into words: if the words are the sentence you began
with, the translation is done.
Example
(Five definitions, translated)
Translate each sentence into a formula, stating the
domain.
- (a) : for every
there is
such that for every .
- (b) The set of real numbers is
bounded above.
- (c) The function
is continuous at : for every there
is
such that for every real with .
- (d) There is no
largest prime.
- (e) Every integer
greater than has
a prime divisor.
Solution. (a) Domain . The outermost claim
is about every : . What it says about is that some
natural number
works: . What it says about is that every natural
number from on is good: , with
the further condition under an implication. So The phrase “for every ” carries two
bounds on ,
membership in
and ; the
first is a bounded quantifier, the second the hypothesis
of the implication. The free variable is (and the statement is
also about the function symbol , which is not a
variable).
(b) Domain ; names a set of reals,
and is a
one-place predicate of (Section 5.1). “Bounded
above” means that some real number is at least every
element of .
Outermost claim: there is an . Its property: every
element of is at
most : The bound belongs to the ; there is no
bound on , which
may be any real number.
(c) Domain , with a one-place function
symbol and a
variable, free in the formula: The last quantifier has no bound of the form
“ something”,
because is
defined on all of ; its restriction
goes under the implication, like in (a). For defined on a set , the last quantifier
would be .
(d) Domain , with the
predicate “ is
prime”. Section 5.1 read the sentence as . A mathematician more often
states it positively, “for every prime there is a larger
prime”: The two forms say the same thing over : the laws of Section
6.2 push the
inside and give , and the order fact that is the same
as
finishes the job. (That last step is a fact about the
order of , not a
law of logic.)
(e) Domain . Outermost claim:
every integer greater than has a property, . The
property: some is
prime and divides . “Divides” is itself a
quantifier: means for some integer . So Unfolded, the first bound is . The innermost quantifier came from a
defined word, “divides”, which is
typical: a definition in words often hides quantifiers,
and a translation unfolds them.
Two remarks on the example. First, the order of the
quantifiers in (a) and (c) is the order in which the
objects are chosen: first, by a
challenger; then
or , by the
defender, knowing ; then or , by the challenger
again, knowing both. That is the game reading of Example (Swapping two quantifiers).
Second, in (c) the letter is free, so the formula
is a statement about ; “ is continuous at every
point” would add in front.
Quick check. Translate “ has a maximum” (an
element of that
is at least every element of ) over . Which quantifier
carries the bound , and does the other quantifier carry a bound
too?
Solution. . The bound belongs to the
: “every
element of ”. The
carries a
bound too, ,
because a maximum must itself lie in ; dropping it gives
, which is “ is bounded above”, a
weaker statement. For the weaker statement is true () and the stronger
one is false.
Warning. Three
mistranslations to avoid. (1) An with under it, such as
: it is true as soon as something lies
outside (Section
5.1). (2) A bound on the wrong quantifier: “ is bounded on ” is ; the form asks for a bound that lies
in and works on
all of , and it
fails for
on ,
which is bounded on by . (3) “For all large
” read as “for all
”: “ for all large
” is , not . The sequence satisfies the
first (take )
and not the second ().
Five
traps
The warning above caught three slips. Here are five
more, each with the reading that shows the wrong formula
saying something else.
Example
(Five traps, each with a separating reading)
The domain is unless the row says
. and are sets of reals, and
is a
one-place predicate (Section 5.1).
| (a) |
Some natural number lies strictly between and . |
|
|
The domain is , by step 1. The
sentence is false, since and ; the
wrong formula is true, with . Under one
domain, a letter for a natural number ranges over the
reals unless its bound says otherwise. |
| (b) |
Every element of and of is positive. |
|
|
,
: the
sentence is false (). The wrong formula speaks only of common
elements, and there are none, so it is true. The “and”
of the sentence is an “or” in the restriction. |
| (c) |
Only even numbers are multiples of . (Over .) |
|
|
The right formula is true; the wrong one is false at
. “Only are ” puts after the arrow, as
“only if” did in Section 1.1. |
| (d) |
If a natural number is divisible by , then it is even. (Over
.) |
|
|
The right formula is true. In the wrong one the last
is free, and read
at it says
“if some number is divisible by , then is even”: the
hypothesis is true () and the conclusion false. “A … it” hides a
“for every”. |
| (e) |
If any element of is negative, then is not a lower bound of
. |
|
|
:
the right formula is true, since its hypothesis is
false. In the wrong one the hypothesis “every element of
is
negative” is true and the conclusion “not every element
of is at
least ” is false
(Section 5.1, the empty set). This is Section 5.1’s
warning on “any”, now with the reading that separates
the two formulas: the empty set. |
A reading like these is a counter-reading for the
step from one formula to the other; it shows that the
two say different things, which is all a translation
needs to know.
Infinitely many, and eventually.
“ for
infinitely many ”
says that however far out you start, some later term is
positive: “Eventually ”, that is, for all large
(warning (3)
above), says The quantifiers are swapped, and the bound
moves from
to , as the two
connectives of Definition 5.1.1
require. For the first is true (every even will do) and the
second is false (every odd fails).
Quick check. Translate “ for only finitely
many ”.
Solution. From some index on, no
term is : . Finitely many
exceptions all lie below some .
Translation error or derivation
error? When a derivation ends in a statement
you believe false, there are two places to look. A
derivation error is an illegal line,
and checking the derivation line by line finds it. A
translation error is a formula that
does not say what its sentence says, and no line check
finds it, because every line may be correct. Suppose a
reader translates “some element of exceeds ” as , the slip of warning (1) above, and takes
. From
the true line , two steps derive that formula: by
Proposition 2.1.2,
then at .
Both steps are legal. The conclusion is a true formula
about , and the
sentence it was meant to translate is false, since
neither nor exceeds . The fault is in the
translation, not in the derivation. So check a
surprising conclusion in two ways: run the line check,
and read the formulas back into words.
Rules for
bounded quantifiers
Every analysis formula has bounds, and each bound
doubles the work of a rule. To use at the term ,
gives , and a second step,
with a line , gives .
To prove with the witness ,
builds and
finishes. Every step is legal and every step is
predictable, and a derivation about limits drowns in
them. So we fold each pair into one step.
A bounded quantifier gets a rule of its own: the
bound travels with the quantifier.
Proposition
6.1.1 (Rules for Bounded Quantifiers)
Let be a fixed
set, so that
is a one-place predicate symbol (Section 5.2), a variable and a formula. The
following four rules, the bounded
rules, may be used in derivations, with the
rule names of the unbounded rules and the same side
conditions: in and , the term is free for in ; in , the name appears in no
premise, in no assumption of a box still open at line
, and not in ; in , it appears in no
premise, in no assumption of a box still open at line
, and not in or in . The last line of each box is a line of
that box itself.
asm, for
–
asm, for
asm, for
, –
Every use of a bounded rule can be replaced by a
block of steps of the unbounded rules (Sections 5.3–5.6)
and of Chapter 1, with the same premises, the same
assumptions open, and the same last line. Hence any
derivation that uses the bounded rules converts into one
that does not. The same holds with and replaced by and , or by the
bounds , , , for a term in which does not occur.
In words: to use “every in has ”, produce an
element of and conclude for . To
prove “some in has ”, exhibit an
element of with . To
prove “every in has ”, let be an arbitrary
element of (the
box opens with the assumption ) and prove
for it. To
use “some in has ”, take such an
element , with
both facts about it as assumptions, and derive something
that does not mention it. These are exactly the
sentences a mathematician writes: “let ”,
“since , the hypothesis applies to ”, “take ”, “choose
such
that …”.
The bounded box
is the only flagged box with an assumption that closes
by . Its assumption mentions the
flag, and that is allowed: the side condition asks about
assumptions of boxes still open at line , and the box’s
own assumption has closed there.
In a finished derivation, the assumption of a bounded
box is printed “asm, for ”,
since the box closes by .
↺Second readingWhy
a proposition, not a definition
Why is this a proposition and not simply a
definition? Because the calculus is fixed: its rules are
those of Chapters 1–2 and Sections 5.3–5.7, and a new
rule is admissible only if it adds no derivable
sequents. Definition 2.3.1
gave one way to show that: a proved sequent, written
with statement letters, may be used as one line. It does
not cover these rules. The bounded and
are one line each, but they are schemas in a
formula, a variable and a term, not in statement
letters; the bounded and
close boxes, which no proved sequent can. So
the proposition proves admissibility the direct way:
each bounded step is shown to be an abbreviation of a
block of unbounded steps. In this sense the bounded
rules are derived rules, in a looser sense that extends
Chapter 2’s: a line citing one abbreviates a block of
primitive steps, not a proved sequent.
Idea. A bounded quantifier is an
abbreviation (Definition 5.1.1):
is the formula , and
is . So each bounded
rule should be an unbounded rule on the unfolded
formula, plus the connective rule that handles or . Write the block,
then check two things: the block is a correct piece of
derivation wherever the bounded step was, and its side
conditions hold exactly when the bounded ones do.
Warning (Not allowed: the bounded
rules). Each step below is wrong; the tag names
the condition of Proposition 6.1.1
that it breaks.
- From alone, write :
the bounded
cites two lines, and the line is missing.
- From alone, write : the bounded
needs the line too.
- Close a bounded box
on
while the assumption of an enclosing box is still
open: the flag appears in an assumption of a box still
open.
- Close a bounded box
on with the
last line : the conclusion mentions the
witness.
The proof writes out, for each bounded rule, the
block of unbounded steps it abbreviates, and checks that
the side conditions match; it is in the fold below.
↺Second readingThe
proof: each bounded rule as a block of unbounded
steps
Proof. We give the replacement
block for each rule and check it. In each block, the
lines of the bounded version keep their labels, and new
lines get new letters.
Bounded . Line is . Replace line by two lines:
,
Line is at
: the formula
is by Definition 5.2.5,
since is not a
variable. Its side condition asks that be free for in (Definition 5.2.6),
which holds exactly when is free for in , since has no
quantifier. Lines
and are available
at and because they were
available at .
Bounded . Replace line by:
,
Line is the
instance at of
, and is free for there exactly when it
is free for in
.
Bounded . Replace the box and line by a flagged box with
no assumption, which contains a box
holding the old lines:
asm, for
–
–
The lines between and are unchanged. Each of
them lies inside both new boxes, so every line it cited
is still available (Definition 1.4.2,
with the flagged boxes of Section 5.4): a line outside
the old box is outside both new ones, and a line inside
the old box is inside the new box.
The side conditions inside the old box are unaffected
too: a line inside it has the same open assumptions as
before,
(now the assumption of the box)
together with the outer ones, because the flagged box
adds none; so every flagged box that closes inside the
old box still meets its side condition. Line is , and it
is the last line of the flagged box, as
requires; it is the instance at of . Now
the side condition of at
line : the
premises are the same as before; the boxes still open at
line are the same
as those open at line in the bounded version,
because the box on
has
closed before line ; and the conclusion is
the same formula. So the unbounded side condition holds
exactly when the bounded one does.
Bounded . Line is . Replace the box’s two assumptions by
one assumption and two lines of :
asm, for
, –
Lines and
now hold the same
formulas as the old assumptions, inside the same box, so
every line that cited them may still cite them. At a
line inside the box, the open assumptions are now together with the outer
ones, where before they were and together
with the outer ones. A name appears in exactly when it appears
in or in
, so
every flagged box that closes inside the box still meets
its side condition. The box assumes the instance at
of ,
as requires. Its side condition at line names , the formula , the premises and the assumptions open
at line : the same
four things as the bounded side condition, with the same
result.
For the bounds and the others, the same four blocks work
with and
in place
of and
. One point
needs the hypothesis that does not occur in : then is , and the bound
contains no bound variable, so free-for conditions are
unaffected by it.
Replacing the bounded steps one at a time, each by
its block, removes them all; the premises and the last
line do not change. This proves the proposition.
Each block is one line longer than the bounded step
it replaces: two lines for one in and
; the extra line in
; three lines (an assumption and two ) for
two assumptions in . So
each bounded step saves exactly one
line, and a derivation with many bounds saves
many. More than the count, the bounded rules keep the
derivation at the level at which a mathematician thinks:
“let ” is one step, not two.
Quick check. Unfolded,
is . A student uses the bounded on
it and writes the box with the single assumption . Is that wrong?
Solution. No, it is the unbounded
, which is always available, since the
bounded formula is the unfolded one. It
costs two lines inside the box to separate from . The bounded
rule opens the box with the two assumptions already
separated. Both are correct; the bounded one is shorter
by one line.
A limit
derivation with bounds
Here is the first derivation in the book about a
limit. The claim is the school fact “if , then ”, with the
definition of Example (Five definitions, translated)
(a).
Claim. Over , derives the same formula with and in place of
and , using two lines of
arithmetic, justified “arith”:
gives , and gives (because ).
Idea. Run the search. The goal
starts with : open a bounded box,
“let ”. The new goal starts with :
postpone it (the step of Section 5.5),
since no witness is in sight. Turn to the premise: it
starts with , and the step of Section 5.3
says to instantiate it at the term the goal needs. Which
term? The goal will need , which follows from : so instantiate at , after
an “arith” line
for the bound. That gives an line:
open its box at once, with a witness
(the step of
Section 5.6), and let the box’s last line be the current
goal. Now the postponed goal has its witness: itself. The remaining
goal opens a bounded box
for , and a
box on
finishes with one , one
,
and the second “arith” line. This is the pattern of Proposition 5.6.2:
fix ,
obtain ,
choose as the witness.
Two abbreviations show the shape. Write for
, “from
on, every term is
within
of ”, and for
the same formula with and . The premise is , and the
goal is the same with . With the lines that
look inside left
as a gap, the derivation is:
1
2asm, for
3arith 2
4 1, 3
5asm, for
6asm, for
13
14 5, 13
15 4, 5–14
16 2–15
Lines 7–12 are the only lines that look inside and : they unfold
at a fresh and
prove the instance that line 13 folds back into .
The derivation in full follows the check below; its
lines 1–6 and 13–16 are the lines above, written
out.
Quick check. In the outline, line 4
instantiates the premise at . Why that
term, and not ?
Solution. The goal needs , which is , so it is enough to have . The term is read off the goal
(Section 5.3’s step), not off the premise. At the premise
would give only , hence , which does not reach the
goal.
1
2asm, for
3arith 2
4 1, 3
5asm, for
6asm, for
7asm, for
8 6, 7
9asm, for
10 8, 9
11arith 10
12 9–11
13 7–12
14 5, 13
15 4, 5–14
16 2–15
Check the side conditions at the three lines that
close flagged boxes, and the witness line.
- Line 13 (, flag ): is not in the
premise, not in line 13, and not in the assumptions
still open at line 13, which are lines 2, 5, and 6.
- Line 14 (): the witness , with its bound on
line 5 and the instance on line 13.
- Line 15 (, flag ): is not in line 15,
the conclusion (the witness has been forgotten by line
14), not in line 4, not in the premise, and not in the
open assumption on line 2.
- Line 16 (, flag ): is not in
the premise and not in line 16, and no assumption is
open at line 16.
Line 4 is where comes to depend on
: the
witness is
obtained from the premise at , so it depends on , exactly as
the order allows. Section 6.4
makes this reading of dependence precise.
In prose, line by line:
Let [lines 2, 16]. Then
[3], so, since , there is with for every [4]; choose such
an [5, 6, 15].
Let with
[7, 9].
Then [8, 10], so [11]. So this works [12–14].
Written with the unbounded rules, the same derivation
has 22 lines, since each of its six bounded steps (lines
4, 8, 13, 14, 15, and 16) costs one line more. The claim
“”
(for ) is
not derived here: its proof needs the Archimedean
property, a fact about inside , not a law of
logic.
Exercises
A. Check your
understanding
Exercise
(A1)
- (a) Translate into
formulas, stating the domain: (i) every real number has
a cube root; (ii) the function is bounded on ; (iii) between any two
different real numbers there is a rational number; (iv)
the sequence
is eventually constant; (v) some natural number divides
every natural number.
- (b) Three students
translate “some element of is larger than every
element of ”, over
:
- (i) ; (ii) ; (iii)
. Which are correct? For
each wrong one, give sets , for which it has the
wrong truth value.
- (c) Which variables
are free in your answer to (a)(iv)?
- (d) Write the
bounded rule as a block of two unbounded
steps, and name the two rules.
Solution. (a) (i) Over
: . (ii) Over : . (iii) Over , with a one-place
predicate symbol: ; “different”
is carried by , which names the smaller number (the case is the same
statement with the letters exchanged). (iv) Over , with a function symbol:
. (v) Over
: ; it is true, with .
(b) Only (i) is correct. (ii) has under : with and , the sentence
in words is false, but (ii) is true, because makes the
implication vacuously true. (iii) has the quantifiers in
the wrong order: it lets the element of depend on . With , (iii) is
true (for each ,
take ),
and the sentence in words is false, since no natural
number exceeds every natural number.
(c) None of the variables: and are bound. The formula
is a statement about the function symbol , which is not a
variable.
(d) From and : first by , then
by ,
which is unfolded.
Exercise
(A2: Drill)
Each part takes a line or two. The domain is , and , are sets of reals. The
parts run from translating, through unfolding and
judging, to single steps of the bounded rules.
- (a) Translate “ is bounded above on
”.
- (b) Translate “every
element of is
less than some element of ”.
- (c) Translate “some
element of is
less than every element of ”.
- (d) Unfold the
bounds of (c).
- (e) Write the mixed
stage, then the formula, for “every element of has a larger element in
”.
- (f) Translate “ for all large
”.
- (g) Translate “ for infinitely
many ”.
- (h) Translate “not
every element of
is positive” and “no element of is positive”, and
decide both for .
- (i) Translate “if
for any real ,
then ”.
- (j) Lines 1 and 2 . What does the bounded 1, 2
give?
- (k) Lines 1 and 2 . What does the
bounded 1, 2 give, with the formula ?
- (l) How many lines
does a bounded save
over the unbounded rule?
Solution.
(a) .
(b) .
(c) .
(d) .
(e) , then
.
(f) .
(g) .
(h) , true for (because of ); , or , false (because of ). One word apart,
opposite truth values.
(i) : “any” after “if” is “some”. It is true,
since no real square is negative.
(j) .
(k) .
(l) One: two
assumptions in place of one assumption and two
lines.
B. Practice
Exercise
(B1: Three definitions)
Formalize each statement, stating the domain and the
kind of each symbol (variable, constant, function
symbol, predicate symbol; membership in a fixed set
is a one-place
predicate symbol, as in Section 5.2).
- (a) The set of real numbers is
bounded (above and below).
- (b) The function
is increasing on : for all , implies .
- (c) The sequence
is bounded:
there is a real
with for all .
Then, for (c), write the formula with the two
quantifiers in the other order, and say why it holds for
every sequence.
Solution. No constants occur in any
of the three parts.
(a) Domain ; , , variables (all bound);
a one-place
and a two-place
predicate symbol. . The two witnesses are chosen before , so they must work for
every element of .
(b) Domain ; , variables (bound);
a one-place
function symbol; a one-place and , two-place predicate
symbols. .
(c) Domain ; , variables (bound);
a one-place
function symbol (the one-domain convention, step 1 of
the procedure), and a one-place
function symbol; a one-place and a two-place predicate
symbol. .
Swapped: . It holds
for every sequence, because the witness may depend on
: take . The
sequence ,
which is not bounded, satisfies it. As in Example (Swapping two quantifiers),
the swap turns a statement about one for all into a statement about
each term separately.
Exercise
(B2: A bounded rehearsal)
Using the bounded rules of Proposition 6.1.1,
derive Then say how many lines the derivation would
have with the unbounded rules only.
Solution. The goal is an : postpone it. The
second premise is an : open its bounded
box at once, with a witness and the two
assumptions and , and aim for the
goal as the box’s last line. Inside, the first premise
is a , and the term the box offers is , with its bound on a
line. The witness for the goal is again.
1
2
3asm, for
4asm, for
5 1, 3
6 5, 4
7 3, 6
8 2, 3–7
At line 8,
is not in line 8, not in line 2, and not in either
premise; no other box is open. The derivation uses three
bounded steps (lines 5, 7 and 8), each of which costs
one more line unbounded, so the unbounded derivation has
lines:
the box assumes and splits it with two
lines; line 5 becomes then
;
line 7 becomes then
.
The bound is the whole point of the exercise: the
witness must
carry its membership in from the premise to the
conclusion, and the bounded rules make that one
assumption and one citation.
Exercise
(B3: One key, twenty sentences)
The domain is . Use only (“ is prime”), , , (“ divides ”, that is, for some
), and the constants , , , with variables , , . Translate sentences
1–18 into formulas. Then translate 19 and 20 into
English and decide whether each is true.
- is an even
prime.
- Some prime divides .
- Every prime greater than is odd.
- No prime is less than .
- Every even number is divisible by .
- Only odd numbers divide .
- divides every
number.
- Some number divides every number.
- Every number is divisible by some number.
- There is no largest prime.
- There are infinitely many primes.
- Every number greater than has a prime
divisor.
- The only divisors of a prime are and the prime
itself.
- If a number divides , it is or .
- Not every odd number is prime.
- Between any two numbers, one less than the other,
there is a third.
- Some prime divides every even number.
- Every divisor of is .
- .
- .
Solution.
- .
- .
- .
- , or .
- .
- .
- .
- .
- .
- .
- .
- .
- .
- .
- .
- .
- .
- .
- “Two numbers that divide each other are equal.” True
in : if and , then , so either , and then too, or , which in means .
- “Every even number has a prime divisor other than
.” False: at , and at every power
of (), the
only prime divisor is .
Sentence 10 restricts to primes and 11 does
not; both are true, and in each follows from the
other. Sentence 16 is false (take , ), and its
translation is still correct: a correct translation of a
false sentence is a false formula.
Exercise
(B4: Unfold, then fold back)
Over , for
fixed sets , , of reals, write for “every
element of is an
element of ”,
for the
set of reals in
or in , and for the set of
those in both. Use only the predicates , , .
- (a) Unfold .
- (b) Unfold .
- (c) Unfold “ has no
element”.
- (d) Fold back .
- (e) Fold back .
- (f) A reader unfolds
as the formula in (e). Give sets that
separate the two, and say why the reader’s formula is
wrong.
Solution. (a) .
(b) .
(c) .
(d) and .
(e) .
(f) , , . Then is false, since and . The formula
of (e) is true, because has no element, so its hypothesis is
false for every .
The reader’s mistake is trap (b) of the section: “in
or in ” is the restriction of
(b), and it must be written with ; the “and” of “every
element of and of
” is an “or” in
the restriction.
Marking scheme. (10 points) - 2:
(a)–(c) together, with every bound attached by under (and by under the of (c)). - 2: (d)
and (e). - 3: (f): the two sets, with one sentence on
each truth value. - 3: the reason in words that the
restriction of (b) is an “or”. Fatal error (0 for (f)):
a pair of sets on which the two formulas agree.
C. Going deeper
Exercise
(C1: Where the stands)
Let and . Translate, over :
- (a) is uniformly
continuous on : for every there
is
such that for all , implies ;
- (b) is continuous at every
point of : for
every and
every there is such that for every ,
implies .
Then describe, in one sentence, the only difference
between the two formulas, and say what it means for the
choice of .
Solution. (a) .
(b) .
The only difference is the position of : in (a)
it stands after , in (b) before it. In (b) the
defender chooses knowing , so may depend on
and on ; in (a) is chosen before
any is given, so
one must
serve every
at once, and it depends on only. Section
6.4 derives (b) from (a) and shows that on satisfies (b) but not
(a); Section 7.2 turns this example into a
counter-model, so (b) does not derive (a).
Exercise
(C2: Six orders, four statements)
Fix a formula (the “matrix”) in the
variables , , , and consider the six
sentences obtained by putting the prefixes , , in front of
in the six
possible orders: , , and so on. Call two of these orders
essentially the same if the two
sentences are provably equivalent () for every
matrix , and
essentially different if some matrix
over gives them
different truth values (read informally, as in Section
5.1).
- (a) Show that the
six orders fall into four groups, with any two orders in
one group essentially the same.
- (b) Using the
matrices
and over
, show that any
two orders from different groups are essentially
different. So the six orders say four different
things.
Solution (Hint 1). Two ’s side by side
can be exchanged: that was one of the derivations of Example (Flagged boxes at work).
What is left to decide is where stands.
Solution (Hint 2). List the six
orders by the position of : first, middle
or last. When it is first or last, the two ’s are side by
side.
Solution. (a) Sort the
orders by the position of .
-
first: and .
- last:
and .
- in
the middle: , and .
Two adjacent ’s may be
exchanged: for every formula , by the derivation
of Example (Flagged boxes at work)
that exchanges two universal quantifiers (it uses
nothing about its matrix but that it is a formula). This
gives the “last” pair at once. For the “first” pair the
’s sit under
: open the
box on with a witness
, exchange the
two ’s
inside it, and close with at
; the other
direction is the same. So there are at most four groups:
, , and .
(b) Call the groups F ( first), L
(last), () and
(). Over , evaluate each group
with the two matrices, reading informally (Section
5.1):
| F |
false: no
exceeds every |
false: no
exceeds every |
| L |
true: given ,
, take |
true: take |
|
true: given ,
take |
false: no
exceeds every |
|
false: no
exceeds every |
true: given ,
take |
Every two rows differ in at least one column, so
every two groups are separated by one of the two
matrices: F from L, from and from by the column in
which the other group has “true”; L from by and from by ; from by either. So the six
orders say four different things: within a group the
sentences are provably equivalent by (a), and across
groups some matrix over tells them apart.
Marking scheme. (10 points) - 2:
lists the six orders and sorts them by the position of
. - 3:
justifies the two collapses, citing the exchange of
adjacent ’s,
and handles the pair under (by an box,
or equivalently). - 3: gives, for each of the six pairs
of groups, a matrix and the two truth values, with
witnesses for the true sentences. - 2: concludes that
the six orders say four different things, combining (a)
and (b). Fatal errors (0 for the step): exchanging with ; a “separation”
in which the two sentences have the same truth
value.
Exercise
(C3: Eventually, therefore infinitely often)
- (a) With the bounded
rules, derive Lines of arithmetic may be justified
“arith”.
- (b) For the
converse, give a reading of over under which the
premise is true and the conclusion false.
Solution. (a) The goal is
a bounded :
open its box first, with . The premise is a bounded : open its box
early, with and its property. The postponed goal needs a
term that is at least and at which the
premise applies, so at least : the sum is both.
1
2asm, for
3asm, for
4asm, for
5arith 2, 3
6 4, 5
7arith 2
8 6, 7
9arith 3
10 9, 8
11 5, 10
12 1, 3–11
13 2–12
Lines 7 and 9 use and , which hold for natural numbers. The side
conditions:
- At line 12,
is not in line 12, not in line 1, not in the premise,
and not in the open assumption on line 2.
- At line 13,
is not in the premise and not in line 13, and no
assumption is open.
- At lines 6 and 11, the term is free for
.
The witness is built from the two names in play: fix
, obtain , choose a term made
from both.
(b) Let be “ is even”. The premise
of the converse, , is true: beyond any there is an even
number, such as .
Its conclusion, , is false: beyond any there is an odd number,
. This is a
counter-reading (Section 7.2).
Marking scheme. (10 points) - 2:
opens the flagged box of and the box
on the premise (in either nesting) before choosing the
witness. - 3: a witness that depends on both names, with
both bounds checked by arith lines. - 2: checks the side
conditions at lines 12 and 13. - 3: (b): a reading, with
both truth values justified. Fatal errors (0 for the
step): a witness chosen before is given; the witness
itself, which
need not be at least .