Each worksheet prints cleanly on A4 or Letter. Answer keys are on a separate page.

The Lumenary · Advanced undergraduate

Type theory and propositions as types

Name: ______________________

Date: ______________________

You will learn to

Type-check terms of the simply typed λ-calculus and read them as proofs in intuitionistic propositional logic
Explain dependent function (Π) and dependent pair (Σ) types and use them to express ∀ and ∃
Define the natural numbers and lists as inductive types and derive their induction principles from their recursors
Prove, with a Kripke model, that some classical tautologies such as Peirce's law are uninhabited types
Contrast a type-theoretic foundation such as Lean's, where every term has a type, with ZFC, where everything is a set

1.
Under the propositions-as-types correspondence, what is a proof of $A \wedge B$ ?
- A.A pair $(a, b)$ of a proof $a$ of $A$ and a proof $b$ of $B$
- B.A proof of $A$ or a proof of $B$
- C.A function from proofs of $A$ to proofs of $B$
- D.The truth value 'true' for both $A$ and $B$
2.
What is the most general simple type of $\lambda f.\, \lambda g.\, \lambda x.\, f\,(g\, x)$ , and hence which tautology does it prove?
- A. $(B \to C) \to (A \to B) \to A \to C$
- B. $(A \to B) \to (B \to C) \to A \to C$
- C. $(A \to B) \to A \to B$
- D. $A \to B \to C$
3.
Which of these types are inhabited by a closed term (equivalently, are theorems of intuitionistic propositional logic)? Here $p, q$ are base types and $\neg A = A \to 0$ . Choose all that apply.
- A. $p \to \neg\neg p$
- B. $\neg\neg p \to p$
- C. $(p \to q) \to (\neg q \to \neg p)$
- D. $p + \neg p$
- E. $\neg\neg\neg p \to \neg p$
4.
In the two-state Kripke model $w_0 \le w_1$ with $p$ known only at $w_1$ , which formulas are forced at $w_0$ ? (Rules: $w \Vdash A \to B$ iff every $v \ge w$ forcing $A$ forces $B$ ; $\bot$ is forced nowhere, $\neg A = A \to \bot$ ; $w \Vdash A \vee B$ iff $w \Vdash A$ or $w \Vdash B$ .) Choose all that apply.
- A. $\neg\neg p$
- B. $p$
- C. $\neg p$
- D. $p \vee \neg p$
5.
Let $A$ be a base type. How many closed β-normal terms of type $A \to A \to A$ are there (counting α-equivalent terms once)?
6.
In the proof of soundness for Kripke models (Theorem 3), the $\to$ -introduction case goes: assume $w$ forces all of $\Gamma$ , let $v \ge w$ force $A$ ; then $v$ forces all of $\Gamma, A$ , so $v \Vdash B$ by induction. Which fact justifies ' $v$ forces all of $\Gamma$ '?
- A.Persistence: what is forced at $w$ stays forced at every $v \ge w$
- B.Reflexivity of $\le$
- C.The induction hypothesis for $\Gamma, A \vdash B$
- D.Excluded middle at $v$
7.
With addition on $\N$ defined by $m + \mathsf{zero} = m$ and $m + \mathsf{succ}\, n = \mathsf{succ}(m + n)$ , why is $n + 0 = n$ true by computation while $0 + n = n$ needs induction?
- A.The recursion is on the second argument, so $n + \mathsf{zero}$ unfolds by the first equation for any $n$ , but $\mathsf{zero} + n$ cannot unfold until $n$ is known to be $\mathsf{zero}$ or a successor.
- B.Because addition is not commutative in type theory.
- C.Because $0 + n = n$ is false for some $n$ .
- D.Because proofs by computation are not allowed for statements with variables.
8.
The lesson's Lean file proves both peirce_classical (A B : Prop) : ((A → B) → A) → A and peirce_uninhabited : ¬ ∃ t, HasType [] t (((Ty.base 0 ⇒ Ty.base 1) ⇒ Ty.base 0) ⇒ Ty.base 0). Why is this not a contradiction?
- A.The first is about Lean's own propositions and uses the axiom Classical.choice; the second is about a different formal system (the simply typed λ-calculus defined in the file), studied as a mathematical object.
- B.One of the two proofs must contain sorry.
- C.Lean is inconsistent.
- D.Ty.base 0 and A are the same, so the statements contradict each other only when A is false.
9.
Write forces(w, f, le, val) for implicational formulas in a finite Kripke model. A formula is either an atom (a string such as 'p') or a tuple ('imp', A, B). le is a set of pairs (u, v) meaning $u \le v$ (reflexive and transitive), and val[w] is the set of atoms known at w. Use: atoms are forced when known; ('imp', A, B) is forced at w iff every v with (w, v) in le that forces A also forces B.
Computational — Practice

Answer key — Type theory and propositions as types

1.
A proof of $A \wedge B$ is a pair $(a, b)$ with $a : A$ and $b : B$ ; the type is $A \times B$ . Using it means projecting: $\pi_1 : A \times B \to A$ and $\pi_2 : A \times B \to B$ . In Lean, fun ⟨a, b⟩ => ⟨b, a⟩ proves $A \wedge B \to B \wedge A$ .
2.
With $x : A$ and $g : A \to B$ we get $g\, x : B$ ; with $f : B \to C$ , $f\,(g\, x) : C$ . Abstracting gives $(B \to C) \to (A \to B) \to A \to C$ : if $B$ implies $C$ and $A$ implies $B$ , then $A$ implies $C$ . The unification algorithm in the experiment finds exactly this (with letters renamed).
3.
Inhabited: $p \to \neg\neg p$ (by $\lambda a\, k.\, k\, a$ ), contraposition (by $\lambda f\, k\, a.\, k\,(f\, a)$ ) and $\neg\neg\neg p \to \neg p$ (by $\lambda h\, a.\, h\,(\lambda k.\, k\, a)$ ). Not inhabited: $\neg\neg p \to p$ and $p + \neg p$ , both classical tautologies refuted by the two-state Kripke model.
4.
$p$ : only at $w_1$ . $\neg p$ : nowhere, since $p$ holds at $w_1$ , which lies above both states. Hence $\neg\neg p$ holds everywhere (vacuously), in particular at $w_0$ , while $p$ does not: the model refutes $\neg\neg p \to p$ . And $p \vee \neg p$ fails at $w_0$ . By soundness, neither $\neg\neg p \to p$ nor $p \vee \neg p$ has a proof term.
5.
A closed normal term of type $A \to A \to A$ must be $\lambda x{:}A.\, \lambda y{:}A.\, M$ with $M$ normal of type $A$ in context $x, y : A$ . A normal term of base type is a variable applied to arguments, and $x, y$ are not functions, so $M$ is $x$ or $y$ . Exactly $2$ terms: $\lambda x\, y.\, x$ and $\lambda x\, y.\, y$ — the Church booleans $\mathsf{TRUE}$ and $\mathsf{FALSE}$ . Proof-theoretically: the formula $A \to A \to A$ has exactly two normal proofs.
6.
Persistence (monotonicity): if $w \le v$ and $w \Vdash C$ then $v \Vdash C$ . For atoms this is the condition on Kripke models; for implications it follows from transitivity. In Lean it is forces_mono, used in the impI case of Derivable.sound.
7.
The definition recurses on the second argument, so $n + \mathsf{zero}$ reduces to $n$ by the first equation whatever $n$ is. But $\mathsf{zero} + n$ with $n$ a variable matches neither equation: it is stuck. Induction supplies the missing step: $0 + \mathsf{zero} = \mathsf{zero}$ by computation, and $0 + \mathsf{succ}\, n = \mathsf{succ}(0 + n) = \mathsf{succ}\, n$ by computation and the induction hypothesis.
8.
peirce_classical is a statement in Lean's logic, proved with excluded middle (from Classical.choice). peirce_uninhabited is a theorem about the simply typed λ-calculus, an inductive datatype defined in the file: no term of that calculus has Peirce's type, as the Kripke model shows. A stronger system can prove that a weaker one cannot prove something — this is routine in logic.
9.
```
def forces(w, f, le, val):
    if isinstance(f, str):
        return f in val[w]
    _, a, b = f
    return all(not forces(v, a, le, val) or forces(v, b, le, val)
               for (u, v) in le if u == w)
```
The tests rebuild the proof of Theorem 4: in the two-state model, $(p \to q) \to p$ is forced at state $0$ but $p$ is not, so Peirce's law fails there, while the K and S axioms are forced (as soundness predicts for every theorem).