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

The Lumenary · First-year graduate

Categorical logic

Name: ______________________

Date: ______________________

You will learn to

Interpret the simply typed λ-calculus with products in a cartesian closed category, prove that βη-equal terms have equal interpretations, and show that $\mathbf{Set}$ is cartesian closed while $\mathbf{Grp}$ is not
Express $\exists$ and $\forall$ as the left and right adjoints of substitution (pulling back predicates), and derive quantifier laws from the fact that adjoints preserve limits or colimits
Define Heyting algebras and prove that intuitionistic propositional logic is sound and complete for them
Use the open sets of $\R$ to show that $P \lor \neg P$ is not intuitionistically derivable, while $\neg\neg(P \lor \neg P)$ is
State the Curry–Howard–Lambek correspondence and place it in the wider landscape (hyperdoctrines, dependent types, toposes)

1.
In the Heyting algebra $\mathcal{O}(\R)$ of open subsets of $\R$ , let $W = \R \setminus \{0\}$ . What are $\neg W$ and $\neg\neg W$ ?
- A. $\neg W = \varnothing$ and $\neg\neg W = \R$
- B. $\neg W = \{0\}$ and $\neg\neg W = W$
- C. $\neg W = \varnothing$ and $\neg\neg W = W$
- D. $\neg W$ is undefined because $W$ is not closed
2.
Which of these categories are cartesian closed? (Choose all that apply.)
- A. $\mathbf{Set}$
- B.The chain $0 \lt \tfrac12 \lt 1$ as a poset category
- C. $\mathbf{Grp}$
- D. $(\N, \le)$ as a poset category
- E. $\mathbf{FinSet}$
3.
In the three-element Heyting algebra $0 \lt \tfrac12 \lt 1$ , for how many elements $a$ does $a \vee \neg a = 1$ hold?
4.
Since $f^* \dashv \forall_f$ , the universal quantifier is a right adjoint, and right adjoints preserve limits (in a poset: meets). Which logical law is an instance of exactly this fact?
- A. $\forall y\,(\varphi \wedge \psi) \iff \forall y\,\varphi \wedge \forall y\,\psi$
- B. $\exists y\,(\varphi \vee \psi) \iff \exists y\,\varphi \vee \exists y\,\psi$
- C. $\forall y\,(\varphi \vee \psi) \iff \forall y\,\varphi \vee \forall y\,\psi$
- D. $\exists y\,(\varphi \wedge \psi) \iff \exists y\,\varphi \wedge \exists y\,\psi$
5.
In the proof that intuitionistic logic is sound for Heyting algebras, one rule needs the distributive law $c \wedge (a \vee b) = (c \wedge a) \vee (c \wedge b)$ . Which rule, and why does the distributive law hold in every Heyting algebra?
- A. $\vee$ -elimination; because $c \wedge -$ is a left adjoint (of $c \Rightarrow -$ ) and so preserves joins
- B. $\to$ -introduction; because every lattice is distributive
- C. $\vee$ -introduction; because joins are least upper bounds
- D. $\to$ -elimination; because $(a \Rightarrow b) \wedge a \le b$
6.
With forallAlong f S = {y | ∀ x, f x = y → x ∈ S}, which Lean statement says that ∀ is right adjoint to pulling back along f : X → Y (for S : Set X, T : Set Y)?
- A.f ⁻¹' T ⊆ S ↔ T ⊆ forallAlong f S
- B.f '' S ⊆ T ↔ S ⊆ f ⁻¹' T
- C.forallAlong f S ⊆ T ↔ S ⊆ f ⁻¹' T
- D.T ⊆ forallAlong f S ↔ f '' S ⊆ T
7.
How many closed βη-normal terms of type $A \times A \to A \times A$ are there, for a base type $A$ ?
8.
A student claims: "Intuitionistic logic proves $\neg(P \vee \neg P)$ ; that is what rejecting excluded middle means." Which response is correct?
- A.The claim is false. In the two-element Boolean algebra $\neg(p \vee \neg p)$ evaluates to $\bot$ , so by soundness it is not derivable. In fact $\neg\neg(p \vee \neg p)$ is derivable.
- B.The claim is true, because $p \vee \neg p$ is not derivable
- C.The claim is true in $\mathcal{O}(\R)$ , since there $U \vee \neg U \ne \R$ for $U = (0, \infty)$
- D.The question is meaningless, because intuitionistic logic has no negation
9.
A finite topology is given as a set opens of frozensets. Write neg(opens, u), returning the pseudo-complement of the open set u (the union of all open sets disjoint from u), and is_boolean(opens, space), returning True exactly when u | neg(opens, u) == space for every open u.
Computational — Practice

Answer key — Categorical logic

1.
$\neg W = \operatorname{int}(\R \setminus W) = \operatorname{int}\{0\} = \varnothing$ , and $\neg\neg W = \neg\varnothing = \operatorname{int}(\R) = \R$ . Since $\neg\neg W = \R \ne W$ , the law $\neg\neg a = a$ fails in $\mathcal{O}(\R)$ . Note that $W \le \neg\neg W$ , as in every Heyting algebra.
2.
$\mathbf{Set}$ , $\mathbf{FinSet}$ and the finite chain are cartesian closed. $(\N, \le)$ has no terminal (greatest) object. $\mathbf{Grp}$ fails because in a CCC with an initial object $0$ we have $0 \times B \cong 0$ (as $- \times B$ is a left adjoint), but in $\mathbf{Grp}$ the initial object is the trivial group $1$ and $1 \times B \cong B$ .
3.
$\neg 0 = 1$ , $\neg\tfrac12 = 0$ and $\neg 1 = 0$ . So $0 \vee \neg 0 = 1$ and $1 \vee \neg 1 = 1$ , but $\tfrac12 \vee \neg\tfrac12 = \tfrac12$ . The answer is $2$ . The middle element witnesses that this Heyting algebra is not Boolean. It is the algebra of open sets of the Sierpiński space, and also of the subobjects of $1$ in the presheaf topos on $\{0 \lt 1\}$ .
4.
Right adjoints preserve all limits that exist. In a poset, a binary product is a meet. Applied to $\forall_\pi$ this gives $\forall_\pi(S \cap S') = \forall_\pi S \cap \forall_\pi S'$ , i.e. $\forall y\,(\varphi \wedge \psi) \iff \forall y\,\varphi \wedge \forall y\,\psi$ . Dually, the left adjoint $\exists_\pi$ preserves joins, which gives option (b). Options (c) and (d) are false, as the parity example shows.
5.
It is $\vee$ -elimination. With $c = \bigwedge \llbracket \Gamma \rrbracket$ , the premises give $c \le a \vee b$ , $a \wedge c \le x$ and $b \wedge c \le x$ , so $c = c \wedge (a \vee b) = (c \wedge a) \vee (c \wedge b) \le x$ . Distributivity holds in every Heyting algebra because $c \wedge -$ has the right adjoint $c \Rightarrow -$ , and left adjoints preserve joins. This is also why non-distributive lattices, such as the subspace lattices of quantum logic, carry no implication satisfying the deduction theorem.
6.
An adjunction $F \dashv G$ of monotone maps means $F(a) \le b \iff a \le G(b)$ . With $F = f^*$ (fun T => f ⁻¹' T) and $G = \forall_f$ (forallAlong f) this is f ⁻¹' T ⊆ S ↔ T ⊆ forallAlong f S, proved in the lesson as forall_adjoint. Option (b) is the adjunction $\exists_f \dashv f^*$ .
7.
In η-long normal form the term is $\lambda p.\,\langle s, t\rangle$ , where $s$ and $t$ are each $\pi_1 p$ or $\pi_2 p$ . That gives $2 \times 2 = 4$ terms. In $\mathbf{Set}$ they are exactly the natural transformations $(-)^2 \Rightarrow (-)^2$ . By Yoneda, $\mathrm{Nat}(\Hom(2,-), \Hom(2,-)) \cong \Hom(2,2)$ , which has $4$ elements, matching the lesson's experiment.
8.
Soundness says every derivable formula is $\top$ in every Heyting algebra. In the Boolean algebra $\{0, 1\}$ , $p \vee \neg p = 1$ and so $\neg(p \vee \neg p) = 0$ . Hence $\neg(p \vee \neg p)$ is not derivable. Theorem 6 gives an explicit derivation of $\neg\neg(p \vee \neg p)$ . Excluded middle is not assumed, and it is provably irrefutable.
9.
```
def neg(opens, u):
    return frozenset().union(*[w for w in opens if not (w & u)])

def is_boolean(opens, space):
    return all(u | neg(opens, u) == space for u in opens)
```
The union of open sets is open, so neg(opens, u) is the largest open set disjoint from u, which is the pseudo-complement $\neg u = u \Rightarrow \varnothing$ . In the Sierpiński space S, u = {1} has $\neg u = \varnothing$ , so excluded middle fails. In the discrete topology D every open set is also closed, and the algebra is Boolean.