Practical Foundations of Mathematics

Paul Taylor

1.9 Exercises I

When Bo Peep got too many sheep to see where each one was throughout the day, she found a stick or a pebble for each individual sheep and moved them from a pile outside the pen to another inside, or vice versa , as the corresponding sheep went in or out. Then one evening there was a storm, and the sheep came home too quickly for her to find the proper objects, so for each sheep coming in she just moved any one object. She moved all of the objects, but she was still worried about the wolf. By the next morning she had satisfied herself that the less careful method of reckoning was sufficient. Explain her reasoning without the aid of numbers.
For each of the connectives and quantifiers, give the phrases in English and any other language you know which usually express them. Point out any ambiguities, and how they are resolved in everyday usage.
Now give in logical notation the literal and intended meanings of the following, choosing appropriate abbreviations for the atomic predicates:

All farmers don't have cows. The library has some books by Russell and Whitehead. All passes must be shown at the gate. Dogs must be carried on the escalator. You hit me and I'll hit you.
The following equations are familiar in elementary algebra. Which of $x, "x and {x|·} ·· are understood?

(x+y)² = x²+2x y+y² ax²+bx+c = 0 x²+y² = 1
Show that reductions in the Lineland Army (Example 1.2.7) are locally confluent. Equivalently, show that (;) is associative.
A Turing machine [ Tur35] consists of a head, which may be in any of a finite number of states, and a tape which extends infinitely in both directions and is divided into cells (indexed by Z), each of which contains one symbol from a finite alphabet. All but finitely many cells contain the blank symbol. For each state in which the head may be, and for each symbol which may be written in the cell currently being read, there is specified a new state, a new symbol and a direction of motion (left or right). Show how to express a Turing machine as a rewrite system. [Hint: the root has the state and the current symbol as two of its arguments; the other two are the left and right parts of the tape, which must be expressed using the blank and one binary operation.] Since computation can only proceed in one place, the head has been called the von Neumann bottleneck.
Express confluence (Definition 1.2.5) as a formula involving (", Ù, Þ , \leadsto and) $. Using proof boxes - in particular the ($E )-rule - show that R satisfies the property iff R^op;R Ì R;R^op.
Prove Theorem 1.2.9 about local confluence.
Show that the formulae

$x. æ
è f[x]Ù"y.(f[y]Þ x = y) ö
ø

$x."y. æ
è f[y]Û x = y ö
ø

æ
è $x.f[x] ö
ø Ù æ
è "x."y. f[x]Ùf[y]Þ x = y ö
ø

are inter-provable. Use them to derive idiomatic proof-box rules for $!.
Suppose that ``x is a widget'' and ``x is a gadget'' are descriptions. Show that: the widget is the gadget iff the gadget is the widget.
Consider the formulae

(a)

"x, y, z.z = yÚy = zÚz = x;

(b)

\lnot \lnot "x, y, z.z = yÚy = zÚz = x;

(c)

"x, y, z.(\lnot \lnot z = y)Ú(\lnot \lnot y = z) Ú(\lnot \lnot z = x);

(d)

"x, y, z.\lnot \lnot (z = yÚy = zÚz = x).

Show that (a) is the strongest and (d) the weakest, and that any other formula obtained by inserting \lnot \lnot (other than between "x, "y and "z) is equivalent to one of these. Restate the weakest using Ù instead.
Devise formulae similar to those of the previous exercise to say that f has exactly three, four, ..., solutions. By adjoining a condition that f and y have no common solutions (Example 2.1.7), interpret the equations 1+1 = 2, 1+2 = 3 and 2+2 = 4 and prove them using the box method. (1+1 = 2 is proved in this sense on page 360 of Principia Mathematica.)
What, if anything, do the negations of x Î FV(t) (Definition 1.1.3), x:X (Notation 1.3.3) and x Î U (Definition 2.2.3) mean?
Show that f(x) = f(y) defines an equivalence relation on X, where f:X® Y is any function.
Show that a relation R:X\leftharpoondown \rightharpoonup Y is total and functional iff the composite R \hookrightarrow XxYp₀® X is bijective. So functions X® Y correspond to sections i of p₀, ie such that i;p₀ = id (Definition 1.3.12).
List the sixteen cases where the functional, total (entire), injective and surjective conditions do and do not hold for a binary relation. For each case give an example and, where possible, a name and notation; three less familiar ones represent overlap, subquotient and its converse.
Show that a relation R:X\leftharpoondown \rightharpoonup Y is functional iff RoR^op Ì id, total iff also id Ì R^opo R, injective iff R^opo R Ì id and surjective iff id Ì RoR^op. Hence prove Lemma 1.3.11. Show also that a function f is injective iff it is a monomorphism: \fung₁;f = \fung₂;fÞ \fung₁ = \fung₂, and surjective iff it is an epimorphism: f;\fung₁ = f;\fung₂Þ \fung₁ = \fung₂; cf Proposition 5.2.2(d).
Describe the sixteen cases for a binary (endo)relation where reflexivity, symmetry, transitivity and functionality do and do not hold, noting those for which idempotence necessarily holds.
Let R:n\leftharpoondown \rightharpoonup m be a decidable relation between two finite sets. Write [`(R)] for the (nxm) matrix with 1 in the (i,j)-position if iRj and 0 otherwise. Compare the matrix product [`(R)]·[`(S)] with the relational composition [`(R;S)].
Show that the sequent G\vdash q is provable in the sequent calculus iff q is provable from hypotheses G in the box style.
Describe the introduction and elimination rules for \lnot and Û by adapting those for Þ and Ù. In each case prove that the derived rules are equivalent, and describe the verbal mathematical idioms which express them.
Show that

(a)

Ú, Ù and Û are commutative and idempotent;

(b)

Ú and Ù are associative;

(c)

the boxes for ("Á ), (Þ Á ) and ($E ) may be interchanged.

What can be done with (ÙÁ ) and (ÚE )?
We tend to abuse Û transitively, so that f Û yÛ c means (fÛ y)Ù(yÛ c), but why is this an abuse?
Prove the following by the box method. Make it clear where any formulae are imported into boxes (Lemma 1.6.3). omitted eqnarray* environment where x Ï FV(y).
In linear implicational logic the only structural rules are identity, cut and exchange ( not weakening and contraction). Contexts are then bags (unordered lists), not sets. There is only one connective (Þ , but it is usually written \multimap ), obeying the sequent form of (Þ Á ) and

omitted prooftree environment

Using ideas of double-entry bookkeeping, develop a box style of proof (like that in Section 1.5) which is sound for this logic. [Hint: the reasons or credit column must cite the two formulae which are used in each (\multimap E ), and there must also be a debit column which records where the present formula is used.] Replace the cross-references by arrows ( proof nets) and \multimap by a ternary node with one outgoing and two incoming arrows. Show that the boxes are then redundant, and investigate the dynamical behaviour when (\multimap E ) and (\multimap Á ) meet.
(Only for those who already know linear logic.) Extend the proof box method to the connectives Ä, Å and &, giving the translations into and from the sequent, l-calculus and proof net approaches.
Writing (in modern notation)

= 2pt omitted array environment

prove Aristotle's syllogisms,

= 2pt omitted array environment
Write the direct and indirect rules of propositional logic in the style of Hilbert (Remark 1.6.10). Using steps of the form "[(x)\vec].ÙGÞ f , extend this to the quantifiers (this wasn't how Hilbert did it).
Formulate and prove the soundness of the rules of natural deduction with respect to a truth values semantics.
An assertion is immediate if it is the conclusion of an applicable rule, ie it may be deduced with no mediating argument. Give examples of mathematical arguments which are obvious but not immediate and vice versa (page 1.7), and also trivial topics (page def trivial) .
Using Remark 1.6.2, translate the proof of Lemma 1.6.6 (that composition preserves functionality and totality) into the vernacular.
Using the (e-d) definition of continuity R® R, show as a proof box that the composite gof of two such functions is continuous.
Why may we assume in Remark 1.7.9(c) that a hypothesis of the form $x. f[x] is used exactly once in a proof, ie with just one witness?
Show how to extend Fact 1.7.1 to fÚy and $x.f[x] in the database, though the proof is no longer uniform. This requires us to use fÚy as soon as possible, contrary to Remark 1.7.9(e); can our Remark be justified?
Devise heuristics which use axioms of the forms x Þ (fÚy) and xÞ $x.f[x ]. Why must the new goal x be put at line 50 and new data (fÚy or $x.f[x]) at line 51, instead of their usual places at the bottom and top of the box? Give examples of theorems (in analysis, for example) whose statements are of this form. What are the idioms for dividing up arguments in which such theorems are used?
Show that f is decidable iff fÚ\lnot f is \lnot \lnot -closed, and then f itself is also \lnot \lnot - closed. Show that de Morgan's law gives (\lnot f)Ú(\lnot \lnot f), so under this assumption every \lnot \lnot -closed formula is decidable.
Write out the truth tables for the two sides of de Morgan's laws and the distributive laws. Show that if two propositional formulae have the same truth table then they are classically inter-provable.
Express each of \lnot , Ú, Ù and Þ in terms of either nand (the Sheffer stroke) or nor.
Write down the formulae for the sum and carry bits in the binary addition of two single-bit numbers (0+0 = 00, 0+1 = 01, 1+0 = 01 and 1+1 = 10). By expressing them in terms of nor, give a circuit for a half adder. Show how to add two n-bit binary numbers; why is the half adder so called?
Show that every surjective function p:X \twoheadrightarrow Y has a section i:Y\hookrightarrow X such that i;p = \id_Y iff the axiom of choice (Definition 1.8.8) holds. [Hint: cf Exercise 1.14.]
Let w be any proposition whose truth-value you know but which others may dispute, such as ``July is in the winter.'' Suppose that W, the type of truth values, consists of true, false, w and \lnot w (with apologies to tropical readers). This supposition is consistent with most of pure mathematics. Explain how it is still the case that W is the two-element set {T,^}. What element of this set is w? Where would you have to be to observe W as a four-element lattice?