# Course review

Maintainer: admin

The exam will take place on April 24, at 9am, in the gym (room 408).

## 1Sources¶

The content on this page has been extracted (not using inference rules) from both Brigitte Pientka's notes (available through WebCT) and Frank Pfenning's notes. Any errors or omissions should be assumed to be the fault of @dellsystem and not of either original author.

## 2Natural deduction¶

Inference rule: premises on top, conclusion on the bottom.

An inference rule with no premises is an axiom.

Hypothetical judgments: when we start from unproven assumptions. Though, if we have a proof for an assumption, we can replace the assumption with the derivation tree for it, eliminating the assumption in the process (substitution principle).

Hypothetical derivation: proof tree for a hypothetical judgment. Strategy: apply intro rules starting from the conclusion and working towards the assumptions; then, apply elimination rules starting from the assumptions.

### 2.1Introduction and elimination rules¶

#### 2.1.1Conjunction¶

Introduction rule:

$$\frac{A \,\text{true} \quad B \,\text{true}}{A \land B \,\text{true}} \, \land I$$

Elimination rule:

$$\frac{A \land B \,\text{true}}{A \,\text{true}} \, \land E_l \qquad \frac{A \land B \,\text{true}}{B \,\text{true}} \, \land E_r$$

#### 2.1.2Truth¶

Introduction rule:

$$\frac{}{\top \,\text{true}} \, \top I$$

Elimination rule:

No elimination rule since $\top$ holds unconditionally (and thus there is no information that we can extract from it).

#### 2.1.3Implication¶

Introduction rule:

$$\frac{}{A\,\text{true}} \, u \quad \quad \\ \vdots \quad \quad \\ \frac{B\,\text{true}}{A \subset B \,\text{true}} \,\subset I^u$$

Elimination rule:

$$\frac{A \subset B \,\text{true} \quad A\,\text{true}}{B\,\text{true}}\, \subset E$$

Note that implications are right-associative. So with $A \subset B \subset C$, start from the end and make that a thing first ($B \subset C$), etc.

Also note that the $u$ in the $I^u$ means that $u$ is no longer available for use as a general assumption, as it was consumed by the introduction rule. In other words, it indicates the end of the scope in which $u$ is valid.

Any assumptions that are discharged more than once should be given different labels.

It's fine if an assumption is not discharged by the end of the proof.

(I'm confused about an example in Pientka's notes in which she shows 3 proofs for $A \subset A \subset (A \land A)$, side by side, but the last two have equivalent assumptions with the same label, even though she mentions earlier that it is critical that all labels denoting assumptions are distinct. Also, where does $v$ come from in the middle one, and where does $u$ come from in the last one? They're not part of the scope ...)

#### 2.1.4Disjunction¶

Introduction rule:

$$\frac{A\,\text{true}}{A \lor B \,\text{true}} \, \lor I_l \qquad \frac{B\,\text{true}}{A \lor B\,\text{true}} \, \lor I_r$$

$$\frac{}{A\,\text{true}} \,u \quad \; \frac{}{B\,\text{true}}\,v \\ \vdots \qquad \qquad\; \vdots \; \\ \frac{A \lor B\,\text{true} \qquad C\,\text{true} \qquad C\,\text{true}}{C \,\text{true}} \, \lor E^{u, v} \qquad \qquad \tag{don't read the source, it's really bad}$$

#### 2.1.5Falsehood¶

Introduction rule:

None, since if there were an introduction rule for deriving $\bot$, then our inference system would immediately be unsound.

Elimination rule:

$$\frac{\bot \,\text{true}}{C \,\text{true}} \, \bot E$$

i.e., we've arrived at a contradiction and so we can conclude anything

#### 2.1.6Example proofs¶

$$\top \land (\top \land \top)$$

Working from the bottom: We can use $\land I$ to get the conclusion, from the hypotheses $\top$ and $(\top \land \top)$. For the former, we can get that immediately using $\top I$; for the latter, we have to do another $\land I$, for which we need $\top$ true twice. But we can get those using, once again, $\top I$. $\blacksquare$

Source: Pientka's notes.

$$A \subset B \subset (A \land B)$$

First, note that since $\subset$ is right-associative, this is equivalent to $A \subset (B \subset (A \land B))$. So first we need to introduce the left-most $\subset$. Let $u$ be $A$ true, and suppose that we have a proof of $B \subset (A \land B)$ given $u$. Well, to get $B \subset (A \land B)$, we need another $\subset$ intro: let $v$ be $B$ true, and suppose that we have a proof of $(A \land B)$ given $v$. But we can get $A \land B$ by using $\land I$ on $u$ and $v$. So that completes the proof.

Source: Pientka's notes.

$$A \subset A \subset (A \land A)$$

Starting from the bottom: first, get $A \subset (A \land A)$ (assuming we have a proof of $u=A$) using $\subset I^u$. Then, get $A \land A$ (assuming we have a proof of $v = A$) using $\subset I^v$. Then, we just use $\land I$ on $u$ and $v$ and that completes the proof.

Source: Pientka's notes.

$$(A \land B) \subset (B \land A)$$

Starting from the bottom: first, get $(B \land A)$ (assuming we have a proof of $u = A \land B$) using $\subset I^u$. To get $B \land A$, we use $\land I$, assuming we have $B$ and $A$ somewhere. But we can get $B$ using $\land E_r$ on $u$, and we can get $A$ using $\land E_l$ on $u$. So we're good.

Source: Pientka's notes.

$$(A \subset (B \land C)) \subset ((A \subset B) \land (A \subset C))$$

i.e., distributivity.

Starting from the bottom: get $(A \subset B) \land (A \subset C)$ (assuming we have $u=A \subset (B \land C)$) using $I^u$. To get $(A \subset B) \land (A \subset C)$, we use $\land I$ on $A \subset B$ and $A \subset C$.

Here we branch into the two cases. To get $A \subset B$, we use $I^v$ where $v= A$. But then we need to get $B$ from somewhere. Well, if we use $\subset E$ on $u$ and $v$, we can get $B \land C$, and then use $\land E_l$ to get $B$. Similarly, for $A \subset C$, we re-use $v= A$ and use $\land E_r$ to get $C$ from $B \land C$. That completes it. $\blacksquare$

Source: Pientka's notes.

$$(A \lor B) \subset (B \lor A)$$

i.e., commutativity of $\lor$.

Starting from the bottom, we get $B \lor A$ (assuming we have $u = A \lor B$) using $I^u$. To get $B \lor A$, we use an elimination rule: let $v = A$, then use $\lor I_l$ to get $B \lor A$, and let $w = B$, then use $\lor I_r$ to get $B \lor A$. Then we can use $\lor E^{v, w}$ to conclude $B \lor A$ (with $u$ being the term on the left).

Source: Pientka's notes.

$$(A \land (B \land C)) \subset (A \land B)$$

This is ridiculously straightforward. Let $u = A \land (B \land C)$, and elim twice to get $A$ (with $\land E_l$) and also $B \land C$ (with $\land E_r$). Then use $\land E_l$ on $B \land C$ to get $B$. Then use $\land I$ on $A$ and $B$ to get $A \land B$. Then just use $\subset I$.

Source: assignment 1, exercise 1.

$$(A \subset B) \subset ((B \subset C) \subset (A \subset C))$$

Starting from the bottom. We need $(B \subset C) \subset (A \subset C)$ (with $u = A \subset B$) using $\subset I^u$. Then, we need $A \subset C$ (with $v = B \subset C$) using $\subset I^v$. Finally, we need $C$ (with $w=A$) using $\subset I^w$. If we use $\subset E$ on $w$ and $u$, we get $B$; if we use $\subset E$ on $B$ and $v$, we get $C$. So we're done.

Source: assignment 1, exercise 1.

$$((A \lor B) \subset C) \subset (A \subset C) \land (B \subset C)$$

Starting from the bottom, we use $I^u$ to get $(A \subset C) \land (B \subset C)$ where $u = ((A \lor B)\subset C)$. Then, obviously need $\land I$; now we just need to get $A \subset C$ and $B \subset C$. For the former, we let $v = A$ and use $I^v$ to get C somehow. How do we get $C$? Well, if we use $\lor I_l$ on $v$, we get $A \lor B$; then, if we use $\subset E$ on $A \lor B$ and $u$, we get $C$. Similarly, to get $C$ on the other side, we use $\lor I_r$ on $w=B$, and conclude that $B \subset C$ using $I^w$. $\blacksquare$.

Source: assignment 1, exercise 1.

$$(A \subset C) \land (B \subset C) \subset ((A \lor B) \subset C)$$

Let $u = (A \subset C) \land (B \subset C)$. We can use $\subset I^u$ on $(A \lor B) \subset C$. To get that, let $v = A \lor B$, and use $\subset I^v$ on $C$. To get $C$, we need to make use of the elimination rule for $\lor$. So let $w_1 = A$, and $w_2 = B$. Next, apply $\land E_l$ to get $A \subset C$ and $\land E_r$ to get $B \subset C$. Then, applying $\subset E$ on $A$ and $A \subset C$ gives us $C$, for the middle branch; similarly, applying $\subset E$ on $B$ and $B \subset C$ gives us $C$. Then we just use $\lor E^{w_1, w_2}$ to close the gap. $\blacksquare$

Source: assignment 1, exercise 1.

$$((A \subset B) \land (A \lor C)) \subset (B \lor C)$$

Let $u = (A \subset B) \land (A \lor C)$. We can use $\subset I^u$ on $B \lor C$. To get that, we let $v = A$ and $w = C$, then use $\lor E^{v, w}$ on $A \lor C$ (the first term) and $B \lor C$ (the middle and last terms). To get $B \lor C$ from $v$ and $w$, we use $\land E_l$ on $u$ to get $A \subset B$. Then, we use $\subset E$ on $A$ and $A \subset B$ to get $B$, after which we just apply $\lor I_l$ to get $B \lor C$. The other branch is even simpler: from $C$, just use $\lor I_r$ to get $B \lor C$. Then, to get $A \lor C$ (the first term), we just use $\land E_r$ on $u$. $\blacksquare$.

Source: assignment 1, exercise 1.

### 2.2Local soundness and completeness¶

For each intro/elim rule, we should check that it's both sound (i.e., does not allow new truths to be deduced) and complete (i.e., strong enough to obtain all the information contained in the connective).

Local soundness: introducing then eliminating a connective should not introduce any new information, so if we do this in a proof, we should be able to get rid of the intro + elim and find a shorter path to the conclusion. We can prove this using a local reduction.

Local completeness: if we eliminate a connective, we get enough information out of it to be able to introduce it again. We can prove this using a local expansion.

#### 2.2.1Conjunction¶

Local soundness

Start with $A$ true and $B$ true. The only things we should be able to extract from $A \land B$ true are $A$ true and $B$ true. So let $\mathcal D_1$ be $A$ true and $\mathcal D_2$ be $B$ true; get $A \land B$ true using $\land I$; then get $A$ true using $\land E_l$. From this we extract $\mathcal D_1$. Similarly, using $\land E_r$, we extract $\mathcal D_2$.

Pientka's notation for this is a pain to type out so I'm just going to take a screenshot of the $A$ true case in her notes:

Local completeness

Let $\mathcal D$ be $A \land B$. Starting from this, we need to use the elimination rules and then the introduction rule to rebuild $A \land B$. This is pretty straightforward: use $\land E_l$ for $\mathcal D$ on the left to get $A$ true, and $\land E_r$ for $\mathcal D$ on the right to get $B$ true, and use $\land I$ to get $A \land B$ true.

Screenshot of the proof in her notes:

Source: Pientka's notes.

#### 2.2.2Implication¶

Local soundness

To introduce $A \subset B$, we need to have a proof of $A$ true first (which we'll call $u$). Let $\mathcal D$ be $B$ true. Then, given $u$ and $\mathcal D$, we can use $\subset I^u$ to conclude $A \subset B$ true. Then, using $A \subset B$ true and $A$ true (which we'll call $\mathcal E$), we can use $\subset E$ to get $B$ true. Thus, if we start with $A$ true as assumption (from which we can get a proof of $\mathcal D$), then use $\subset I^u$ and $\subset E$, all we can conclude is that if we have $\mathcal E$ as an assumption, we can get a proof of $\mathcal D$, which is what we wanted.

Note that we can instead write $[\mathcal E/u]\mathcal D$ on the right side, to indicate that we substitute $\mathcal E$ in place of the assumption $u$.

Local completeness

Given $\mathcal D = A\subset B$ true and $u = A$ true, we use $\subset E$ to conclude $B$ true, and then use $\subset I^u$ to conclude $A \subset B$ true, as desired.

Source: Pientka's notes.

#### 2.2.3Disjunction¶

Local soundness

There are two cases: one for reconstituting that if we have $A$ true, we can get $C$ true; and another for reconstituting that if we have $B$ true, we can get $C$ true.

For the former, let $\mathcal D = A$ true. Use $\lor I_l$ to get $A \lor B$ true. Then, using the assumptions $u = A$ true (from which we can get a proof of $\mathcal E = C$ true) and $v = B$ true (from which we can get a proof of $\mathcal F = C$ true), we use the rule $\lor E^{u, v}$ to conclude that $C$ true. So if $\mathcal D$ holds, then we get $\mathcal E$, as desired.

For the latter, we let $\mathcal D = B$ true, and use $\lor I_r$ to get $A \lor B$ true; the rest is the same. Thus if $\mathcal D$ holds, then we get $\mathcal F$, as desired.

There's a typo in the proof of this in Pientka's notes; $B$ true is labelled $u$ whe it should be labelled $v$.

Local completeness

This one is a bit weird - although you still follow the general principle of elim-then-intro, the actual proof looks very similar to the reduction (i.e., intro-then-elim), which is very confusing. In Pientka's notes, she just puts in the proof without any explanation, but Frank Pfenning's notes on harmony have a pretty good explanation.

The basic idea: start with $\mathcal D = A \lor B$. Let $u = A$ true and $v = B$ true be the assumptions. From $u$, use $\lor I_l$ to get $A \lor B$ true; from $v$, use $\lor I_r$ to get $A\lor B$ true. Then, you have 3 instances of $A \lor B$ true, and you can use $E^{u, v}$ to conclude $A \lor B$ true.

If you think about it, there isn't really any other way to do it, since the elim rule for $\lor$ only allows you to conclude $C$ provided that $A$ and $B$ both allow you to conclude $C$. So $C$ must be $A \lor B$. Plus, $A \lor B$ must be on the left. And to get the other $A \lor B$s, we need to use intro rules. $\blacksquare \checkmark \bigstar \heartsuit \wr \text{pls let me pass}$

Source: Pientka's notes.

#### 2.2.4Alternative conjunction¶

Suppose we had the following elimination rule for conjunction instead of the standard one:

$$\frac{}{A\,\text{true}} \,u \quad \; \frac{}{B\,\text{true}}\,v \\ \vdots \; \\ \frac{A \lor B\,\text{true} \qquad C\,\text{true}}{C \,\text{true}} \, \lor E^{u, v} \qquad \qquad$$

The introduction rule remains the same:

$$\frac{A \,\text{true} \quad B \,\text{true}}{A \land B \,\text{true}} \, \land I$$

These rules are locally sound and complete. Proofs:

Local soundness

There are two: one starting with $A$, and one starting with $B$. For the one starting with $A$, let $D_1$ be $A$ true, and let $D_2$ be $B$ true. Apply $\land I$ to get $A \land B$ true. Now let $u = A$ and $v = B$ and apply $\land E^{u, v}$ on $A \land B$ and $A$ (which we've derived from $u$, ignoring $v$) to get $D_1 = A$.

To get $D_2=B$, just ignore $u$ instead of $v$.

Local completeness

Just as with disjunction, this one looks a bit weird at first. Basically, we need $A \land B$ to be our conclusion (so the last line, or bottom, of the proof tree). We can get this using $\land E^{u, v}$ where $u = A$ and $v = B$ - just use $\land I$ on $u$ and $v$ to get $A \land B$ on the right.

Actually, it looks like there's an alternative approach: with $A \land B$ on the bottom, we use $\land I$ to get it from $A$ and $B$. To get $A$, we use $\land E^{u, v}$ on $A \land B$ with $u = A$ and $v = B$. Similarly, to get $B$, we have another proof subtree where we do the same thing. This should work? But it's not in the official solutions for the question. So I guess it doesn't, though I'm not sure why.

Source: assignment 1, exercise 3.

#### 2.2.5Nand¶

Let's define our own introduction/elimination rules for $A \bar \land B$.

Introduction rule

$$\frac{}{A} \,u \quad \; \frac{}{B}\,v \quad\qquad\qquad\quad\; \\ \vdots \qquad\qquad\qquad \;\, \\ \frac{p}{A \bar \land B} \, \lor I^{u, v, p} \qquad \qquad \tag{where p is any arbitrary proposition.}$$

Elimination rule

$$\frac{A \bar \land B \qquad A \qquad B}{C} \, \bar \land E$$

These rules are locally sound and complete. Proofs:

Local soundness

As usual, there are two proofs. For the first, we start with $u = A$ and $v=B$. Suppose we have a proof tree $\mathcal D$ whereby we can derive $p$ starting from $u$ and $v$. Then we can use $\bar \land I^{u, v, p}$ to conclude that $A \bar \land B$. Then, if $\mathcal E_1 = A$ and $\mathcal E_2 = B$, we use $\bar \land E$ to conclude $A$.

For the other proof, we just conclude $B$ instead of $A$ in the final step (the rest is the same).

Local completeness

Let $u = A$ and $v = B$. Start with $A \bar \land B$. Combining this with $A$ and $B$, we use $\bar \land E$ to conclude $p$. Then we immediately use $\bar \land I^{u, v, p}$ to reconstitute $A \bar \land B$. Easy.

Source: assignment 1, exercise 4 (optional).

### 2.3Classical logic¶

Pientka doesn't really mention this in her notes, but exercise 2 of assignment 1 briefly covers this. Classical logic is basically constructive logic (what we had above) with an additional axiom: the law of the excluded middle (so $p \lor \neg p$ holds for all $p$).

## 3Proof terms¶

$M: A$ means that $A$ is a proposition, and $M$ is a proof term for $A$ (i.e., the term that represents a proof of $A \text{true}$).

### 3.1List of proof terms¶

These notes mostly follow Pientka's, with some things confirmed by Frank Pfenning's, because Pientka's notes had some typos that made me lose my faith (and my sanity). I'm also mostly using Pfenning's notation (with the $\Gamma$s and all that) because Pientka's notation takes longer to type and in any case she ends up using that notation eventually.

#### 3.1.1Conjunction¶

Introduction rule

$$\frac{\Gamma \vdash M:A \qquad N:B}{\Gamma \vdash \langle M, N \rangle: A \land B} \, \land I$$

Elimination rules

$$\frac{\Gamma \vdash M: A \land B}{\Gamma \vdash \text{fst} \, M:A} \,\land E_l \qquad \qquad \frac{\Gamma \vdash M: A \land B}{\Gamma \vdash \text{snd}\,M:B} \, \land E_r$$

Local reduction

It's really the same as the original local soundness rule, we just annotate it. Not including it here.

From the two soundness proofs, we get two reduction rules (just using the last line of each side of the arrow):

• $\text{fst}\,\langle M, N \rangle \implies M$
• $\text{snd}\,\langle M, N \rangle \implies N$

Note that reduction is type-preserving: if $M:A$ and $M \implies M'$, then $M':A$. So if $M$, of type $A$, reduces to $M'$, then $M'$ is also of type $A$ (where $A$ is, again, a proposition). This statement is sometimes referred to as subject reduction.

Local expansion

Just annotate the local completeness rule, starting from the $A \land B$ on the right being $M$. We should get $\langle \text{fst} M, \text{snd} M \rangle$ on the right. So the local expansion rule is

$$M: A \land B \implies \langle \text{fst} M, \text{snd} M \rangle$$

#### 3.1.2Truth¶

Introduction rule

$$\frac{}{(): \top} \, \top I$$

(There's a typo in Pientka's notes - the annotated term should be on the bottom, not on the top. There's a pun in there somewhere but fuck it.)

Elimination rule

There isn't one. Since this isn't a connective, we don't have local reduction/expansion rules, either.

#### 3.1.3Implication¶

Introduction rule

$$\frac{\Gamma, u:A \vdash M :B}{\Gamma \vdash (\lambda u:A .M): A \subset B} \, \subset I^u$$

Elimination rule

$$\frac{\Gamma \vdash M: A \subset B \qquad \Gamma \vdash N:A}{\Gamma \vdash M N : B}\, \subset E$$

Local reduction

As before, we just annotate the local soundness proof to get

$$(\lambda x: A.M) N \implies [N/x]M$$

Local expansion

Once again, here we annotate the local completeness proof:

$$M : A \subset B \implies \lambda x: A.M x$$

#### 3.1.4Disjunction¶

Introduction rules

$$\frac{\Gamma \vdash M: A}{\Gamma \vdash \text{inl}^A M: A \lor B} \, \lor I^l \qquad \frac{\Gamma \vdash N:B}{\Gamma \vdash \text{inr}^B N: A\lor B} \, \lor I^r$$

Elimination rule

$$\frac{\Gamma \vdash M: A \lor B\qquad \Gamma, x:A\vdash N_l: C \qquad \Gamma, y: B \vdash N_r:C}{\Gamma \vdash \text{case}\,M\,\text{of inl}^A x \to N_l \mid \, \text{inr}^B y \to N_r}\,\lor E^{x, y}$$

Local reduction

Again, we simply annotate the two local soundness proofs:

$$\text{case}(\text{inl}^A M) \text{of inl}^A x \to N_l \mid \text{inr}^B y \to N_r \implies [M/x]N_l$$

For the other rule, we have:

$$\text{case}(\text{inr}^B M) \text{of inl}^A x \to N_l \mid \text{inr}^B y \to N_r \implies [M/y]N_r$$

Local expansion

Not mentioned in either Pientka's or Pfenning's notes ... I'll come back to this later.

#### 3.1.5Falsehood¶

Introduction rule

There isn't one.

Elimination rule

$$\frac{\Gamma \vdash M: \bot}{\Gamma \vdash \text{abort}^C C: C} \, \bot E$$

#### 3.1.6Iff¶

Introduction rule

$$\frac{\Gamma, u:B \vdash M: A \qquad \Gamma, v:A \vdash N:B}{\Gamma \vdash [ u.M, v.N ] : A \equiv B}\,\equiv I^{u, v}$$

Note that you need to keep track of the assumptions $u$ and $v$ within the proof term for the introduction rule.

Elimination rules

$$\frac{M: A \equiv B \qquad N:A}{\text{iff}_L(M, N): B} \, \equiv E_l \qquad\qquad \frac{M: A \equiv B \qquad N: B}{\text{iff}_R (M, N): A}\,\equiv E_r$$

Local reduction

$$\text{iff}_L([u.M, v.N], S) \implies [S/u]M \qquad \text{iff}_R([u.M, v.N], S) \implies [S/v]N$$

Local expansion

$$M \implies [u.\text{iff}_R(M, u), v.\text{iff}_L(M, v)]$$

Source: assignment 2, exercise 3.

### 3.2Example annotations¶

They're basically the same as regular proofs, only you need to use the annotated rules. Nothing too complicated.

$$(A \land A) \subset A$$

Given $u = A \land A$ we need to be able to get $A$. Well, using $\land E_l$, we can. So from $u = x:A \land A$ we get $\text{fst}\, x: A$. Then, for the implication, we need a lambda, so we have $\lambda x: A \land A.\text{fst}\, x:(A \land A) \subset A$.

Alternatively, we could extract the right $A$ from $A \land A$, in which case we'd just have to replace the $\text{fst}\,$ by $\text{snd}\,$.

I think there's a typo in the notes - it should be $u = x: A \land A$ not $u = x:A$.

Source: Pientka's notes.

$$(A \land B) \subset (B \land A)$$

Let $u = x:A \land B$. Use $\land E_r$ to get $\text{snd}\, x: B$. On the other branch, use $\land E_l$ to get $\text{fst}\, x: A$. Then use $\land I$ to get $\langle \text{snd}\, x, \text{fst}\, x \rangle: B \land A$. Finally, for the implication, we need a lambda, so we have $\lambda x: A \land B.\langle \text{snd}\, x, \text{fst x} \rangle: (A \land B) \subset (B \land A)$.

Source: Pientka's notes.

$$(A \land (B \land C)) \subset (A \land B)$$

For implication, the pattern is pretty easy to pick up on: the $x$ in the lambda needs to be of type $A \land (B \land C)$, and the body of the lambda needs to be of type $A \land B$ somehow. How do we derive $A \land B$? Well, if $u = x: A\land (B\land C)$, then $\text{fst}\, x$ gives us $A$, $\text{snd}\, x$ gives us $B \land C$ and so $\text{fst}\,\, \text{snd}\, x$ gives us $B$, and then using $\land I$ gives us $A \land B$. So we have

$$\lambda x: A \land B(\land C). \langle \text{fst}\, x, \text{fst}\,\,\text{snd}\, x \rangle: A \land (B \land C) \subset (A \land B)$$

Source: assignment 1, question 1.

$$(A \subset B) \subset ((B \subset C) \subset (A \subset C))$$

Our assumption is $u = x: A \subset B$. From this, we need to be able to extract something of type $(B \subset C) \subset (A \subset C)$. This itself requires the assumption $v = y:B \subset C$, from which we need to be able to extract something of type $A \subset C$. To get this, we need the assumption $w = z: A$. Then, by applying $x$ to $z$, we get $x z: B$ (using $\subset E$). Furthermore, applying $y$ to $x z$, we get $y (x z): C$. Thus to extract something of type $A \subset C$, we need $\lambda z: A. y (x z): A \subset C$.

Next, we define the scope of $y$: $\lambda y: B. \lambda z: A. y (x z): (B \subset C) \subset (A \subset C)$. Lastly, we define the scope of $x$:

$$\lambda x: A \subset B. \lambda y: B. \lambda z: A. y (x z): (A \subset B) \subset ((B \subset C) \subset (A \subset C))$$

Source: assignment 1, question 1.

$$((A \lor B) \subset C) \subset (A \subset C) \land (B \subset C)$$

Our assumption is $x:(A \lor B) \subset C$. From this, we need to extract $(A \subset C) \land (B \subset C)$. Clearly we need to extract the left and right terms individually, then use $\land I$. Well, to get $A \subset C$ is easy: if we have the assumption $y:A$, then we can use $\lor I^l$ to get $\text{inl}^A y: A \lor B$. So we have

$$\lambda y: A.\text{inl}^A y: A \subset (A \lor B)$$

And if we apply $x$ to the proof term for $A \lor B$, we get

$$\lambda y: A. x (\text{inl}^A y): A \subset C$$

Similarly, for the other branch, we have:

$$\lambda z: B. x (\text{inr}^B z): B \subset C$$

Then we just use $\land I$ and close off the scope with $\subset I$:

$$\lambda x: (A \lor B) \subset C. \langle \lambda y: A. x (\text{inl}^A y), \lambda z: B. x (\text{inr}^B z): B \subset C \rangle: ((A \lor B) \subset C) \subset (A \subset C) \land (B \subset C)$$

Source: assignment 1, question 1.

$$(A \subset C) \land (B \subset C) \subset (A \lor B) \subset C$$

Let $x = (A \subset C) \land (B \subset C)$. Need to prove $(A \lor B) \subset C$. To do this, let $y = A \lor B$, from which we need to conclude $C$. It looks like we'll need to use $\lor E$ somehow.

First, suppose that $A$ is true. How can we use this to conclude that $C$ is true? Well, if $z_1:A$, then applying $\text{fst}\, x: A \subset C$ to $z_1$ will give us $C$:

$$(\text{fst}\, x) z_1: C$$

Similarly, for the other branch, suppose that $z_2: B$ is true. Then, applying $\text{snd}\, x: B \subset C$ to $z_2$ will give us $C$:

$$(\text{snd}\, x) z_2: C$$

Now we can use $\lor E$ to conclude $C$:

$$\text{case}\,y\,\text{of inl}^A z_1 \to (\text{fst}\, x) z_1 \mid \text{inr}^B z_2 \to (\text{snd}\, x) z_2: C$$

Next, we limit the scope of $y$ using $\subset I$:

$$\lambda y: A \lor B. \text{case}\,y\,\text{of inl}^A z_1 \to (\text{fst}\, x) z_1 \mid \text{inr}^B z_2 \to (\text{snd}\, x) z_2: (A \lor B) \subset C$$