Give a construction of the integers (Z)
from the natural numbers such that z = {m,n|m-n £ z}.
Define addition and subtraction for both this coding and the one in Example
1.2.1.
Show how to add and multiply complex numbers as pairs
of reals, verifying the commutative, associative and distributive
laws and the restriction of the operations to the reals.
The volume-flow (in m^{3} s^{-1}
) down a pipe of radius r of a liquid under pressure p is ch^{n}r^{m}p^{k}
for some dimensionless c, where h is the dynamic viscosity,
in units of kg m^{-1} s^{-1}.
Find n, m and k.
Show how to add Dedekind cuts and multiply them by
rationals, justifying the case analysis of the latter into positive,
zero and negative. What do your definitions say when the cuts represent
rationals? Verify the associative, commutative and distributive laws.
Express Ö2, Ö3 and Ö6 as Dedekind
cuts, and hence show that
Ö2·Ö3 = Ö6.
Let x = (L,U) and y = (M,V) be Dedekind cuts of Q
and put
omitted eqnarray* environment
Show that (the lower closure of) \typeN_{1}È\typeN_{2} and (the upper
closure of) \typeW_{1}È\typeW_{2} define a Dedekind cut of R.
Calling it xy, verify the usual laws for multiplication, without using
case analysis [Con76].
For any Cauchy sequence (\arga_{n}), show that there
is an equivalent sequence (\argb_{m}) which satisfies
"n, m.|\argb_{n}-\argb_{m}| < 1m+1n [BB85].
Show how to add Cauchy sequences and to multiply them
by rational numbers.
Show how to reduce a Cauchy sequence of reals ( ie
of Cauchy sequences) to a Cauchy sequence of rationals [Hint: diagonalise].
Define multiplication of Cauchy sequences, without
using a case analysis according to sign.
Let (\arga_{n}) be a Cauchy sequence and (L,U) a
Dedekind cut. Formulate the predicate f[(\arga_{n}),(L,U)],
that they denote the same real value. Show that for every Cauchy sequence
there is a cut, and that
f[(\arga_{n}),(L,U)]Ùf[(\argb_{n}),(L,U)] Û (\arga_{n} ) ~ (\argb_{n}).
Hence f is an injective functional relation
\realno_{C} \hookrightarrow \realno_{D}. Show that it respects addition and
multiplication. Show, using excluded middle, that f is bijective
(see also Exercise 2.30).
Explain the difference between p(U) in Example
2.1.5 and \funf_{!}(U) in Remark
2.2.7.
Show that each element U,V of X+Y, defined in
Example 2.1.7, is either of the form
{x}, Æ with x Î X, or else of the form Æ,{y}
with y Î Y, but not both. [Hint: use (ÚE ) on the first
clause.] Deduce that for any functions f:X® Q and g:Y® Q
, the subset \fred_{!}(U)È\guy_{!}(V) Ì Q has exactly
one element. So there is a unique function [f,g]:X+Y® Q such
that [f,g]on_{0} = f and [f,g]on_{1} = g.
Using the isomorphism
P(X+Y) º P(X) xP(Y), construct the product XxY from powersets and disjoint
unions. [Hint: consider those U Ì X+Y with exactly one element
in each component.]
For any set X, show that there is a function
c:P( X)\{Æ} ® X such that
"U.c(U) Î U, iff the axiom of choice holds (Definition
1.8.8). (This was Zermelo's formulation
of the axiom of choice.)
Any predicate f[x] gives rise to an equivalence
relation ~ on {0,1}xX so that
"x.(f[x] Û 0,x ~ 1,x). Let Y = ({0,1}xX)/ ~
and p:Y\twoheadrightarrow X by p[i,x] = x. Prove that
"y. $j.y = [j,p(y)], making your use of ($E ) explicit.
Show that if this has a Choice function then f is decidable. Hence
the axiom of choice implies excluded middle.
Show that
omitted eqnarray* environment
giving the functional relations involved. Use these to show that the
axiom of comprehension may be eliminated from Zermelo type theory, in
the sense that every type is of the form {x: U|f[x]}
where U is a type-expression built from 1, N,
x and P alone. Hence develop a formalism for Zermelo type
theory with unordered contexts.
Let a,b,c,d Î X, not necessarily distinct.
Explain carefully what the left hand side means ( cf Example
2.1.6(c)) and prove that
{a,b} = {c,d}Û (a = cÙb = d)Ú(a = dÙb = c)
by simplifying a disjunction of 16 cases, 14 of which give a = b = c = d.
For x,y,x¢,y¢ Î Z, write
KWP(x,y) = {{x},{x,y}} Î P^{2}(Z)
for the Wiener-Kuratowski pair. Using Exercise
2.18, show that
KWP(x,y) = KWP(x¢,y¢)Û x = x¢Ùy = y¢,
without using excluded middle on x = yversusx ¹ y.
Give the functional relations
P^{2}(Z)\leftharpoondown \rightharpoonup Z defining the product projections p_{0} and
p_{1}. Hence for X,Y Ì Z show that
{KWP(x, y)|x Î XÙy Î Y} Ì P^{2}(Z) satisfies the
rules for the product type (Remark 2.2.2).
This formula is the one surviving instance of an early application of
the representation of the formal poset x £ y by subsets (Definition
3.1.7).
Explain how
P^{n}(N) Ì P^{m}( N) for n £ m. Using Exercises 2.17
and 2.19, show that the types U with
U Ì P^{n}(N) for some n Î N form a model of pure Zermelo
type theory. It is known as the von Neumann hierarchyV_{w2}
.
Give the l-terms which define the isomorphism
between X and X^{1}x1^{X}, and verify that they
are mutually inverse.
Show how to orient the b- and h-rules
for pairs (Remark 2.2.2) to make them
confluent and strongly normalising (Definitions
1.2.5 and 1.2.8).
The normal form says how the types are bracketed.
A (raw) l-term is in head normal
form if it looks like
where x is either a constant or a variable, possibly one of the y_{i},
and no sub-sequence x \argu_{1}¼\argu_{k} is a d-redex.
Show that a term is in normal form iff it is hereditarily head
normal.
The de Bruijn index of a bound variable
is the number of ls which separate its use from its declaration
in the tree structure of the term. For example
lx.(ly.xy)x becomes l.(l.2 1)1. ( Cf the way in
which a compiled procedure accesses local variables relative to the
current stack pointer.) Give the formal translation of raw l-terms
from variables to de Bruijn indices and vice versa . Show that,
using indices, substitution is performed textually, except that in
(lx.a)[y: = b] the free indices within b are incremented.
Show that a-conversion is unavoidable in
the reduction of the untyped term (lx.xx)(lx, y.xy).
Combinatory algebra is given by one binary
operation called application and two constants S
and K with laws Sxyz = xz(yz) and
Kxy = x (Example 2.4.2). Show functional
completeness, that any term p in variables x_{1},¼, x_{n} is
equivalent to some fx_{1}x_{2}···x_{n}, where f is a
term with no (free) variables. [Hint: by structural recursion, use
u = (Ku)x and (ux)(vx) = (Suv)x
to eliminate x_{n} first and similarly the other variables.] Translate
the term T = lx, y, z.xzy.
Recall from Remark 1.6.10
that the two axioms of implicational logic are the types of
S and K. Use Exercise
2.26 to prove the deduction theorem,
that if f is provable from hypotheses a_{1},¼,a_{n}
then
a_{1}Þ ···Þ a_{n} Þ f is provable under no hypothesis. This says that
each instance of the (Þ Á )-rule is derivable in
this calculus.
Suppose that X^{R}\triangleleft R, iej:X^{R}\hookrightarrow R, q:R\twoheadrightarrow X^{R} with
j;q = \id_{X R}. Show that any f:X® X has a fixed point.
Use the elimination rule for Æ to show
$x:Æ.f[x]\dashv \vdash ^ and
"x: Æ.f[x]\dashv \vdash T. Formulate the substitution
rule and use it to show that any X® Æ is invertible. Show
also that
$x:1.f\dashv \vdash f[x: = *] \dashv \vdash "x:1.f.
Consider the last clause in the definition of a Dedekind
cut (Remark 2.1.1). Show that an assignment
(x_{e} ,y_{e} ) of witnesses (as in Remark
2.4.3(g)) provides a pair of Cauchy sequences
which define the same real number in the sense of Exercise
2.11.
Show that Peirce's law,
((qÞ f)Þ q)Þ q (Remark
2.4.10), excluded middle and the restart
rule are intuitionistically equivalent.
What, in a word, is a well founded functional relation?
(Pierre de Fermat) Show that a prime number can be
expressed as the sum of two squares iff it is (either 2 or) of the form 4n+1.
[Hint: define q\prec p on primes of this form if q < p and there are
numbers k and 1 £ m < p such that kpq = m^{2}+1.]
Prove the results of Section 2.6
using minimal counterexamples, and also using descending sequences.
Explain where excluded middle and König's Lemma are needed when
using these forms of induction.
Suppose that finitely many types of polygonal tile
are given, with the property that a disc of arbitrary radius may be covered
with copies of the tiles, without overlaps. Using König's Lemma (Corollary
2.5.10), show that the whole plane (R^{2}
) may be covered.
Let \prec be a decidable binary relation with
no cycles on a finite set. Show that it is well founded ( cf Corollary
2.5.11). [Hint: consider the number of
descendants of each element and use Proposition
2.6.2.]
Show directly that the interleaved product relation
(Proposition 2.6.9) is well founded. Investigate
whether any of the three product relations have well founded analogues
for infinite families of sets. Is the order of potential words in a dictionary
well founded?
Show that the lexicographic product of two transitive
relations is transitive, and similarly for the trichotomy law.
Find an example of a union of well founded relations
which is not well founded, to show that lower is necessary
in Proposition 2.6.6.
Let f:(X, < )® (Y,\prec ) be a function
between sets with binary relations which is (non-strictly) monotone
in the sense that
x¢ < x Þ fx¢\prec fx Ú fx¢ = fx
where (Y,\prec ) is well founded. Suppose that every set
f^{-1}[y] Ì (X, < ) is well founded. Show that X is also well founded.
Using proof boxes, show that the transitive closure
of a well founded relation is also well founded (Theorem
3.8.11)
Write a program to check for repeats in a list.
Let f:X\twoheadrightarrow Y be any surjective
function between sets. Show that
mapf:List(X) \twoheadrightarrow List(Y) (Example
2.7.6(d)) and deduce that a finite set of
witnesses may be chosen without invoking the axiom of choice (Definition
1.8.8).
Show that for the Church numerals (Example
2.4.1), the terms
succ = ln.lx.lf.f(nxf) rec = lx.ls.ln.nx(lx.sxn)
define the successor and primitive recursion operator:
recxs 0\leadsto xrecxs (succn)\leadsto s(recxsn).
[For any type a, put
N = a® (a® a)® a ; then n:N, x,x:a, f,x:a® a,
succ:N® N and
rec:a® (a® a)® N® a.] Show that
(m+n) = recmsucc and similarly define multiplication and other
arithmetical functions, cf Remark
2.7.7 and Example
2.7.8.
Show that if a is the n-element set then
the Church numerals of type a® (a® a)® a
up to M+n-1 are distinct, but that afterwards they repeat with period M,
where M is the least common multiple of 1,2,¼,n. Estimate M.
Show how recursive programs such as factorial of the
form
p(0) = xp(n+1) = s(p(n),n)
can be written without using the argument n in the evaluation phase.
[Hint: what is the recursive definition of q(n) = p(n),n?]
A set X is Dedekind-infinite if there
are an element x Î X, a subset U Ì X with x Ï U and
an injection s:X\hookrightarrow U. Show that (X,x,s) is exactly
a model of the first four Peano axioms (Definition
2.7.1). Using powerset and comprehension
but not the existence of N, show that X contains a definable
model of all five axioms.
Show that
"l.rotate( length(l),l) = l, where
omitted eqnarray* environment
Justify the following binary list induction scheme:
omittedprooftreeenvironment
Consider the language of higher order predicate calculus
with only the connectives " and Þ . Show that
the formulae on the right hand side of Proposition
2.8.6 satisfy the introduction and elimination
rules for the other connectives.
Prove Proposition 2.8.7,
that
x = y \dashv \vdash "q.q[x]Û q[y], making clear where the congruence rules are used. Express
the proof in such a way as to make equality a derived connective. By substituting
the two-way formula for q, show that the result remains true
with one-way implication:
"q.q[x]Þ q [y].
Show that W satisfies Exercise
1.10(d) but that (c) gives excluded middle.
If you know some sheaf theory, show that (b) fails in
Shv( R).
Let i:W\hookrightarrow W. Show
that "x.i(x)Þ (x = i(T)). On the assumption
that i(i(T)) = T, show that i^{2} = id and
i(x) = (x = i( T)). Without this assumption, deduce that
i(x) = [i(i(T))Ù( x = i(T))]. By computing i(T) and i^{3}(T), show that
the assumption is redundant.