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. 

Chapter 7 - Exercise 10

Exercise 7.10

As Exercise 7.9:

$$\begin{gather} ∀_{x∈S}(P(x) ⇒Q(x)) \\ \\ ⇒ \\  \\ ∀_{y∈S}(P(y) ⇒R(y)) \\ \\ ⇒ \\ \\ ∀_{z∈S}(P(z) ⇒(Q(z)∧R(z))) \end{gather}$$

The following is a first order natural deduction.

The corresponding type is

$$ (\Pi x:S.(Px \to Qx)) \to (\Pi y:S.(Py \to Ry)) \to (\Pi z:S.(Pz \to (\Pi C:*.((Qz \to Rz \to C) \to C)))) $$

with a context of $S:*, \; P, Q,R, : S \to*$.The following is a flag-style derivation in λC.

Chapter 7 - Exercise 9

Exercise 7.9

Verify that each of the following expressions is a tautology in constructive logic, (1) by giving a proof in first order natural deduction, and (2) by giving a flag-style derivation in λC:

(a) $∀x∈S(¬P(x) ⇒(P(x) ⇒(Q(x)∧R(x))))$

(b) $∀x∈S(P(x)) ⇒∀y∈S(P(y)∨Q(y))$

(a) The following is a first order natural deduction.

The corresponding type is

$$ \Pi x:S . ((Px \to \bot) \to (Px \to ( \Pi C:*.(Qx \to Rx \to C) \to C ) ) ) $$

with a context of $S:*, \; P, Q, R : S \to*$.

The following is a flag-style derivation in λC.

(b) The following is a first order natural deduction.

The corresponding type is

$$(  \Pi x:S.Px ) \to ( \Pi y:S. ( \Pi C:*.( (Py \to C) \to (Qy \to C) \to C) ) ) $$

with a context of $S:*, \; P, Q, : S \to*$.The following is a flag-style derivation in λC.

Chapter 7 - Exercise 8

Exercise 7.8

Give λC-derivations verifying the following tautologies of constructive logic (hint: use Exercise 7.7 and Section 7.2):

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

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

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

Constructive logic means we don't have the double negation rule or the law of the excluded middle.

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

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

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

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

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

The following is a λC derivation of an inhabitant of this type. The derivation uses $P$ and $Q$ as abbreviations for longer expressions.

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

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

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