Practice: Categorical logic

Categorical logic

Warm-upHuman

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$ ?

Choose one

\neg W = \varnothing

and

\neg\neg W = \R

\neg W = \{0\}

and

\neg\neg W = W

\neg W = \varnothing

and

\neg\neg W = W

\neg W

is undefined because

W

is not closed

Categorical logic

Warm-upHuman

Which of these categories are cartesian closed? (Choose all that apply.)

Choose all that apply

\mathbf{Set}

The chain

0 \lt \tfrac12 \lt 1

as a poset category

\mathbf{Grp}

(\N, \le)

as a poset category

\mathbf{FinSet}

Categorical logic

CoreHuman

In the three-element Heyting algebra $0 \lt \tfrac12 \lt 1$ , for how many elements $a$ does $a \vee \neg a = 1$ hold?

Categorical logic

CoreHuman

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?

Choose one

\forall y\,(\varphi \wedge \psi) \iff \forall y\,\varphi \wedge \forall y\,\psi

\exists y\,(\varphi \vee \psi) \iff \exists y\,\varphi \vee \exists y\,\psi

\forall y\,(\varphi \vee \psi) \iff \forall y\,\varphi \vee \forall y\,\psi

\exists y\,(\varphi \wedge \psi) \iff \exists y\,\varphi \wedge \exists y\,\psi

Categorical logic

CoreHuman

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?

Choose one

\vee

-elimination; because

c \wedge -

is a left adjoint (of

c \Rightarrow -

) and so preserves joins

\to

-introduction; because every lattice is distributive

\vee

-introduction; because joins are least upper bounds

\to

-elimination; because

(a \Rightarrow b) \wedge a \le b

Categorical logic

CoreFormal

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)?

Choose one

f ⁻¹' T ⊆ S ↔ T ⊆ forallAlong f Sf '' S ⊆ T ↔ S ⊆ f ⁻¹' TforallAlong f S ⊆ T ↔ S ⊆ f ⁻¹' TT ⊆ forallAlong f S ↔ f '' S ⊆ T

Categorical logic

CoreHuman

How many closed βη-normal terms of type $A \times A \to A \times A$ are there, for a base type $A$ ?

Categorical logic

StretchHuman

A student claims: "Intuitionistic logic proves $\neg(P \vee \neg P)$ ; that is what rejecting excluded middle means." Which response is correct?

Choose one

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.The claim is true, because

p \vee \neg p

is not derivableThe claim is true in

\mathcal{O}(\R)

, since there

U \vee \neg U \ne \R

for

U = (0, \infty)

The question is meaningless, because intuitionistic logic has no negation

Categorical logic

StretchComputational

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.

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.