Chapter 7 - Exercise 5

Exercise 7.5

As Exercise 7.2(b):

(a) $¬(A ⇒B) ⇒A$ (hint: use Exercise 7.1(b))

(b) $¬(A ⇒B) ⇒(A∧¬B)$ (hint: use Exercise 7.1(d))

As a reminder of exercise 7.2(b), we need to "verify that the following expression is a tautology in classical logic, by giving a corresponding flag-style derivation in λC (use DN)".

(a) The type corresponding to $¬(A ⇒B) ⇒A$ is

$$ ((A \to B) \to \bot) \to A $$

The following is a λC derivation of an inhabitant of this type.

(b) The type corresponding to $¬(A ⇒B) ⇒(A∧¬B)$ is

$$((A \to B) \to \bot) \to \Pi C:*.((A \to (B \to \bot) \to C) \to C)$$

The following is a λC derivation of an inhabitant of this type.

Chapter 7 - Exercise 4

Exercise 7.4

Give λC-derivations to show that the following natural deduction rules are derivable in λC (cf. Section 7.2,I):

(a) (∧-elim-left-sec),

(b) (∧-elim-right-sec).

(a) The (∧-elim-left-sec) rule is, in second order, 

$$\frac{\Pi C : ∗. (A \to B \to C) \to C}{A}$$

Our task is to find $?_2$ in the type theoretic version of this rule,

$$ \frac{\Gamma \vdash c : \Pi C : *. (A \to B\to C) \to C}{\Gamma \vdash ?_2 :A} $$

That is, given the context that the conjunction holds, we need to show that $A$ holds by finding an inhabitant.

The following is a λC derivation, showing that 

$$cA(\lambda x:A.\lambda y:B.x)$$

inhabits $A$ as a result of the given context which includes an encoding of the conjunction.

(b) The task for the  (∧-elim-left-sec) rule is, in second order, 

$$\frac{\Pi C : ∗. (A \to B \to C) \to C}{B}$$

Our task is to find $?_2$ in the type theoretic version of this rule,

$$ \frac{\Gamma \vdash c : \Pi C : *. (A \to B\to C) \to C}{\Gamma \vdash ?_2 :B} $$

The following is a λC derivation, showing that 

$$cB(\lambda x:A.\lambda y:B.y)$$

inhabits $B$ as a result of the given context which includes an encoding of the conjunction.

Chapter 7 - Exercise 3

Exercise 7.3

Give λC-derivations proving that the following expressions are tautologies in classical logic (so you may use DN or ET):

(a) $(A ⇒B) ⇒(¬B ⇒ ¬A)$

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

(a) The expression $(A ⇒B) ⇒(¬B ⇒ ¬A)$ is equivalent to the following type:

$$ (A \to B) \to ((B \to \bot) \to (A \to \bot)) $$

The following is a λC derivation.

Note this derivation didn't use DN or ET.

(b) The expression $(¬B ⇒ ¬A) ⇒(A ⇒B)$ is equivalent to the following type:

$$ ((B \to \bot) \to (A \to \bot)) \to (A \to B) $$

The following is a λC derivation.

Chapter 7 - Exercise 2

Exercise 7.2

(a) Formulate the double negation law (DN) as an axiom in λC.

(b) Verify that the following expression is a tautology in classical logic, by giving a corresponding flag-style derivation in λC (use DN):

$$(¬A ⇒A) ⇒A$$

(a) The double negation law is, for some proposition $A$,

$$\neg \neg A \implies A$$

Using the fact that $\neg A$ is encoded as $A \implies \bot$, the double negation law can be encoded as the following type being inhabited

$$((A \to \bot) \to \bot) \implies A$$

We can further abstract away the $A$, as follows

$$\Pi \alpha : *. ((\alpha \to \bot) \to \bot) \to \alpha$$

(b) The following is a flag-format derivation showing that $(¬A ⇒A) ⇒A$ is a tautology. It uses $i_{DN}$ instantiated with $A:*$.

Chapter 7 - Exercise 1

Exercise 7.1

Verify that each of the following expressions is a tautology in constructive logic, (1) by giving a proof in natural deduction, and (2) by giving a corresponding derivation in λC.

You may employ the flag style for the derivations, as in the examples given in the present chapter.

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

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

(c) $(A ⇒¬B) ⇒((A ⇒B) ⇒¬A)$

(d) $¬(A ⇒B) ⇒¬B$ (hint: use part (a)).

This summary of natural deduction was helpful in this exercise (pdf).

(a) The following is a natural deduction proof in tree format.

The following is a derivation in λC in flag notation. It shows the type $B \to (A \to B)$ is inhabited by $\lambda b:B. \lambda a:A.b$ in the context $A,B:*$.

(b) The following is a natural deduction proof in tree format. We replace $\neg A$ with the equivalent $A \to \bot$.

The following is a derivation in λC in flag notation. It shows the type $(A \to \bot) \to (A \to B)$ is inhabited by $\lambda f: A \to \bot.\lambda a:A. faB$ in the context $A,B:*$.

(c) The following is a natural deduction proof in tree format. We replace $\neg A$ with the equivalent $A \to \bot$.

The following is a derivation in λC in flag notation. It shows the type $ (A \implies (B \implies \bot)) \implies ((A \implies B) \implies (A \implies \bot)))$ is inhabited by $\lambda f:A \to (B \to \bot) .\lambda g:A \to B. \lambda a:A . fa(ga)$ in the context $A,B:*$.

(d) The following is a natural deduction proof in tree format. We replace $\neg A$ with the equivalent $A \to \bot$.

The following is a derivation in λC in flag notation. It shows the type $((A \implies B) \implies \bot) \implies ( B \implies \bot)$ is inhabited by $\lambda f:(A \to B) \to \bot.\lambda b:B.f(\lambda a:A.b) $ in the context $A,B:*$.

Chapter 6 - Exercise 11

Exercise 6.11

Let $Γ ⊢M : N$ in λC and $Γ ≡ x_1 : A_1,...,x_n : A_n$.

(a) Prove that the $x_1, ..., x_n$ are distinct.

(b) Prove the Free Variables Lemma (Lemma 6.3.3) for λC.

(c) Prove that $FV(A_i) ⊆\{x_1,...,x_{i−1}\}$, for $1 ≤i ≤n$.

(a) Definition 2.4.2 (3) states that "a context is a list of declarations with different subjects". So by definition, all the subjects $x_1, \ldots, x_n$ are distinct.

An alternative argument is to consider which derivation rules for λC allow for the building of a context. These are the (var) and (weak) rules. In both cases, a subject $x$ can only be added to an existing context if it doesn't already exist in that context. In this way, a derived context can only have distinct subjects. 

---

(b) The Free Variables Lemma 6.3.3 for λC is

If $Γ ⊢A : B$, then $FV(A), FV(B) ⊆ dom(Γ)$.

The Free Variables Lemma for λC covers not just the term $A$ but also the type B, unlike λ→ for example.

To prove the lemma we use structural induction on the derivation rules for λC, reproduced here for ease of reference.

(sort) rule

There are no free variables in the expression $A \equiv *$, nor in $B \equiv \Box$. Thus the proposition is trivially true for $∅⊢*:☐$. That is, both $FV(A)$ and $FV(B)$ are empty sets, and so are subsets of any set, including $∅ \equiv dom(Γ)$.

(var) rule

Here the conclusion of the rule is $Γ,x:A ⊢ x:A$. 

The induction hypothesis is that the lemma holds for the premise $Γ⊢A:s$. That is, $FV(A), FV(s) ⊆ dom(Γ)$. 

Because the context $Γ,x:A$ is an extension of $Γ$ with $x:A$, this means $FV(x) ⊆ dom(Γ, x:A)$. We already have $FV(A) ⊆ dom(Γ)$, and since $dom(Γ) ⊆ dom(Γ,x:A)$, we have $FV(A) ⊆ dom(Γ, x:A)$.

Together, this means $FV(x), FV(A) ⊆ dom(Γ, x:A)$. 

So the lemma holds for judgements resulting from the (var) rule.

(weak) rule

Here the conclusion of the rule is $Γ,x:C⊢A:B$.

The induction hypothesis is that the lemma holds for both premises $Γ⊢A:B$ and $Γ⊢C:s$. That is, $FV(A), FV(B) ⊆ dom(Γ)$ and $FV(C), FV(s) ⊆ dom(Γ)$. 

Since the context $Γ,x:C$ is an extension of $Γ$ with $x:C$, we immediately have $FV(A), FV(B) ⊆ dom(Γ,x:A)$.

So the lemma holds for judgements resulting from the (weak) rule.

(form) rule

Here the conclusion of the rule is $Γ⊢\Pi x:A.B \; : \;s_2$.

The induction hypothesis is that the lemma holds for both premises $Γ⊢A:s_1$ and $Γ,x:A⊢B:s_2$. That is, $FV(A), FV(s_1) ⊆ dom(Γ)$ and $FV(B), FV(s_2) ⊆ dom(Γ,x:A)$.

We need to show that $FV(\Pi x:A.B), FV(s_2) ⊆ dom(Γ)$. 

The free variables in $\Pi x:A,B$ are the free variables in $A$ and $B$ all except $x$, that is, $FV(A) \cup FV(B) \setminus {x}$. Since we know $FV(A)⊆dom(Γ)$ and $FV(B)⊆dom(Γ,x:A)$, we have  $FV(\Pi x:A.B)⊆dom(Γ)$, since

$$\begin{align} FV(\Pi x:A.B) &= FV(A) \cup FV(B) \setminus \{x\} \\ \\ &⊆ dom(Γ) \cup dom(Γ,x:A) \setminus \{x\} \\ \\ & = dom(Γ, x:A) \setminus \{x\} \\ \\ & = dom(Γ) \end{align}$$

Now we consider $FV(s_2)$. By definition $s_2$ can only be $*$ or $\Box$, and so has no free variables. So vacuously $FV(s_2) ⊆ dom(Γ)$.

We've shown that $FV(\Pi x:A.B), FV(s_2) ⊆ dom(Γ)$, and so the lemma holds for judgements resulting from the (form) rule.

(appl) rule

Here the conclusion of the rule is $Γ⊢MN:B[x:=N]$.

The induction hypothesis is that the lemma holds for both premises $Γ⊢M:\Pi x:A.B$ and $Γ⊢N:A$. That is, $FV(M), FV(\Pi x:A.B) ⊆dom(Γ)$ and $FV(N), FV(A) ⊆ dom(Γ)$.

We need to show that $FV(MN), FV(B[x:=N]) ⊆ dom(Γ)$.

Since $FV(MN)= FV(M) \cup FV(N)$, we have $FV(MN) ⊆ dom(Γ)$.

Let's now consider $FV(B[x:=N])$. This is the set of free variables in $B$ except $x$ which has been substituted for $N$. So $FV(B[x:=N]) = FV(B) \setminus \{x\}$. We have $FV(\Pi x:A.B) ⊆dom(Γ) = FV(A) \cup FV(B) \setminus \{x\} ⊆dom(Γ)$.

Now, $FV(B) \setminus \{x\} ⊆ FV(A) \cup FV(B) \setminus \{x\}$, and so we conclude $FV(B) \setminus \{x\} ⊆ dom(Γ)$. That is, $FV(B[x:=N]) ⊆ dom(Γ)$.

So the lemma holds for judgements resulting from the (appl) rule.

(abst) rule

The conclusion of the rule is $Γ⊢λx:A.M : \Pi x:A.B$.

The induction hypotheses is that the lemma holds for both premises $Γ, x:A⊢M:B$ and $Γ⊢\Pi x:A.B:s$. That is $FV(M), FV(B) ⊆ dom(Γ,x:A)$ and $FV(A) \cup FV(B) \setminus \{x\}, FV(s) ⊆ dom(Γ)$.

We need to show that $FV(\lambda x:A.M), FV(\Pi x:A.B) ⊆ dom(Γ)$.

Let's start with $FV(\lambda x:A.M) = FV(A) \cup FV(M) \setminus \{x\}$. We know $FV(M)⊆dom(Γ, x:A)$ so $FV(M) \setminus \{x\} ⊆dom(Γ)$. We also know  $FV(A) \cup FV(B) \setminus \{x\} ⊆ dom(Γ)$, which gives us  $FV(A) \setminus \{x\} ⊆ dom(Γ)$. Together this gives us $FV(A) \cup FV(M) \setminus \{x\} ⊆ dom(Γ)$. That is, $FV(\lambda x:A.M) ⊆ dom(Γ)$.

Now let's consider $FV(\Pi x:A.B)$. We already know $FV(\Pi x:A.B) ⊆dom(Γ)$. 

Together we have $FV(\lambda x:A.M), FV(\Pi x:A.B) ⊆ dom(Γ)$.

So the lemma holds for judgments resulting from the (abst) rule.

(conv) rule

The conclusion of the rule is $Γ⊢A:B'$. 

The induction hypotheses is that the lemma holds for both premises $Γ⊢A:B$ and $Γ⊢B':s$. That is $FV(A), FV(B) ⊆dom(Γ)$ and $FV(B'), FV(s) ⊆dom(Γ)$.

We need to show that $FV(A), FV(B') ⊆dom(Γ)$.

We already have $FV(A)⊆dom(Γ)$ from the induction hypothesis. We also have $FV(B')⊆dom(Γ)$ from the induction hypothesis.

Together this is $FV(A), FV(B') ⊆dom(Γ)$. 

So the lemma holds for judgements resulting from the (conv) rule.

Structural Induction

By showing that the lemma holds for the conclusion of each construction rule, assuming it holds for the premises, we have shown the lemma holds for all derivable judgements.

---

(c) We use structural induction on the derivation of the judgement $Γ ⊢M : N$ from premises using the rules for λC. Let's consider each rule in turn.

For each rule we assume the premises have well-scoped contexts, that is each free variable in each $A_i$ is defined earlier in the context. This assumption is the induction hypothesis. We aim to show the rule conclusion also has a well-scoped context.

(sort) rule

There is no premise. The context is empty, so it is vacuously true that it is well-scoped.

(var) rule

The premise is $Γ⊢A:s$, and for the induction hypothesis we assume the context is well scoped. 

We need to show the context of the conclusion $Γ,x:A⊢x:A$ is also well-scoped.

Applying the Free Variables Lemma to the premise $Γ⊢A:s$ tells us that all the free variables in $A$ are in $Γ$. This means $Γ,x:A⊢x:A$ is well-scoped.

(weak) rule

The same logic applies to the (weak) rule as for the (var) rule. 

(form), (appl), (abst), (conv) rules

All of these rules have same context in the premise as in the conclusion. The induction hypotheses that. the premise contexts are well-scoped immediately tells us the conclusion contexts are well-scoped too.

We have shown that all judgements derivable by the λC rules have well-scoped contexts. 

So by structural induction we have finally shown that $FV(A_i) ⊆ \{x_1,...,x_{i−1}\}$, for $1 ≤i ≤n$.

Chapter 6 - Exercise 10

Exercise 6.10

Given $S : *$ and $P_1,P_2 : S →*$, we define in λC the expression:

$$R ≡ λx : S. ΠQ : S →*. (Πy : S. (P_1 y →P_2 y →Qy)) →Qx$$

We claim that $R$ codes ‘the intersection of $P_1$ and $P_2$’, i.e. the predicate that holds if and only if both $P_1$ and $P_2$ hold. In order to show this, give inhabitants of the following types, plus (shortened) derivations proving this:

(a) $Πx : S. (P_1 x →P_2 x →Rx)$

(b) $Πx : S. (Rx →P_1 x)$

(c) $Πx : S. (Rx →P_2 x)$

Why do (a), (b) and (c) entail that R is this intersection?

(Hint for (b): see Exercise 5.8(a).)

(a) An inhabitant of the type is

$$ \lambda x:S.\lambda f: P_1 x. \lambda g:P_2 x. \lambda h :  \Pi y : S. (P_1 y \to P_2 y \to Qy).hxfg  $$

The following is a shortened derivation.

(b) An inhabitant of the type is 

$$ \lambda x:S . \lambda f:Rx .    ( f P_1 (\lambda y:S.(\lambda a:P_1 y . \lambda b:P_2 y.a)) ) $$

The following is a shortened derivation.

(c) An inhabitant of the type is

$$ \lambda x:S . \lambda f:Rx .    ( f P_2 (\lambda y:S.(\lambda a:P_1 y . \lambda b:P_2 y.b)) ) $$

The following is a shortened derivation.

The claim is that, for $x \in S$,

$$ P_1(x) \land P_2(x) \iff R(x) $$

"If and only if" $\iff$ has a particular meaning. $A \iff B$ means both $A \implies B$ and $B \implies A$.

In this case, it means both of the following are true:

• $ P_1(x) \land P_2(x) \implies R(x) $
• $ R(x) \implies P_1(x) \land P_2(x) $ which is equivalent to both $ R(x) \implies P_1(x) $ and $ R(x) \implies P_2(x) $.

The first is shown by (a), and the second is shown by both (b) and (c). So together, (a), (b) and (c), show that $R$ codes the intersection of $P_1$ and $P_2$.

Chapter 6 - Exercise 9

Exercise 6.9

Given $S : ∗, P : S → *$ and $f : S → S$, we define in λC the expression:

$$M ≡ λx : S. ΠQ : S →*. (Πz : S. (Qz →Q(f z))) →Qx$$

Give a term of type $Πa : S. (M a →M(f a))$ and a (shortened) derivation proving this.

The following is an inhabitant of the type $\Pi a:S . (Ma \to M(fa))$

$$\lambda b:Ma . \lambda Q:S\to *.\lambda g: (\Pi z : S. (Qz \to Q(f z))).ga(bQg)$$

The following is a shortened derivation.

Chapter 6 - Exercise 8

Exercise 6.8

(a) Let $Γ ≡ S : *, P : S → *$. Find an inhabitant of the following type $N$ in context $Γ$, and prove your answer by means of a shortened derivation:

$$N ≡ [Πα : *. ((Πx : S. (P x →α)) →α)] → [Πx : S. (P x →⊥)] →⊥$$

(b) Which is the smallest system in the λ-cube in which your derivation may be executed?

(c) The expression $Πα : ∗. ((Πx : S. (P x →α)) →α$ may be considered as an encoding of $∃_{x∈S}(P(x))$. (We shall show this in Section 7.5.) In Section 7.1 we make plausible that $A →⊥$ may be considered as an encoding of the negation $¬A$. With these things in mind, how can we interpret the content of the expression $N$? (See also Figure 5.2.)

(a) The shortened derivation below proves the inhabitant is

$$\lambda f:[\Pi \alpha : *. ((\Pi x : S. (P x \to \alpha)) \to \alpha)].\lambda g:[\Pi x : S. (P x \to \bot)]. f \bot g$$

(b) The ∏-types and their corresponding (form) types are:

• $S \to *$ corresponds to $(*, \Box)$
• $(Px \to \alpha)$ corresponds to $(*,*)$
• $\Pi x:S.(Px \to \alpha)$ corresponds to $(*,*)$
• $((\Pi x:S.(Px \to \alpha))\to \alpha)$ corresponds to $(*,*)$
• $\Pi \alpha:*.((\Pi x:S.(Px \to \alpha))\to \alpha)$ corresponds to $(\Box,*)$
• $\bot$ corresponds to $(\Box,*)$
• $(Px \to \bot)$ corresponds to $(*,*)$
• $\Pi x:S.(Px \to \bot)$ corresponds to $(*,*)$
• $[\Pi x:S.(Px \to \bot)] \to \bot$ corresponds to $(*,*)$
• $[Πα : *. ((Πx : S. (P x →α)) →α)] → [Πx : S. (P x →⊥)] →⊥$ corresponds to $(*,*)$

The minimal system is therefore λP2.

(c) The interpretation of N is 

$$\exists_{x \in S} (P(x)) \implies \neg (\forall_{x\in S}(\neg P(x) ) )$$

In words, if there exists at least one $x \in S$ for which $P(x)$ is true, that implies it is not the case that $P(x)$ is false for all $x \in S$.

Chapter 6 - Exercise 7

Exercise 6.7

Given $Γ ≡S : ∗, Q : S →S →∗$, we define in λC the expressions:

$M_1 ≡ λx,y : S. ΠR : S →S →∗. ((Πz : S. Rzz) →Rxy)$

$M_2 ≡ λx,y : S. ΠR : S →S →∗.((Πu,v : S. (Quv →Ruv)) →Rxy)$

(a) Give an inhabitant of $Πa : S. M_1 aa$ and a shortened derivation proving your answer.

(b) Give an inhabitant of $Πa,b : S. (Qab →M_2 ab)$ and a shortened derivation proving your answer.

(a) We first establish that $Πa : S. M_1 aa$ is

$$Πa : S.  ΠR : S →S →∗. ((Πz : S. Rzz) →Raa)$$

The following derivation proves the inhabitant is

$$\lambda a:S. \lambda R:S \to S \to *.\lambda f:(\Pi z:S.Rzz). fa$$

(b) We first establish that $Πa,b : S. (Qab →M_2 ab)$ is

$$Πa,b : S. (Qab → ΠR : S →S →∗.((Πu,v : S. (Quv →Ruv)) →Rab))$$

The following derivation proves the inhabitant is

$$\lambda a,b:S. \lambda q:Qab . \lambda R:S \to S \to *.\lambda f:(\Pi u,v : S. (Quv \to Ruv)) . fabq$$

Chapter 6 - Exercise 6

Exercise 6.6

Let $$M ≡λS : *. λP : S →*. λx : S. (P x →⊥)$$

(a) Which is the smallest system in the λ-cube in which $M$ may occur?

(b) Prove that $M$ is legal and determine its type.

(c) How could you interpret the constructor $M$, if $A →⊥$ encodes $¬A$?

(a) The arrow types and their corresponding (form) types in the judgment $M$ are as follows:

• $S \to *$ corresponds to $(*,\Box)$
• $\bot$ corresponds to $(\Box, *)$
• $Px \to \bot$ corresponds to $(*, *)$
• $(S \to *) \to (S \to *)$ corresponds to $(\Box,\Box)$ - see derivation of types below.
• $* \to (S \to *) \to (S \to *)$ corresponds to $(\Box,\Box)$ - see derivation of types below.

Therefore the smallest system in the λ-cube in which $M$ can occur is the full λC.

(b) The following is a shorted derivation of the judgement.

Because $M$ has been derived following the derivation rules, has a type and a context (here, empty), then $M$ is legal. 

As a reminder, Definition 6.3.7 updates the definition of legality as being typable or inhabited.

In the empty context, $M$ has the following type $$\Pi S:*. ( (S \to *)  \to (S \to *) )$$

Note 1, alternative notation for this is $(S:*) \to ( (S \to *)  \to (S \to *)$.

Note 2, the official solutions appear to have a typo, suggesting the type is $S \to ( (S \to *)  \to (S \to *)$.

(c) $M$ can be interpreted as constructing the negation of a proposition $P$ supplied as an argument, where that proposition is about all elements of a set $S$.

Chapter 6 - Exercise 5

Exercise 6.5

Let $J$ be the following judgement:

$$ S : * \quad  \vdash  \quad \lambda Q : S \to S \to *. \lambda x : S. Qxx \quad  : \quad  (S \to S \to *) \to S \to * $$

(a) Give a shortened derivation of $J$ and determine the smallest subsystem to which $J$ belongs.

(b) We may consider the variable $Q$ in $J$ as expressing a relation on set $S$. How could you describe the subexpression $λx : S. Qxx$ in this setting? And what is then the interpretation of the judgement $J$?

(a) The following is a shortened derivation.

The following are the arrow sub-expressions, and the corresponding (form) types:

• $S \to *$ corresponds to $(*,\Box)$
• $S \to S \to *$ corresponds to $(*,\Box)$
• $(S \to S \to *) \to S \to *$ corresponds to $(\Box,\Box)$

This means the smallest subsystem the judgement $J$ can belong to is λPω.

(b) The subexpression $\lambda x:S.Qxx$ can be interpreted as a relation taking one argument constructed from a relation $Q$ taking two arguments, achieved by providing $Q$ with the same argument twice.

The interpretation of the judgement is therefore "the existence of a proposition about two elements of a set implies the existence of a proposition about one element of that set, and the proof is the construction of a relation taking one parameter from a relation taking two parameters by providing it with the same parameter twice ".

Chapter 6 - Exercise 4

Exercise 6.4

Let $Γ ≡S : *, Q : S →S →*$ and let $M$ be the following expression:

$$M ≡ (Πx,y : S. (Qxy → Qyx → ⊥)) → Πz : S. (Qzz → ⊥)$$

(a) Give a shortened derivation of $Γ ⊢M : *$ and determine the smallest subsystem to which this judgement belongs.

(b) Prove in λC that $M$ is inhabited in context $Γ$. You may use a shortened derivation.

(c) We may consider $Q$ to be a relation on set $S$. Moreover, it is reasonable to see $A →⊥$ as the negation $¬A$ of proposition $A$. (We shall explain this in Section 7.1.) How can $M$ then be interpreted, if we also take Figure 5.2 into account? And what is a plausible interpretation of the inhabiting term you found in (b)?

(a) The following is a shortened derivation of $Γ ⊢M : *$.

The following are the arrow sub-terms and their corresponding (form) types:

• Context $S \to *$ corresponding to $(*,\Box)$.
• Context $S \to S \to *$ corresponding to $(*, \Box)$.
• Subterm $Qyx \to \bot$ corresponding to $(*,*)$.
• Subterm $\bot$ corresponding to $(\Box, *)$.
• Subterm $Qxy \to Qyx \to \bot$ corresponding to $(*,*)$.
• Subterm $\Pi x,y:S.(Qxy \to Qyx \to \bot)$ corresponding to $(*,*)$
• Subterm $Qzz \to \bot$ corresponding to $(*,*)$.
• Subterm $Qxy \to Qyx \to \bot$ corresponding to $(*,*)$.
• Subterm $\Pi z:S.(Qzz \to \bot)$ corresponding to $(*,*)$
• Term $(\Pi x,y:S.(Qxy \to Qyx \to \bot)) \to \Pi z:S.(Qzz \to \bot)$ corresponds to $(*,*)$.

This means the smallest subsystem the judgement can belong to is λP2.

(b) By inspection the inhabitant should be

$$\lambda f:(\Pi x,y:S.(Qxy \to Qyx \to \bot)) . (\lambda z:S.(\lambda q:Qzz.fzzq))$$

The following is a derivation of this inhabitant, continuing from the derivation of the type above.

(c) The interpretation of $M$ is as follows.

$$\forall_{x,y \in S}(\;  Q(x,y) \implies \neg Q(y,x)\; ) \implies \forall_{z \in S}(\; \neg Q(z,z) \; )$$

In words, if $Q$ is asymmetric, then $Q$ is not reflexive.

The interpretation of the inhabitant is "there exists a function (here, $f$) that maps an asymmetric function to an irreflexive function", which proves the above logical statement.