The n-Category Café

But, you’re supposed to be finishing that ‘Rosetta Stone’ paper, where you explain how symmetric monoidal closed categories show up in many different guises in logic, topology, and physics.

(Ducks fireball ) No, wait! I’ve been working on it! I understand what I’m supposed to be writing about a lot better now. For example, here’s what it means to be a multiplicative intuitionistc linear logic (MILL):

• in linear logic, propositions are resources, like a bolt. We can’t use the same bolt to hold on the wheel of my bike and the door of a car!

• in multiplicative logic, we can get new resources by sticking others together. For example,

  sandwich = bread $\otimes$ peanut butter $\otimes$ jam $\otimes$ bread

  Note that the order matters! The empty resource is denoted $I$.

• in intuitionistic logic, a proposition is true iff there’s a proof of it, and a proposition is false iff there’s a proof of its negation. So statements that were tautologies in classical logic, like $P \wedge \neg P,$ don’t hold any more.

  But what’s the proof of a resource!? It’s a process for taking a resource and turning it into something else:

  grind : wheat $\to$ flour.

  There can be lots of different ways to transform a resource of one kind $A$ into a resource of another kind $B$. The set of ways to do that is denoted $A \vdash B.$

  A description of a process is a recipe, and a recipe is a resource itself. It’s a proposition that the set $A \vdash B$ is nonempty, and is denoted $A \multimap B.$ A proof of $A \multimap B$ from no assumptions is a process

  $f:I \to A \multimap B$

  that produces (from nothing) a recipe for converting an $A$ into a $B$—a description of an element of the set $A \vdash B$! For each process in the set, there’s a corresponding recipe, and that’s currying.

I’ve also understood the difference between Hilbert style proofs (all the complexity in the axioms, with only one inference rule modus ponens) and Gentzen-style proofs (one axiom, hyp, and lots of inference rules).

I understand how the axioms that are usually given aren’t really axioms, they’re “axiom schemata,” which says that any process of the proper form is an axiom. The usual inference rules work the same way: for every process of a given form, we get another process of this other form.

This comes into play when we try to translate from the function symbols in the theory of a braided monoidal closed category (BMCC) into the language of MILL: they’re really specific processes, but we can encode them as inference rules that mention specific resources in the same way that the left and right unitors mention the void resource.

Also, I drew up dinatural transformation diagrams that show how the axiom hyp says that composition has left and right units, while the inference rule cut says that composition is associative.

I pared down Lambek & Scott’s definiton of a cartesian closed category (CCC) until I was left with a BMCC. Now I’m working on pictures for the string diagrams.