Exercise 8.5
Identify the definitions in the following text and rewrite the text in a formal form, using exclusively the definition format, as demonstrated in Figure 8.8. Assume that $\mathbb{R}$ is a type. Employ the flag format and the set notation $\{x : \mathbb{R} | P x\}$.
‘The real number $r$ is rational if there exist integer numbers $p$ and $q$ with $q \ne 0$ such that $r = p/q$. A real number that is not rational is called irrational. The set of all rational numbers is called $\mathbb{Q}$. Every natural number is rational. The number 0.75 is rational, but $\sqrt{2}$ is irrational.’
The following is the flag format version of the given text.
Note: In line (6) the definition rational is used with an argument that is a natural number, $n : \mathbb{N}$. However the definition of rational at line (3) specifies the argument needing to be of type $\mathbb{R}$. This could be a type-mismatch but we can overlook this because natural numbers are a subset of the real numbers, and so $n \in \mathbb{R}$ .
