Categories of logical formulae

Consider the set of formulas of a logic. If there was only one sort of "unary" deduction $\phi \Rightarrow \psi$ - like $(\forall x)\phi(x) \Rightarrow \phi(a)$ - we would immediately have a category of formulas (with deductibility $\Rightarrow$ as morphism). But alas, there are other ("higher") deduction rules, e.g.

$\lbrace p, q \rbrace \Rightarrow p \wedge q$ (rule of conjunction)

$\lbrace p\rightarrow q, p \rbrace\Rightarrow q$ (modus ponens)

(How) can formulas of "classical logics" (propositional and FO) be made into a category despite of those other relations (= rules)?

-

Classical propositional logic is basically a boolean algebra, which may be viewed as a poset, which may be viewed as a category. We at the very least need to fix the primitive predicates; then the objects of the category are the well-formed formulae, and we have a morphism $P \to Q$ if and only if $\{ P \} \vdash Q$, where $P$ and $Q$ are well-formed formulae. Under this scheme, the product is logical conjunction, the coproduct is logical disjunction, and the exponential is material implication. (Write out the universal properties in logical form and you'll see they correspond to the natural deduction rules for the respective logical operators.)

We may also talk about the category of boolean algebras, where the morphisms are boolean algebra homomorphisms, but I think that's not what you're looking for.

As for first-order logic — a similar thing can be done, but now we have to introduce several (indeed, infinitely many) categories. Firstly, recall that a formula in first-order logic can have free variables. Formulae that have the same free variables live in the same categories; as before we have a morphism $\phi(x, y, \ldots, z) \to \psi(x, y, \ldots, z)$ iff $\{ \phi(x, y, \ldots, z) \} \vdash \psi(x, y, \ldots, z)$, and we have categorical products, coproducts, and exponentials corresponding to $\land$, $\lor$, and $\implies$ as before.

What do $\forall$ and $\exists$ correspond to? Well, remember that the formulae inside a given category have the at most a particular set of free variables, so these operations necessarily take objects from one category to another, i.e. they must be functors of some kind, and indeed they are. Let $\mathrm{Form}(x, y, \ldots, z)$ denote the category of formulae with free variables contained in $\{ x, y, \ldots, z \}$. Trivially, we have inclusion functors $* : \mathrm{Form}(x, y, \ldots, z) \to \mathrm{Form}(x, y, \ldots, z, t)$. Conversely, $\forall t$ is a functor $\mathrm{Form}(x, y, \ldots, z, t) \to \mathrm{Form}(x, y, \ldots, z)$. It turns out $\forall t$ is a right adjoint for $*$ — writing out the definition of adjunction gives the natural deduction rules for $\forall$ introduction and elimination. Similarly, $\exists t$ is a functor of the same type, and is a left adjoint of $*$.

This categorical viewpoint of logic is discussed at various points in Awodey's Category Theory, but is not the main aim of the book.

-
@Zhen Lin: Thanks again for this answer, which I really learned to appreciate only yesterday. Can you give me some more references (next to Awodey)? – Hans Stricker Aug 26 '11 at 8:26
@Hans: I'm afraid I haven't read much of the literature at all, so I can't really help there. There's a very brief discussion in Appendix A of Lawvere and Rosebrugh's Sets for Mathematics, but I think it's secretly about semantics more than syntax (and a prelude to an exposition on the internal logic of a topos). Mac Lane and Moerdijk's Sheaves in Geometry and Logic has a section on the ‘syntactic topos’ of a theory but I don't yet understand what that is about; I suspect it's not really what you want either. – Zhen Lin Aug 26 '11 at 8:42
@Zhen Lin: Thanks anyway! – Hans Stricker Aug 26 '11 at 8:53

The Lindenbaum algebra is a natural Boolean algebra associated with any theory $T$. The Lindenbaum algebra can be taken to consist of equivalence classes of formulas, where two formula are equivalent if they are proved equivalent by $T$, and the Boolean algebra structure is inherited naturally from the syntax. Since the Lindenbaum algebra is a Boolean algebra, it admits of diverse characterizations in mathematics, for every Boolean algebra can be viewed alternatively as a ring (a Boolean ring), as an algebraic structure (with $\wedge$ and $\vee$), as a partial order (defined by an order $\leq$ with certain properties, such as lub, glb and complements), as a lattice (either with $\wedge$ and $\vee$ or $\leq$) or finally, as a category (since every partial order can be viewed as a category).

-
@Joel: Thanks, happy to hear from you again! But to be honest: I didn't want to presuppose any theory $T$, just naked formulae. – Hans Stricker Jan 2 '11 at 0:47
In that case, Hans, you've just got the empty theory $T$, and it is a special case. – Joel David Hamkins Jan 2 '11 at 0:53
The point I obviously didn't make clear enough is, that I am looking for a relation (= morphism) that is purely and immediately syntactical. That is: I am not looking for formualae that are "provably equivalent" (which might be very hard to show), but "obviously equivalent" (by a small set of rules). – Hans Stricker Jan 2 '11 at 0:58
@Hans: Your requirement seems problematic---if we compose all the "obvious" implications in the proof of Fermat's Last Theorem, then morphism we get is a far from obvious implication. Closure under composition means that if we allow simple proofs, we need complicated ones as well. – Daniel Litt Jan 2 '11 at 1:01
@Daniel: The "obvious" implications should build the skeleton only, is it possible to formulate this? – Hans Stricker Jan 2 '11 at 1:07

I think you actually identified a correct categorical structure on the set of formulae. Namely, let the objects be valid formulae, with a single morphism $p\to q$ if $p\implies q$. Then ternary relations like $p, q\implies p\wedge q$ are encoded in the categorical structure via the fact that $p\wedge q$ is the categorical product of $p$ and $q$. Similarly, modus ponens follows by looking at the slice category over $q$, for example.

EDIT: Upon further reflection, there's a slightly more complicated category which may also encapsulate what you want. Namely, let objects be valid formulae, and let morphisms be proofs, with composition given by concatenation and the identity given by the empty proof. The remarks about products, modus ponens, etc. seem to still hold for this more complicated category.

-
@Daniel: You write "$p\rightarrow q$ if $p \Rightarrow q$". What does your "$p\Rightarrow q$" mean? – Hans Stricker Jan 2 '11 at 0:33
To clarify, I mean that there should be a single morphism from $p$ to $q$ if $p$ implies $q$. – Daniel Litt Jan 2 '11 at 0:33
That is maybe what I initially thought of (but couldn't make final sense): $p \wedge q$ implies $p$ and $q$, but this doesn't force $p \wedge q$ "to be true" when $p$ and $q$ "are true". How can the latter be achieved? – Hans Stricker Jan 2 '11 at 0:43
Well as long as every operation you're interested in is encoded in the categorical structure, you simply say "the set of 'true' statements is the least subcategory containing $p$ and $q$ and satisfying such and such," (e.g. closed under products). JDH's answer might give you a little more wiggle room (though I think the category he alludes to is exactly the skeleton of the one I suggest), in that it is easier to talk about things like ideals, etc. in a Boolean algebra. Of course it is all the same. – Daniel Litt Jan 2 '11 at 0:48
It is a free category, but I don't think your remark on products is true. Namely we only need a unique proof of $P\wedge Q$ from $R$ *for each proof of $P,Q$ from $R$. This holds as long as there's some mild equivalence relation on proofs, e.g. if two parts of a proof are logically independent, we allow them to be reordered. Of course actually defining such an equivalent relation coherently might be difficult/impossible. – Daniel Litt Jan 2 '11 at 15:40

I suspect the notion you are looking for is either a multicategory or a polycategory. Multicategories generalise categories by allowing more than one object in the domain of an arrow. These were introduced by Lambek specifically for the study of logical derivations. See

J. Lambek (1969) "Deductive Systems and Categories (II)" in Category Theory, Homology Theory and their Applications I, Springer Lecture Notes in Mathematics 87, R. J. Hilton (ed.)

Polycategories generalise multicategories by allowing multiple objects in the codomain of an arrow. See

M. E. Szabo (1975) "Polycategories", Communications in Algebra 3.

Of course there is a rich history of looking at categories whose objects are formula and whose arrows are proofs, coming mostly from the computer science literature. Lambek and Scott's book may be a good place to start, or for a more modern take try this introductory article http://arxiv.org/abs/1102.1313 However, for classical logics such categories always reduce to boolean algebras, so people tend to work with intuitionistic or linear logics.

-

I found the answers to a somehow related question on Entailment and Implication @ n-Category Café very enlightening, too.

-