Practical Foundations of Mathematics

Paul Taylor

2.9  Exercises II

1. 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.

2. 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.

3. The volume-flow (in m³ s^-1 ) down a pipe of radius r of a liquid under pressure p is chⁿr^mp^k for some dimensionless c, where h is the dynamic viscosity, in units of kg m^-1 s^-1. Find n, m and k.

4. 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.

5. Express Ö2, Ö3 and Ö6 as Dedekind cuts, and hence show that Ö2·Ö3 = Ö6.

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₁È\typeN₂ and (the upper closure of) \typeW₁È\typeW₂ define a Dedekind cut of R. Calling it x y, verify the usual laws for multiplication, without using case analysis [Con76].

7. 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].

8. Show how to add Cauchy sequences and to multiply them by rational numbers.

9. Show how to reduce a Cauchy sequence of reals ( ie of Cauchy sequences) to a Cauchy sequence of rationals [Hint: diagonalise].

10. Define multiplication of Cauchy sequences, without using a case analysis according to sign.

11. 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[(\argan),(L,U)]Ùf[(\argbn),(L,U)] Û (\argan ) ~ (\argbn).

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

12. Explain the difference between p(U) in Example  2.1.5 and \funf_!(U) in Remark  2.2.7.

13. 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₀ = f and [f,g]on₁ = g.

14. Using the isomorphism P(X+Y) º P(X) xP(Y), construct the product Xx Y from powersets and disjoint unions. [Hint: consider those U Ì X+Y with exactly one element in each component.]

15. 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.)

16. Any predicate f[x] gives rise to an equivalence relation ~ on {0,1}x X 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.

17. 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.

18. 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.

19. For x,y,x¢,y¢ Î Z, write

    KWP(x,y) = {{x},{x,y}} Î P2(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 = y versus x ¹ y. Give the functional relations P²(Z)\leftharpoondown \rightharpoonup Z defining the product projections p₀ and p₁. Hence for X,Y Ì Z show that {KWP(x, y)|x Î XÙy Î Y} Ì P²(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).

20. Explain how Pⁿ(N) Ì P^m( N) for n £ m. Using Exercises 2.17 and 2.19, show that the types U with U Ì Pⁿ(N) for some n Î N form a model of pure Zermelo type theory. It is known as the von Neumann hierarchy V_w2 .

21. Give the l-terms which define the isomorphism between X and X¹x1^X, and verify that they are mutually inverse.

22. 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.

23. A (raw) l-term is in head normal form if it looks like

    ly1.ly2.¼lyn.x\argu1\argu2¼ \argum,

    where x is either a constant or a variable, possibly one of the y_i, and no sub-sequence x \argu₁¼\argu_k is a d-redex. Show that a term is in normal form iff it is hereditarily head normal.

24. 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.x y)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.

25. Show that a-conversion is unavoidable in the reduction of the untyped term (lx.x x)(lx, y.x y).

26. Combinatory algebra is given by one binary operation called application and two constants S and K with laws Sx y z = x z(y z) and Kx y = x (Example 2.4.2). Show functional completeness, that any term p in variables x₁,¼, x_n is equivalent to some fx₁x₂···x_n, where f is a term with no (free) variables. [Hint: by structural recursion, use

    u = (K u)x    and    (ux)(vx) = (S u v)x

    to eliminate x_n first and similarly the other variables.] Translate the term T = lx, y, z.x z y.

27. 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₁,¼,a_n then a₁Þ ···Þ a_n Þ f is provable under no hypothesis. This says that each instance of the (Þ Á )-rule is derivable in this calculus.

28. Suppose that X^R\triangleleft R, ie j: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.

29. 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.

30. 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.

31. Show that Peirce's law, ((qÞ f)Þ q)Þ q (Remark  2.4.10), excluded middle and the restart rule are intuitionistically equivalent.

32. What, in a word, is a well founded functional relation?

33. (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 k p q = m²+1.]

34. 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.

35. 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² ) may be covered.

36. 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.]

37. 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?

38. Show that the lexicographic product of two transitive relations is transitive, and similarly for the trichotomy law.

39. 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.

40. 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.

41. Using proof boxes, show that the transitive closure of a well founded relation is also well founded (Theorem  3.8.11)

42. Write a program to check for repeats in a list.

43. 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).

44. Show that for the Church numerals (Example  2.4.1), the terms

    succ = ln.lx.lf.f(nx f)    rec = lx.ls.ln.nx(lx.sxn)

    define the successor and primitive recursion operator:

    rec x  s  0\leadsto x       rec x   s  (succ n)\leadsto s(rec x  s  n).

    [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) = rec  m succ and similarly define multiplication and other arithmetical functions, cf Remark  2.7.7 and Example  2.7.8.

45. 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.

46. Show how recursive programs such as factorial of the form

    p(0) = x       p(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?]

47. 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.

48. Prove by list induction that

    read(write(l,m,a),n) = omitted casearray environment

    omitted eqnarray* environment

49. Show that "l.rotate( length(l),l) = l, where omitted eqnarray* environment

50. Justify the following binary list induction scheme:

    omitted prooftree environment

51. 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.

52. 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].

53. 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).

54. Let i:W\hookrightarrow W. Show that "x.i(x)Þ (x = i(T)). On the assumption that i(i(T)) = T, show that i² = 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³(T), show that the assumption is redundant.