Chapter 5 - Exercise 7

Exercise 5.7

Prove that the following propositions are tautologies by giving shortened λP-derivations:

(a) $(A ⇒B) ⇒((B ⇒C) ⇒(A ⇒C))$

(b) $((A ⇒B) ⇒A) ⇒((A ⇒B) ⇒B)$

(c) $(A ⇒(B ⇒C)) ⇒((A ⇒B) ⇒(A ⇒C))$

(a) The type associated with $(A ⇒B) ⇒((B ⇒C) ⇒(A ⇒C))$ is

$$ \Pi x:(\Pi a:A.B).(\Pi y:(\Pi b:B.C).(\Pi a:A.C)) $$

By inspection, the inhabitant should be

$$ \lambda x:(\Pi a:A.B).(\lambda y:(\Pi b:B.C).(\lambda a:A.y(xa))) $$

The following is a shortened derivation in λP, first deriving the type, then the inhabitant.

(b) The type associated with $((A ⇒B) ⇒A) ⇒((A ⇒B) ⇒B)$ is

$$ \Pi x:(\Pi s:(\Pi a:A.B).A) . (\Pi t:(\Pi a:A.B).B) $$

By inspection, the inhabitant should be

$$ \lambda x:(\Pi s:(\Pi a:A.B).A) . (\lambda t:(\Pi a:A.B). t(xt)) $$

The following is a shortened derivation λP, first deriving the type, then the inhabitant.

(c) The type associated with $(A ⇒(B ⇒C)) ⇒((A ⇒B) ⇒(A ⇒C))$ is

$$ \Pi x:(\Pi a:A . (\Pi b:B.C)) . (\Pi y:(\Pi a:A .B).(\Pi a:A.C)) $$

By inspection, the inhabitant should be

$$ \lambda x:(\Pi a:A . (\Pi b:B.C)) . (\lambda y:(\Pi a:A .B). (\lambda a:A.xa(ya))) $$

The following is a shortened derivation in λP, first deriving the type, then the inhabitant.

Chapter 5 - Exercise 6

Exercise 5.6

Prove that $(A ⇒(A ⇒B)) ⇒(A ⇒B)$ is a tautology, (first) in natural deduction and (second) by means of a shortened λP-derivation.

Natural Deduction

The following is a natural deduction proof of the logical statement.

Full λP Derivation

Noting that the associated type for $A \implies B$ is $\Pi x:A.B$, then the type for the given logical statement is 

$$\Pi z:(\Pi y:A.(\Pi x:A.B)) . (\Pi x:A.B)$$

By inspection, a term that inhabits that type is

$$\lambda z:(\Pi y:A.(\Pi x:A.B)). (\lambda x:A. zxx)$$

The following is a full derivation, before we develop a shorted one below (click to enlarge).

Shortened λP Derivation

The following is a shortened derivation.

Chapter 5 - Exercise 5

Exercise 5.5

Prove that $A ⇒ ((A ⇒ B) ⇒ B)$ is a tautology by giving a shortened λP-derivation.

To show that $A ⇒ ((A ⇒ B) ⇒ B)$ is a tautology, we need to show that corresponding type is derivable and is also inhabited.

Full Derivation

The following is a flag notation derivation of both the type and the inhabitant. This is a full derivation before we develop a shortened derivation.

Shortened Derivation

The following is a shortened derivation.

Chapter 5 - Exercise 4

Exercise 5.4

Prove that * is the only legal kind in λP.

The set of kinds $\mathbb{K}$ is defined as

$$\mathbb{K} = * \; | \; \mathbb{K} \to \mathbb{K}$$

The textbook gives examples of kinds

$$∗, \; ∗→∗, \; ∗→∗→∗, \; (∗→∗) →∗, \; (∗→∗) →∗→∗, \; ∗→(∗→∗) →∗$$

For a kind $k$ to be legal, there must exist a context $Γ$ and type $t$ such that $Γ⊢k:t$.

All judgements are a result of the derivation rules for λP, given in Figure 5.1, so we can examine them to see how a judgement of the form $Γ⊢k:t$ can be derived.

The axiomatic (sort) rule $\emptyset \vdash *:\Box$ immediately tells us that * is a legal kind.

Using the definition of kinds, aside from *, all other kinds are arrow types of the form $\mathbb{K} \to \mathbb{K}$. All of them are derived from the simplest $* \to *$. If we can show that $* \to *$ is not derivable, then we have shown all the other kinds (except *) are not derivable.

The type $* \to *$ is only derived by the (form) rule. Note that $* \to *$ is an abbreviation of $\Pi x:*.*$.

$$(form) \quad \frac{Γ ⊢ A:* \qquad Γ, x:A ⊢ B:s}{Γ ⊢ \Pi x:A.B:s} \quad x \notin Γ$$

To form $\Pi x:*.*$, we must have $A=*$ and $B=*$. The first premise would then require $*:*$.

There is no derivation rule that results in $Γ ⊢*:*$, and so kinds aside from * are not derivable in λP.

Chapter 5 - Exercise 3

Exercise 5.3

Extend the flag derivation of Exercise 5.2(b) to a complete derivation of

$$S : *, Q : S →S →* ⊢ Πx : S. Πy : S. Qxy : *$$

The following is the flag derivation (click to enlarge).

Chapter 5 - Exercise 2

Exercise 5.2

Give a complete (i.e. unshortened) λP-derivation of

$$ S : ∗ ⊢ S →S →∗ : \Box $$

(a) in tree format,

(b) in flag format.

(a) The following shows the derivation in tree format.

$$(1) \; \emptyset \vdash * : \Box \quad (sort)$$

$$ \frac{(1) \; \emptyset \vdash * : \Box}{(2) \; S:* \vdash S:*} \quad (var)$$

$$ \frac{(1) \; \emptyset \vdash * : \Box \qquad (1) \; \emptyset \vdash * : \Box}{(3) \; S:* \vdash *:\Box} \quad (weak)$$

$$ \frac{(3) \; S:* \vdash *:\Box \qquad (2) \; S:* \vdash S:*}{(4) \; S:*, x:S \vdash *:\Box} \quad (weak)$$

$$ \frac{(2) \; S:* \vdash S:* \qquad (4) \; S:*, x:S \vdash *:\Box}{(5) \; S:* \vdash S \to *:\Box} \quad (form)$$

$$ \frac{(5) \; S:* \vdash S \to *:\Box \qquad (2) \; S:* \vdash S:*}{(6) \; S:*, x:S \vdash S \to *:\Box} \quad (weak)$$

$$ \frac{(2) \; S:* \vdash S:* \qquad (6) \; S:*, x:S \vdash S \to *:\Box}{(7) \; S:* \vdash S \to S \to *:\Box} \quad (form)$$

(b) The following shows the derivation in flag format.

Chapter 5 - Exercise 1

Exercise 5.1

Give a diagram of the tree corresponding to the complete tree derivation of line (18) of Section 5.3.

The following is a flag format derivation for easy reference.

And the following is a diagram corresponding to the tree derivation (click to enlarge).