Feeds:
Posts

## A transcript of my qualifying exam

I passed my qualifying exam last Friday. Here is a copy of the syllabus and a transcript.

Although I’m sure there are more, I’m only aware of two other students at Berkeley who’ve posted transcripts of their quals, namely Christopher Wong and Eric Peterson. It would be nice if more people did this.

## How to invent intuitionistic logic

(This is an old post I never got around to finishing. It was originally going to have a second half about pointless topology; the interested reader can consult Vickers’ Topology via Logic on this theme.)

Standard presentations of propositional logic treat the Boolean operators “and,” “or,” and “not” as fundamental (e.g. these are the operators axiomatized by Boolean algebras). But from the point of view of category theory, arguably the most fundamental Boolean operator is “implies,” because it gives a collection of propositions the structure of a category, or more precisely a poset. We can endow the set of propositions with a morphism $p \to q$ whenever $p \Rightarrow q$, and no morphisms otherwise. Then the identity morphisms $\text{id}_p : p \to p$ simply reflect the fact that a proposition always implies itself, while composition of morphisms

$\displaystyle (p \Rightarrow q) \wedge (q \Rightarrow r) \to (p \Rightarrow r)$

is a familiar inference rule (hypothetical syllogism). Since it is possible to define “and,” “or,” and “not” in terms of “implies” in the Boolean setting, we might want to see what happens when we start from the perspective that propositional logic ought to be about certain posets and figure out how to recover the familiar operations from propositional logic by thinking about what their universal properties should be.

It turns out that when we do this, we don’t get ordinary propositional logic back in the sense that the posets we end up identifying are not just the Boolean algebras: instead we’ll get Heyting algebras, and the corresponding notion of logic we’ll get is intuitionistic logic.