Citation: Baez, John, and Mike Stay. "Physics, topology, logic and computation: a Rosetta Stone". Springer Berlin Heidelberg, 2011.
Web: https://arxiv.org/abs/0903.0340
Tags: Philosophical, Monoidal-categories
This paper outlines a precise sense in which physics, topology, logic, and computation are analogous. The analogy is that there are natural ways of constructing closed braided monoidal categories in each of these settings, and so category theory gives an analogy between them.
The physics and topology front is pretty clear. The category of Hilbert spaces is monoidal and has an internal hom given by the tensor product. The category of bordisms is monoidal and its internal hom is given by the tensor product as well. When the internal hom is given by the tensor product we call a category compact - the category of Hilbert spaces and bordisms are both compact. This analogy is obviously quite useful and well explored, especially in TQFTs which are symmetric monoidal functors from bordisms to Hilbert spaces.
A separate analogy says that logic is like computation. Here, we say that propositions are like types and proofs are like computations. Of course computations have to be totally functional in this setting, so the exact way of turning computation into a category is to think about lambda calculus. Seeing as logic and computation are closely related fields, this correspondence has been known since the 1970s, with roots back to even the 1950s:
> Curry, Haskell Brooks, et al. Combinatory logic. Vol. 1. Amsterdam: North-Holland, 1958.
> Howard, William A. "The formulae-as-types notion of construction." To HB Curry: essays on combinatory logic, lambda calculus and formalism 44 (1980): 479-490.
> Farooqui, Husna. "The Curry-Howard Correspondence." (2021).
The insight of this paper is that both of these well-establishes two-fold analogies can be viewed as part of a larger four-fold analogy, because the structure of both of these analogies is that the theories and question can be used to make categories. This is a nice idea.
I also like some of the side-comments in this paper. There is a general sense in which functors are like representations. Of course, representations of the 1-object group category are literally representations of the group. Representations of the bordism category are TQFTs. In logic, representations of an axiomatic system are models! There is a general sense in which representations of an object are more real than the object itself, because a representation tells you how it acts on the world.