Exercise 8.2
The formal text represented below in flag format, is about a number of well-known notions in analysis, containing some statements with omitted proofs.
(a) Translate the text into a more usual format, as you might find in a textbook. (Note: $∃^1$ expresses unique existence; ‘there exists exactly one ...’.)
(b) Which of the eight lines are formalised definitions? Which are formalised mathematical statements?
(c) Which constants have been introduced in the text and which constants will have been introduced before?
(d) Underline all instantiations of parameter lists in the formal text and explain accurately what has been instantiated for what, and why that is correct.
(a) For a set $V \subseteq \mathbb{R}$, a subset of the real numbers,
(1) $V$ is bounded from above if there exists a $y \in \mathbb{R}$, such that for all $x \in \mathbb{R}$, it is true that $ x \in V \implies x \le y $.
(2) For a given $s \in \mathbb{R}$, $s$ is an upper bound of $V$ if for all $x \in R$, it is true that $ x \in V \implies x \le s $.
(3) For a given $s \in \mathbb{R}$, $s$ is a least upper bound of $V$ if $s$ is an upper bound and for all $x \in \mathbb{R}$ it is true that $ x < s $ implies that $x$ is not an upper bound of $V$.
(4) If $V$ is non-empty, and $V$ is bounded from above, then there exists exactly one $s \in \mathbb{R}$ that is the least upper bound of $V$.
(5) $S$ consists of elements $x$ which are elements of $\mathbb{R}$, where each element $x$ is of the form $\frac{n}{n+1}$ where $n$ is some natural number.
(6) That set $S$ is a subset of $\mathbb{R}$.
(7) That set $S$, which is a subset of $\mathbb{R}$, is bounded from above.
(8) The number 1 is the (only) least upper bound of the set $S$, which is a subset of $\mathbb{R}$,
(b) All the eight lines are formalised definitions because formalised mathematical statements are equivalent to formalised definitions, as explained in Chapter 8 section 9.
However, it can be practical to consider a distinction between a definition that is general in application, and a mathematical statement about specific objects. In this case lines (1), (2), and (3) can be considered formalised definitions, and (4), (5), (6), (7) and (8) considered formalised mathematical statements about specific objects, here $S$ and $s$.
(c) All constants are introduced in the text, except the following which are introduced before: $*_s, *_p, \mathbb{R}, \mathbb{N}, \emptyset$.
We could argue that $\exists, \exists^1, \forall$ are also constants referencing a lambda-expression, which we've seen in earlier chapters.
(d) The following shows instantiations of parameter lists,
Let's discuss each relevant line.
(3) $upper \text{-} bound(V,u,s)$ is defined in line (2), and in line (3) has $V$ instantiated for $V$, $u$ for $u$, and $s$ for $s$.
(3) The second instance of $upper \text{-} bound$ has $V$ instantiated for $V$, $u$ for $u$, and this time $x$ for $s$. Here $x$ has the compatible type $\mathbb{R}$, and here makes sense as the upper bound refers to all $x \in \mathbb{R}$, albeit $x<s$,
(3) $bounded \text{-} from \text{-} above(V,u)$ is defined in line (1), and here has $V$ instantiated for $V$, and $u$ for $u$.
(4) $least \text{-} upper \text{-} bound(V,u,s)$ is defined in line (4), and here has $V$ instantiated for $V$, $u$ for $u$, and $s$ for $s$.
(7) Here $bounded \text{-} from \text{-} above(S,p_6)$ has $S$ instantiated for $V$, and $p_6$ instantiated for $u$. This is because the relevant set is $S:= \ldots :*_s$, and $p_6$ is a proof that $S$ is a subset of $\mathbb{R}$.
(8) Here $least \text{-} upper \text{-} bound(S, p_6, 1)$ has $S$ instantiated for $V$, and $p_6$ instantiated for $u$, and 1 for $s$. This is because the relevant set is $S:= \ldots :*_s$, and $p_6$ is a proof that $S$ is a subset of $\mathbb{R}$. The 1 is the specific element of $\mathbb{R}$ the proof $p_8$ makes an assertion about.
