Feeds:
Posts

## 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.

## The cohomology of the n-torus

The goal of this post is to compute the cohomology of the $n$-torus $X = (S^1)^n \cong \mathbb{R}^n/\mathbb{Z}^n$ in as many ways as I can think of. Below, if no coefficient ring is specified then the coefficient ring is $\mathbb{Z}$ by default. At the end we will interpret this computation in terms of cohomology operations.

## Decisions, decisions

Newcomb’s paradox is the name usually given to the following problem. You are playing a game against another player, often called Omega, who claims to be omniscient; in particular, Omega claims to be able to predict how you will play in the game. Assume that Omega has convinced you in some way that it is, if not omniscient, at least remarkably accurate: for example, perhaps it has accurately predicted your behavior many times in the past.

Omega places before you two opaque boxes. Box A, it informs you, contains $1,000. Box B, it informs you, contains either$1,000,000 or nothing. You must decide whether to take only Box B or to take both Box A and Box B, with the following caveat: Omega filled Box B with \$1,000,000 if and only if it predicted that you would take only Box B.

What do you do?

(If you haven’t heard this problem before, please take a minute to decide on an option before continuing.)

## Cartesian closed categories and the Lawvere fixed point theorem

Previously we saw that Cantor’s theorem, the halting problem, and Russell’s paradox all employ the same diagonalization argument, which takes the following form. Let $X$ be a set and let

$\displaystyle f : X \times X \to 2$

be a function. Then we can write down a function $g : X \to 2$ such that $g(x) \neq f(x, x)$. If we curry $f$ to obtain a function

$\displaystyle \text{curry}(f) : X \to 2^X$

it now follows that there cannot exist $x \in X$ such that $\text{curry}(f)(x) = g$, since $\text{curry}(f)(x)(x) = f(x, x) \neq g(x)$.

Currying is a fundamental notion. In mathematics, it is constantly implicitly used to talk about function spaces. In computer science, it is how some programming languages like Haskell describe functions which take multiple arguments: such a function is modeled as taking one argument and returning a function which takes further arguments. In type theory, it reproduces function types. In logic, it reproduces material implication.

Today we will discuss the appropriate categorical setting for understanding currying, namely that of cartesian closed categories. As an application of the formalism, we will prove the Lawvere fixed point theorem, which generalizes the argument behind Cantor’s theorem to cartesian closed categories.

## The homotopy groups are only groups

Often in mathematics we define constructions outputting objects which a priori have a certain amount of structure but which end up having more structure than is immediately obvious. For example:

• Given a Lie group $G$, its tangent space $T_e(G)$ at the identity is a priori a vector space, but it ends up having the structure of a Lie algebra.
• Given a space $X$, its cohomology $H^{\bullet}(X, \mathbb{Z})$ is a priori a graded abelian group, but it ends up having the structure of a graded ring.
• Given a space $X$, its cohomology $H^{\bullet}(X, \mathbb{F}_p)$ over $\mathbb{F}_p$ is a priori a graded abelian group (or a graded ring, once you make the above discovery), but it ends up having the structure of a module over the mod-$p$ Steenrod algebra.

The following question suggests itself: given a construction which we believe to output objects having a certain amount of structure, can we show that in some sense there is no extra structure to be found? For example, can we rule out the possibility that the tangent space to the identity of a Lie group has some mysterious natural trilinear operation that cannot be built out of the Lie bracket?

In this post we will answer this question for the homotopy groups $\pi_n(X)$ of a space: that is, we will show that, in a suitable sense, each individual homotopy group $\pi_n(X)$ is “only a group” and does not carry any additional structure. (This is not true about the collection of homotopy groups considered together: there are additional operations here like the Whitehead product.)

## New page on reading recommendations

I’ve added a new page of reading recommendations, mostly for undergraduates, to the top. The emphasis is intended to be on well-written and accessible books. Comments and suggestions welcome.

## The p-group fixed point theorem

The goal of this post is to collect a list of applications of the following theorem, which is perhaps the simplest example of a fixed point theorem.

Theorem: Let $G$ be a finite $p$-group acting on a finite set $X$. Let $X^G$ denote the subset of $X$ consisting of those elements fixed by $G$. Then $|X^G| \equiv |X| \bmod p$; in particular, if $p \nmid |X|$ then $G$ has a fixed point.

Although this theorem is an elementary exercise, it has a surprising number of fundamental corollaries.