Chapter 9 - Exercise 10

Let $\mathcal{J}_1, \ldots, J_n$ be judgements such that, listed in this order, they form a derivation. Let

$$ \mathcal{J}_n \; \equiv \;  \Delta_n \; ; \; \Gamma_n \; \vdash \; M_n \; : \; N_n \; \mid \; J_n $$

be the final judgement in this derivation, with $J_n$ its justification in $λD_0$.

Assume that for all $i < j$: if $\mathcal{J}_i \equiv \Delta_i ; \Gamma_i \vdash M_i : N_i$, then we have that $\Delta_i \; ; \; \Gamma_i \; \vdash \; *: \Box$.

(a) Let $J_n$ be a case of the (weak)-rule. Prove that

$$\Delta_n \; ; \; \Gamma_n \; \vdash \;  *: \Box$$

(b) The same if $J_n$ is a case of the (var)-rule.

(c) The same if $J_n$ is a case of the (def)-rule.

(d) The same if $J_n$ is a case of one of the other $λD_0$-rules as given in Figure 9.3.

(a) If $J_n$ is the (weak) rule then it must be the case that

$$ (\textit{weak}) \quad \frac{\Delta_n ; \Gamma_n^{\prime} \vdash M_n:N_n \quad \Delta_n;  \Gamma_n^{\prime} \vdash C:s}{\Delta_n ; \Gamma_n \vdash M_n:N_n} \quad \text{ where } x \notin  \Gamma_n^{\prime} $$

where $\Gamma_n \equiv  \Gamma_n^{\prime}, x:C$, and $s=*$ or $s=\Box$. 

The first premise $\Delta_n ; \Gamma_n^{\prime} \vdash M_n:N_n$ must have been derived before $\mathcal{J}_n$. By the given assumption, this means $\Delta_n ; \Gamma_n^{\prime} \vdash *:\Box$. 

Using the (weak) rule

$$ (\textit{weak}) \quad \frac{\Delta_n ; \Gamma_n^{\prime} \vdash *:\Box \quad \Delta_n;  \Gamma_n^{\prime} \vdash C:s}{\Delta_n ; \Gamma_n \vdash *:\Box} \quad \text{ where } x \notin  \Gamma_n^{\prime} $$

This is the conclusion we desire.

(b) If $J_n$ is the (var) rule then it must be the case that

$$ (\textit{var}) \quad \frac{\Delta_n ; \Gamma_n^{\prime} \vdash N_n:s}{\Delta_n ; \Gamma_n \vdash M_n:N_n} $$

where $\Gamma_n \equiv  \Gamma_n^{\prime}, M_n:N_n$, and $s=*$ or $s=\Box$. 

The premise $\Delta_n ; \Gamma_n^{\prime} \vdash N_n:s$ must have been derived before $\mathcal{J}_n$. By the given assumption, this means $\Delta_n ; \Gamma_n^{\prime} \vdash *:\Box$.

Using the (weak) rule

$$ (\textit{weak}) \quad \frac{\Delta_n ; \Gamma_n^{\prime} \vdash *:\Box \quad \Delta_n;  \Gamma_n^{\prime} \vdash N_n:s}{\Delta_n ; \Gamma_n \vdash *:\Box} \quad \text{ where } x \notin  \Gamma_n^{\prime} $$

This is the conclusion we desire.

(c) If $J_n$ is the (def) rule then it must be the case that

$$ (\textit{def}) \quad \frac{\Delta_n^{\prime};\Gamma_n \vdash M_n:M_n \quad \Delta_n^{\prime} ; \bar{x}:\bar{A} \vdash C:D} {\Delta_n ; \Gamma_n \vdash M_n:N_n} \quad \text{ if } a \notin \Delta $$

where $\Delta_n \equiv \Delta_n^{\prime},\bar{x}:\bar{A} \triangleright a(\bar{x}) := C:D$. 

The first premise $\Delta_n^{\prime};\Gamma_n \vdash M_n:M_n$ must have been derived before $\mathcal{J}_n$. By the given assumption, this means $\Delta_n^{\prime};\Gamma_n \vdash *:\Box$. 

Using the (def) rule

$$ (\textit{def}) \quad \frac{\Delta_n^{\prime};\Gamma_n \vdash *:\Box \quad \Delta_n^{\prime} ; \bar{x}:\bar{A} \vdash C:D} {\Delta_n ; \Gamma_n \vdash *:\Box} \quad \text{ if } a \notin \Delta $$

This is the conclusion we desire.

Note: This exercise is suggesting that correctness is preserved by the $\lambda D_0$ derivation rules.

(d) As an edge case, we'll try the (sort) rule.

If $J_n$ is the (sort) rule then it must be the case that

$$ (\textit{sort}) \quad \emptyset ; \emptyset \vdash *:\Box $$

This is the desired conclusion, with $\Delta = \emptyset, \Gamma = \emptyset$. 

Chapter 9 - Exercise 9

Let $Γ \equiv A : *, B : *, C : *$. Prove, by giving full derivations in $λD_0$:

(a) $\emptyset; \Gamma \; \vdash \; *:\Box$

(b) $\emptyset; \Gamma \; \vdash \; A : *$

(c) $\emptyset; \Gamma \; \vdash \; B : *$

(d) $\emptyset; \Gamma \; \vdash \; C : *$

The following derives all the results (a)-(d) in flag-format.

Chapter 9 - Exercise 8

See Exercises 9.6 and 9.7.

(a) Let $\Delta^{′} ≡ D_1, \ldots ,D_5$. Assume that $D_6$ is correct in environment $\Delta^{′}$ and

$$\Delta^{′} ; ∅ ⊢ (a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050) : *_p$$

Derive:

$$ \Delta ; ∅ ⊢ \texttt{formalprf}_6 : a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050 $$

(b) Assume that the conditions mentioned in Exercise 9.7(a) have been satisfied. What is the fastest manner to prove

$$D_1 ; f :  \mathbb{N} → \mathbb{R}, n :  \mathbb{N} ⊢ a_1(f,n) : \mathbb{R} $$

We remind ourselves of definitions $D_1$ to $D_6$:

$$\begin{align*} D_1 \; &≡ \; f : \mathbb{N} \to \mathbb{R}, \; n : \mathbb{N} \quad \triangleright \quad a_1(f,n) := \sum ^n_{i=0}(f i) : \mathbb{R} \\ \\ D_2 \; & ≡ \; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R} \quad \triangleright \quad a_2(f,d) := \forall _{n:\mathbb{N}}(f (n+1)−f n= d) : *_p \\ \\ D_3 \; & ≡ \; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \quad \triangleright \\ & a_3(f,d,u,n) := \texttt{formalprf}_3 : f n= f 0 + n \cdot d \\ \\ D_4 \; & ≡ \; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \quad \triangleright \\ & a_4(f,d,u,n) := \texttt{formalprf}_4 : a_1(f, n) = \frac{1}{2} \cdot (n+1) \cdot (f 0 + f n)  \\ \\ D_5 \; & ≡ \; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \quad \triangleright \\  & a_5(f,d,u,n) := \texttt{formalprf}_5 : a_1(f,n) = (n+1) \cdot f 0+ \frac{1}{2}\cdot n \cdot (n+1) \cdot d \\ \\  D_6 \; & ≡ \; \emptyset \quad \triangleright \quad a_6 := \texttt{formalprf}_6 : \sum^{100}_{ i=0} (i) = 5050 \end{align*}$$

(a) We're given $D_6$ is correct in environment $\Delta^{′}$. This means

$$\Delta^{\prime}, \emptyset \; \triangleright \; a_6 := \texttt{formalprf}_6 : \sum^{100}_{ I=0} (i) = 5050 \; ; \; \emptyset \; \vdash \; * : \Box $$

We're also given

$$\Delta^{′} ; ∅ ⊢ (a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050) : *_p$$

And we want to derive

$$  \Delta ; ∅ ⊢ \texttt{formalprf}_6 : a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050  $$

---

Let's consider the (inst) rule. The conclusion is a judgement $\Delta; \Gamma \vdash a(\bar{U}):N[\bar{x} := \bar{U}]$. Here the constant $a$ is $\texttt{formalprf}_6$ with no parameter list. The type $N$ is $\sum^{100}_{ i=0} (i) = 5050$. Noting that $\Gamma = \emptyset$, this gives us

$$ (\textit{inst}) \quad \frac{\Delta ; \emptyset \vdash *:\Box }{\Delta; \emptyset \vdash \texttt{formalprf}_6 : \sum^{100}_{ i=0} (i) = 5050} \tag{i} $$

where $\Delta = \Delta^{\prime}, D_6$. The first premise is true because we're given that $D_6$ is correct in the environment $\Delta^{\prime}$. There is no second premise as there are no parameters to the defined constant $\texttt{formalprf}_6$.

---

Next we want to show that $\sum^{100}_{ i=0} (i) = 5050$ is $βδ$-equivalent to $a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050$. 

$$ a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050  \quad  \triangleq _ \beta \quad \sum ^{100}_{i=0}(    i)  = (λx : \mathbb{N} . x)5050 \quad \triangleq _ \beta \quad \sum ^{100}_{i=0}(i)  = 5050 $$

That is,

$$ a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050  \quad \triangleq_\beta \quad \sum ^n_{i=0}(f i)  = 5050  \tag{ii} $$

---

We need the (def) rule to build the required second premise for the (conv) rule.

$$ (\textit{def}) \quad \frac{ \Delta^{\prime};\emptyset \vdash (a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050) : *_p  \quad \quad  \Delta^{\prime};\emptyset \vdash \texttt{formalprf}_6 : \sum^{100}_{ i=0} (i) = 5050 }{ \Delta ; \emptyset ⊢ (a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050) : *_p} \tag{iii}$$

where $\Delta = \Delta^{\prime}, D_6$. The second premise is intuitively true, but can be justified by another application of the (inst) rule as follows:

$$ (\textit{inst}) \quad \frac{\Delta^{\prime} ; \emptyset \vdash *:\Box }{\Delta^{\prime}; \emptyset \vdash \texttt{formalprf}_6 : \sum^{100}_{ i=0} (i) = 5050} $$

There is no second premise as there are no parameters to the defined constant $\texttt{formalprf}_6$.

---

We can now use the (conv) rule using result (ii), and result (iii) as the second premise.

$$ (\textit{conv}) \quad \frac{ \Delta; \emptyset \vdash \texttt{formalprf}_6 : \sum^{100}_{ i=0} (i) = 5050 \quad \quad  \Delta ; ∅ ⊢ (a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050) : *_p } {\Delta ; ∅ ⊢ \texttt{formalprf}_6 : a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050}$$

---

We have derived the required conclusion.

$$\Delta ; ∅ ⊢ \texttt{formalprf}_6 : a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050 \tag*{$\Box$}$$

(b) We want to prove to prove

$$D_1 ; f :  \mathbb{N} → \mathbb{R}, n :  \mathbb{N} ⊢ a_1(f,n) : \mathbb{R} $$

We assume that $D_1$ is correct in the empty environment. By exercise 9.7(a) this means the definiens and its type is derivable from the context of the definition.

The context of the definition matches the context of what we want to prove, namely $f :  \mathbb{N} → \mathbb{R}, n :  \mathbb{N}$.  The definition tells us that in this context, $a_1(f,n)$ has type $\mathbb{R}$. This what we want to prove, so we are done.

In effect, what we want to prove is defined to be true by the definition.

Chapter 9 - Exercise 7

We call a definition $D$ correct in environment Δ if $\Delta,D; \emptyset ⊢ *: \Box$.

Consider $D_1$ to $D_6$ as in Exercise 9.6.

(a) On what condition can you derive that $D_1$ is correct in environment $\emptyset$?

(b) How do you prove that $D_2$ is correct in environment $D_1$?

(c) The same question for $D_3$ in environment $D_1,D_2$.

We remind ourselves of the (def) rule:

$$ \frac{ \Delta ; \Gamma \; \vdash \; K:L \quad \quad  \Delta; \bar{x}:\bar{A} \; \vdash \; M:N }{ \Delta,  \bar{x}:\bar{A} \triangleright a(\bar{x}) := M:N ; \Gamma \; \vdash \; K:L} \quad \text{ if } a \notin \Delta $$

We also remind ourselves of definitions $D_1$ to $D_6$:

$$\begin{align*} D_1 \; &≡ \; f : \mathbb{N} \to \mathbb{R}, \; n : \mathbb{N} \quad \triangleright \quad a_1(f,n) := \sum ^n_{i=0}(f i) : \mathbb{R} \\ \\ D_2 \; & ≡ \; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R} \quad \triangleright \quad a_2(f,d) := \forall _{n:\mathbb{N}}(f (n+1)−f n= d) : *_p \\ \\ D_3 \; & ≡ \; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \quad \triangleright \\ & a_3(f,d,u,n) := \texttt{formalprf}_3 : f n= f 0 + n \cdot d \\ \\ D_4 \; & ≡ \; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \quad \triangleright \\ & a_4(f,d,u,n) := \texttt{formalprf}_4 : a_1(f, n) = \frac{1}{2} \cdot (n+1) \cdot (f 0 + f n)  \\ \\ D_5 \; & ≡ \; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \quad \triangleright \\  & a_5(f,d,u,n) := \texttt{formalprf}_5 : a_1(f,n) = (n+1) \cdot f 0+ \frac{1}{2}\cdot n \cdot (n+1) \cdot d \\ \\  D_6 \; & ≡ \; \emptyset \quad \triangleright \quad a_6 := \texttt{formalprf}_6 : \sum^{100}_{ I=0} (i) = 5050 \end{align*}$$

(a) Definition $D_1$ is correct in the empty environment $\emptyset$ if $D_1; \emptyset \vdash *: \Box$.

The (def) rule tells us the premises required to derive this.

$$ \frac{ \emptyset; \emptyset \; \vdash \; *:\Box \quad \quad  \emptyset; f : \mathbb{N} \to \mathbb{R}, \; n : \mathbb{N} \; \vdash \; \sum ^n_{i=0}(f i) : \mathbb{R} }{ \emptyset,  D_1 ; \emptyset \; \vdash \; *:\Box} $$

The first premise is simply the (sort) rule. The second premise requires the definition $D_1$ be well typed, that is, the definiens and its type can be derived from the context of the definition.

So the condition is that $D_1$ is well typed in the empty environment.

(b) Definition $D_2$ is correct in environment $D_1$ if $D_1, D_2 ; \emptyset \vdash *:\Box$. 

The (def) rule tells us the premises required to derive this.

$$ \frac{ D_1; \emptyset \; \vdash \; *:\Box \quad \quad  D_1; f : \mathbb{N} \to \mathbb{R},  d : \mathbb{R} \; \vdash \; \forall _{n:\mathbb{N}}(f (n+1)−f n= d) : *_p }{ D_1,  D_2 ; \emptyset \; \vdash \; *:\Box} $$

The first premise is the requirement that $D_1$ is correct in the empty environment, from part(a) above.

The second premise is the requirement that $D_2$ is well-formed in the environment $D_1$.

(c) Definition $D_3$ is correct in environment $D_1, D_2$ if $D_1, D_2, D_3; \emptyset \vdash *:\Box$. 

The (def) rule tells us the premises required to derive this.

$$ \frac{ D_1, D_2; \emptyset \; \vdash \; *:\Box \quad \quad  D_1, D_2; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \; \vdash \; \texttt{formalprf}_3 : f n= f 0 + n \cdot d }{ D_1,  D_2, D_3 ; \emptyset \; \vdash \; *:\Box} $$

The first premise is the requirement that $D_2$ is correct in the environment $D_1$. 

The second premise is the requirement that $D_3$ is well-formed in the environment $D_1, D_2$.

Chapter 9 - Exercise 6

Consider the following environment $\Delta$ consisting of six definitions, in which we use, for the sake of convenience, some well-known formats such as the $\Sigma$ and infix-notations:

$$ \begin{align} D_1 \; &≡ \; f : \mathbb{N} → \mathbb{R}, \; n : \mathbb{N} \quad \triangleright \quad a_1(f,n) := Σ^n_{i=0}(f i) : \mathbb{R} \\ \\ D_2 \; & ≡ \; f : \mathbb{N} →\mathbb{R}, \; d : \mathbb{R} \quad \triangleright \quad a_2(f,d) := \forall _{n:\mathbb{N}}(f (n+1)−f n= d) : ∗_p \\ \\ D_3 \; & ≡ \; f : \mathbb{N} →\mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \quad \triangleright \\ & a_3(f,d,u,n) := \texttt{formalprf}_3 : f n= f 0 + n \cdot d \\ \\ D_4 \; & ≡ \; f : \mathbb{N} →\mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \quad \triangleright \\ & a_4(f,d,u,n) := \texttt{formalprf}_4 : a_1(f, n) = \frac{1}{2} \cdot (n+1) \cdot (f 0 + f n)  \\ \\ D_5 \; & ≡ \; f : \mathbb{N} →\mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \quad \triangleright \\  & a_5(f,d,u,n) := \texttt{formalprf}_5 : a_1(f,n) = (n+1) \cdot f 0+ \frac{1}{2}\cdot n \cdot (n+1) \cdot d \\ \\  D_6 \; & ≡ \; \emptyset \quad \triangleright \quad a_6 := \texttt{formalprf}_6 : \sum^{100}_{ I=0} (i) = 5050 \end{align} $$

Assume that $\texttt{formalprf}_3$ to $\texttt{formalprf}_6$ are meta-terms, standing for real proof terms.

(a) Rewrite this environment in flag format.

(b) What is a name used for $a_2$ in the standard literature?

(c) Find the δ-normal form with respect to $\Delta$ of $a_5(λx : \mathbb{N}. 2x,2,u,100)$, where $u$ is an inhabitant of $a_2(λx : \mathbb{N}. 2x,2)$.

(a) The following is the environment in flag format.

(b) $a_2$ defines an arithmetic progression, where $d$ is the common difference.

(c) The definition $D_5$ is

$$  a_5(f,d,u,n) := \texttt{formalprf}_5 : a_1(f,n) = (n+1) \cdot f 0+ \frac{1}{2}\cdot n \cdot (n+1) \cdot d  $$

This means $a_5(λx : \mathbb{N}. 2x,2,u,100)$ is

$$  a_5(λx : \mathbb{N}. 2x,2,u,100) := \texttt{formalprf}_5 : a_1(λx : \mathbb{N}. 2x,100) = (100 + 1) \cdot (λx : \mathbb{N}. 2x) 0+ \frac{1}{2}\cdot 100 \cdot (100 + 1) \cdot 2  $$

Continuing by unfolding $a_1$,

$$  a_5(λx : \mathbb{N}. 2x,2,u,100) := \texttt{formalprf}_5 :  \sum _{i=0}^{100}((λx : \mathbb{N}. 2x)i) = (100 + 1) \cdot (λx : \mathbb{N}. 2x) 0+ \frac{1}{2}\cdot 100 \cdot (100 + 1) \cdot 2  $$

The above is the δ-normal form. 

Out of interest we can continue to simplify,

$$  a_5(λx : \mathbb{N}. 2x,2,u,100) := \texttt{formalprf}_5 : \sum _{i=0}^{100}(2i) = 10100  $$

That is,

$$ \texttt{formalprf}_5 \; : \; \sum _{i=0}^{100}(2i) = 10100 $$

Chapter 9 - Exercise 5

Check that all instantiations of the parameters of constants defined and used in Exercise 8.2 satisfy the requirements imposed by the (inst)-rule.

The following is the text used in Exercise 8.2.

The following summarises the derivation rules for $\lambda D_0$.

The (inst)-rule ensures that the substituted expressions $\bar{U}$ are derivable in the environment and context $\Delta; \Gamma$.

There are only two instantiations in Exercise 8.2, at line (7) and (8). Let's consider each in turn.

(7) In defining $p_7$, the type $\textit{bounded-from-above}(S,p_6)$ has instantiated

• $V$ as $S$
• $u$ and $p_6$

in that order.

The (inst)-rule requires that we can derive $S:*_s$ in $\Delta; \Gamma$. Indeed, line (5) of the environment establishes $S$ with type $*_s$.

Next, the (inst)-rule requires that we can derive $p_6: V \subseteq \mathbb{R}[V:=S]$ which is $p_6:S \subseteq \mathbb{R}$. Line (6) of the environment establishes $p_6$ with type $S \subseteq \mathbb{R}$. 

And so the instantiations of $\textit{bounded-from-above}(S,p_6)$ satisfy the requirements of the (inst)-rule.

(8) In defining $p_8$, the type $\text{least-upper-bound}(S, p_6, 1)$ has instantiated

• $V$ as $S$
• $u$ as $p_6$
• $s$ as 1

in that order.

The (inst)-rule requires that we can derive $S:*_s$ in $\Delta; \Gamma$. Indeed, line (5) of the environment establishes $S$ with type $*_s$.

Next, the (inst)-rule requires that we can derive $p_6: V \subseteq \mathbb{R}[V:=S]$ which is $p_6:S \subseteq \mathbb{R}$. Line (6) of the environment establishes $p_6$ with type $S \subseteq \mathbb{R}$. 

Finally, the (inst)-rule requires that we can derive $1:\mathbb{R}[V:=S, u:=p_6]$  which is simply $1:\mathbb{R}$. Determining the type of 1 as $\mathbb{R}$ requires no further work.

And so the instantiations of $\textit{least-upper-bound}(S,p_6,1)$ satisfy the requirements of the (inst)-rule.

Chapter 9 - Exercise 4

This question has been updated by the errata.

See Section 9.6. Add the following definition to $(D_1) \ldots  (D4)$:

$$ (D_5) \quad x: \mathbb{Z}, y: \mathbb{Z} \triangleright d(x,y) := (x+ y)^2 $$

Let $\Delta  ≡D_1, \ldots ,D_5$. Give the full δ-reduction diagram of $d(a(u,v),b(w,w))$.

The following diagram illustrates the δ-reduction of $d(a(u,v),b(w,w))$.

(click to enlarge)

The final result is

$$ d(a(u,v), b(w,w)) \; \triangleq \; (u^2 + v^2 + 2 w^2)^2 $$

Chapter 9 - Exercise 3

The text in Exercise 8.2 contains eight new definitions. Let $Δ$ be the corresponding environment. Rewrite the type in line (8) in such a manner that all definitions of $Δ$ have been unfolded.

Let's remind ourselves of the text in Exercise 8.2

The type in line (8) is

$$\textit{least-upper-bound}(S, p_6, 1)$$

Using (3) we have

$$\textit{upper-bound}(S, p_6, 1) \;  \land \; \forall x:\mathbb{R}. (x < 1 \implies \neg \textit{upper-bound}(S, p_6, x))$$

Using (2) we have

$$ \forall x: \mathbb{R}.(x \in S \implies x \le 1) \;  \land \; \forall x:\mathbb{R}. (x < 1 \implies \neg \forall y: \mathbb{R}.(y \in S \implies y \le x)  )$$

Note the use of $y$ to avoid clashing with $x$.

Using $(5)$ we have

$$\begin{gather*} \forall x: \mathbb{R}.(x \in  \{z:\mathbb{R} \mid \exists n : \mathbb{R}.(n \in \mathbb{N} \land z=\frac{n}{n+1} ) \}  \implies x \le 1) \\ \\  \land \\ \\ \forall x:\mathbb{R}. (x < 1 \implies \neg \forall y: \mathbb{R}.(y \in \{z:\mathbb{R} \mid \exists n : \mathbb{R}.(n \in \mathbb{N} \land z=\frac{n}{n+1} ) \}  \implies y \le x)  ) \end{gather*}$$

Chapter 9 - Exercise 2

Consider the following two definitions, $D_i$ and $D_j$:

$ \bar{x} \; : \;  \bar{A} \;  \triangleright \; a(\bar{x}) \; := \; K : L$

$ \bar{y} \; : \;   \bar{B} \; \triangleright \; b(\bar{y}) \; := \; M : N$

Let $Δ ; Γ ⊢ U : V$ and assume that $D_i$ and $D_j$ are elements of the list $Δ$, where $D_i$ precedes $D_j$.

(a) Describe exactly where the constant $a$ may occur in $D_i$ and $D_j$.

(b) Describe where the constant $b$ may occur in $Δ$.

(a) Since $D_i$ defines the constant $a$, it can only occur once in $D_i$ at the position of the definiendum. It cannot occur in the definiens, because we don't allow self-referencing definitions, which means it is not in $K$ nor in $L$. It cannot occur in $\bar{x}$ because it hasn't been defined at this point. 

Since $D_j$ occurs after $D_i$, the constant $a$ can occur anywhere in $D_j$, except as the definiendum because we can't redefine the constant $a$. So $a$ can occur in $\bar{B}$, $M$ and $N$.

(b) The constant $b$ can only occur after it has been defined. So it cannot occur anywhere in $\Delta$ before $D_j$, and that means it cannot occur in $D_i$ which occurs before $D_j$.

Chapter 9 - Exercise 1

Consider the environment $Δ ≡ D_1,D_2, D_3, D_ 4$ of Section 9.6. Describe the dependencies between the four definitions and give all possible linearisations of the corresponding partial order.

Let's remind ourselves of the environment $\Delta$.

$ (D_1) \quad x : \mathbb{Z},y : \mathbb{Z} \quad \triangleright \quad a(x,y) := x^2 +y^2 \quad : \quad \mathbb{Z} $

$ (D_2) \quad x : \mathbb{Z},y : \mathbb{Z}  \mathbb{Z} \quad \triangleright \quad b(x,y) := 2·(x·y) \quad : \quad \mathbb{Z} $

$ (D_3) \quad x : \mathbb{Z},y : \mathbb{Z}  \mathbb{Z} \quad \triangleright \quad c(x,y) := a(x,y)+b(x,y) \quad : \quad \mathbb{Z} $

$ (D_4) \quad x : \mathbb{Z},y : \mathbb{Z}  \mathbb{Z} \quad \triangleright \quad \textit{lemma}(x,y) := c(x,y) = (x+y)^2 \quad : \quad ∗_p $

Here, $D_3$ depends on $D_1$ and also $D_2$. There is no relation between $D_1$ and $D_2$. Furthermore, $D_4$ depends only on $D_3$.

There are two possible linearisation of the partial order:

$$ D_1 \leftarrow D_2  \leftarrow D_3 \leftarrow D_4 $$

$$ D_2 \leftarrow D_1  \leftarrow D_3 \leftarrow D_4 $$

Chapter 8 - Exercise 6

Exercise 8.6

Consider the following mathematical text:

‘If $k$, l and m are integers, $m$ being positive, then one says that $k$ is congruent to l modulo $m$ if $m$ divides $k−l$. We write $k ≡l(\mod  m)$ to indicate that $k$ is congruent to $l$ modulo m$.

Hence $−3 ≡17(\mod 5)$, but not $−3 ≡−17(\mod 5)$.

If $k ≡l(\mod m)$ then also $l ≡k(\mod m)$.

$k ≡l(\mod m)$ if and only if there is an integer $u$ such that $k= l+um$.’

(a) Rewrite the texts in a formal form, as a list of definitions. Assume that $\mathbb{Z}$ is a type. Employ the flag format. Formalise $k ≡l(\mod m)$ as $eqv(k,l,m,u)$, with$u$ a proof that $m$ is positive.

(b) Indicate the scopes of all variables and constants introduced in the formal text.

(c) Identify all instantiations of the parameter lists introduced in the formal text and check that the type conditions are respected.

(a) The following is a flag-format formalisation of the text.

Note the author's solution has $\implies$ instead of $\iff$ for line (6).

(b) The scopes of the variables and constants are as follows:

• $k,l,m$ have local scope lines (2) to (6).
• $u$ has local scope lines (3) to (6).
• $v, p_1, p_2$ have global scope.
• $\textit{eqv}, q, r$ have global scope.
• $n$ has scope limited to the expression $(k=l+nm)$ at line (6).

(c) The instantiations of introduced parameter lists are as follows:

• line (5) $\textit{eqv}(k,l,m,u)$ is an identity instantiation.
• line (5) $\textit{eqv}(l,k,m,u)$ is not an identity instantiation. The type of $l$ and $k$ match the introduced types $\mathbb{Z}$. The type of $m$ is the expected $\mathbb{Z}$. The type of $u$ is $m>0$ as expected.
• line (6)  $\textit{eqv}(k,l,m,u)$ is an identity instantiation.
• line (8)  $\textit{eqv}(-3, 17, 5, v)$ has $-3, 17, 5$ of the expected type $\mathbb{Z}$ and $v$ is of type $m>0$  with $m=5$.
• line (9)  $\textit{eqv}(-3, -17, 5, v)$ has $-3, -17, 5$ of the expected type $\mathbb{Z}$ and $v$ is of type $m>0$ with $m=5$.

Chapter 8 - Exercise 5

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}$ .

Chapter 8 - Exercise 4

Exercise 8.4

The following formal text in flag format is about some well-known notions in algebra, where ‘op’ means a binary operation on $S$, in Curried form (cf. Remark 1.2.6).

(a) Translate the text into a more usual format, as you might find in a textbook. Use infix notation when appropriate.

(b) Underline all variables that are bound to a binding variable introduced in the text.

(c) Rewrite lines (1) and (2) in the format $Γ \triangleright a(...) := M : N$ as described in Section 8.5.

(a) 

(1) Given a set $S$ and a binary operator op that takes two elements of $S$ and returns an element of $S$, then $(S,\textit{op})$ is a semigroup if for all $x, y, z \in S$

$$  x \textit{ op }     (y \textit{ op } z) \; = \;  (x \textit{ op } y) \textit{ op } z  $$

(2) Given a semigroup $(S,\textit{op})$, the element $e \in S$ is a unit if for all $x \in S$

$$ x \textit { op } e = x \quad \land \quad e \text{ op } x = x $$

(3) A semigroup $(S,\textit{op})$ is a monoid if there exists an element $e \in S$ that is a unit.

(4) The unit of a semigroup is unique. That is, if $e_1$ and $e_2$ are units of a semigroup then $e_1 = e_2$.

(b) The following shows all the bound variables.

(c) 

(1)

$$ S:*_s, \textit{op}:S \to S \to S \; \triangleright \;  \textit{semigroup}(S, \textit{op}) \; := \; \forall_{x,y,z:S} \left ( \textit{op} \; x \;  (\textit{op} \; y \; z) = \textit{op} \;  (\textit{op} \; x \; y) \; z \right ) \; : \; *_p $$

(2) 

$$ \begin{gather*} S:*_s, \textit{op}:S \to S \to S,  u:\textit{semigroup}(S, \textit{op}), e:S \; \triangleright \\ \\ \textit{unit}(S, \textit{op}, u, e) \; := \; \forall_{x:S} \left ( \textit{op} \; x \; e = x \land \textit{op} \; e \; x =x  \right )  \; : \; *_p  \end{gather*}$$

Chapter 8 - Exercise 3

Exercise 8.3

Consider the formal text in Exercise 8.2. Describe the partial order representing the dependencies between the definitions given in this text. (Cf. the end of Section 8.5.)

The following is the formal text in Exercise 8.2

There is a partial order because some definitions depend on others, but some don't. 

Let's first list the dependencies.

• $bounded\text{-}from\text{-}above$ does not depend on another definition
• $upper\text{-}bound$ does not depend on another definition
• $least\text{-}upper\text{-}bound$ depends on $upper\text{-}bound$
• $p_4$ depends on $least\text{-}upper\text{-}bound$
• $S$ does not depend on another definition
• $p_6$ depends on $S$
• $p_7$ depends on $bounded\text{-}from\text{-}above$ and $p_6$ (which depends on $S$)
• $p_8$ depends on $least\text{-}upper\text{-}bound$ (which depends on $upper\text{-}bound$) and $p_6$ (which depends on $S$)

The following summarises these dependencies visually.

We can see definitions like $S$ and $bounded\text{-}from\text{-}above$ do not depend on other definitions, but are depended on by other definitions.

We can also see some definitions like $p_7$ depend on more than one definition.

Finally, we can see there is no relation between $bounded\text{-}from\text{-}above$ and $S$. This is why the dependencies are a partial order.

Chapter 8 - Exercise 2

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.

Chapter 8 - Exercise 1

Exercise 8.1

In Section 8.7, we gave the name $p(m,n,u)$ to a proof of the proposition

$$∃x,y : \mathbb{Z}. (mx+ny = 1)$$

in the context $Γ ≡ m : \mathbb{N}^+, n : \mathbb{N}^+, u : coprime(m,n)$.

Assume that we have constructed, in context $m : \mathbb{N}^+, n : \mathbb{N}^+$, a proof (i.e. an inhabitant) $q(m,n)$ of the proposition

$$coprime(m,n) ⇒coprime(n,m)$$

Find an inhabitant of

$$∃x,y : \mathbb{Z}. (nx+my = 1)$$

in context $Γ$.

We start with $p$ which is the name given to the proof of the proposition

$$ \exists x,y : \mathbb{Z}. (mx+ny = 1) \tag{i}$$

The name also carries with it the ordered list of arguments $(m,n,u)$. The first two arguments are the positive natural numbers $n$ and $m$ expected by the proof. The third argument is a proof that the first two arguments, $m$ and $n$ (in that order), are co-prime.

We want to prove the proposition

$$ \exists x,y : \mathbb{Z}. (nx+my = 1) \tag{ii}$$

The order of $n$ and $m$ is different to (i), and this means $p(m,n,u)$ is not a proof of (ii).

We are given a proof $q(m,n)$ of the proposition $coprime(m,n) \implies coprime(n,m)$, that is

$$q(m,n) \; : \; coprime(m,n) \implies coprime(n,m)$$

So the proof $q(m,n)$ applied to $u$, the proof $coprime(m,n)$, gives us a proof $coprime(n,m)$.

$$ q(m,n)u \; : \; coprime(n,m)$$

We also check that the context of $q$ allows it to be used in the context in which we apply it to $u$, that is, $\Gamma$. The context of $q$ us a subset of $\Gamma$ so can be used, and it can be used with $u$ because $u$ is defined in $\Gamma$.

If we are to use $p$ as a proof of $∃x,y : \mathbb{Z}. (nx+my = 1)$, the order of the variables $n$ and $m$ require the proof to be of the form $p(n,m,?)$ and not $p(m,n,?)$. The $?$ a proof that $n$ and $m$ (in that order) are co-prime. We have that from above.

And so $p(n,m,q(m,n)u)$ is a proof of the proposition (ii). That is

$$ \Gamma \;  \triangleright \;  p(n,m,q(m,n)u) \; : \; \exists x,y:\mathbb{Z}.(nx + my = 1)$$

We can choose to give this proof a name, $r(m,n.u)$

$$ \Gamma \;  \triangleright \; r(m,n,u) \; := \;  p(n,m,q(m,n)u) \; : \; \exists x,y:\mathbb{Z}.(nx + my = 1)$$

Chapter 7 - Exercise 14

Exercise 7.14

Let $Γ ≡ S : *, P : S →*, Q : S →*$. Consider the following λC-expression:

$$\begin{gather}M ≡ λu : (∃x : S. (P x∧Qx)). λα : ∗. λv : (Πx : S. (P x →α)). \\ uα(λy : S. λw : (P y∧Qy). vy(w(P y)(λs : P y. λt : Qy. s)))\end{gather}$$

(a) Find a type $N$ such that $Γ ⊢M : N$.

(b) Which logical tautology is expressed by $N$ and proved by $M$?

(c) Give a derivation of $Γ ⊢M : N$.

(a) The following derives $M$ and in doing so, establishes $N$ as

$$(\exists x : S. (P x \land Qx)) \quad \to \quad \Pi \alpha:*.( (\Pi x:S.(Px \to \alpha)) \to \alpha)$$

(b) The logical tautology is 

$$\exists _{x \in S}(P (x) \land Q(x)) \; \implies \; \exists_{x \in S}(P(x))$$

That is, if there exists an $x$ in $S$ such that $P(x)$ and $Q(x)$ are true, then there exists an $x$ in $S$ such that $P(x)$ is true.

(c) A derivation is given above in (a).

Chapter 7 - Exercise 13

Exercise 7.13

Verify that the following expression is a tautology in constructive logic, by giving a flag-style derivation in λC:

$$ \exists_{x \in S}(P(x)) \quad \implies \quad  ( \; \forall_{y \in S}(P(y) \implies Q(y)) \implies \exists_{z \in S}(Q(z)) \; ) $$

Before we develop a derivation in λC it is educational to develop a natural deduction proof, because it will guide the λC derivation.

This answer on stack exchange is a helpful explanation of intro and elim rules for ∃ and ∀.

• https://math.stackexchange.com/questions/3115707/can-anyone-clarify-the-rules-for-forall-intro-and-elimination-and-exists#3115741

The corresponding type is

$$ \Pi \alpha : * . ((\Pi x : S. (P x \to \alpha )) \to \alpha) \quad \to \quad  \Pi y:S.(Py \to Qy) \quad \to \quad  \Pi \alpha : * . ((\Pi z : S. (Q z \to \alpha )) \to \alpha) $$

The following is a derivation in λC.

Chapter 7 - Exercise 12

Exercise 7.12

(a) Complete the derivation given in Section 7.5 that shows that the natural deduction rule (∃-intro-sec) is derivable in λC.

(b) Give a flag-style λC-derivation verifying the following tautology of classical logic:

$$¬∃_{x∈S}(¬P(x)) ⇒ ∀_{y∈S}(P(y))$$

(Hint: use part (a) and DN.)

(a) The natural deduction rule (∃-intro-sec) is.

$$ \frac{a : S \quad \quad P a}{\Pi \alpha :*. ((\Pi x : S. (P x \to \alpha)) \to \alpha)} $$

The following is a derivation in λC.

(b) The corresponding type is

$$ (\Pi \alpha :*. ((\Pi x : S. ((P x \to \bot)\to \alpha)) \to \alpha  ) \to \bot ) \; \to \; \Pi y:S.Py $$

The following is a derivation in λC.

Chapter 7 - Exercise 11

Exercise 7.11

Let $S : ∗$ and $P,Q : S →∗$. Let $y : Πα : ∗. ((Πx : S. (P x →α)) →α)$, $z : Πx : S. (P x →Qx)$ and $x : S$.

(a) Find a correct type for $y(Qx)$.

(b) Why is the application $y(Qx)z$ incorrect?

(c) Check that this results corresponds with Remark 7.5.2.

(a) We start with $Qx : *$. To avoid the $x$ in $Qx$ being captured by the $\Pi x:S$ in $y$, we should rename the variable $x$ to $z$. This gives us

$$ y(Qx) \; : \;  (Πz : S. (P z → Qx)) → Qx $$

(b) The function $y(Qz)$ takes an argument of type $Πz : S. (P z → Qx)$. 

The type of $z$ is $ Πx : S. (P x →Qx)$, which is different, and so $y(Qz)$ cannot be applied to $z$.

(c) This result supports Remark 7.5.2.