Propositional logic with categories

I have some vague sense that certain types of categories are related to certain types of logic. I've been meaning to learn more about this, so I thought I'd ask about the simplest case, propositional logic. In particular, I'd be interested in a statement of the completeness theorem for propositional logic using these ideas (something like a representation theorem for a certain class of categories).

Here's what I think is a start: a propositional calculus should, at least, behave like a bicartesian closed category $C$, possibly satisfying some extra conditions. The product should be $\vee$, the coproduct should be $\wedge$, and the exponential object should be $\rightarrow$. I think the terminal object is $\top$ and the initial object is $\bot$, and the exponential $p \rightarrow \bot$ should then be $\neg p$. Maybe this means the same thing as "Heyting algebra."

We're specifically interested in the free bicartesian closed category $C_P$ on a set $P$ of primitive propositions, and in functors from $C_P$ to the truth-value category $\mathbf{2} = \{ \bot \rightarrow \top \}$. If I've set up the definitions correctly, then a subset $S$ of $C_P$ semantically entails an object $t$ if and only if, for every functor $F : C_P \to \mathbf{2}$ such that $F(s) = \top \forall s \in S$, it is also true that $F(t) = \top$.

If I've set up the definitions correctly, functors like $F$ are defined by what they send to $\top$. If we want to characterize such sets syntactically, we write down some set of axioms and some set of inference rules telling us when objects sent to $\top$ let us construct other objects sent to $\top$, and then the completeness theorem tells us that these axioms and inference rules characterize the functors $F$.

But I'm clearly missing something important: at some point we introduce the law of the excluded middle, and then our Heyting algebras should collapse to Boolean algebras. But I'm not sure exactly when that point is. Can someone help me out? I suspect this is an exercise in a book on topos theory somewhere.

Qiaochu, let me see if this answers your question:

Proposition: Suppose $B$ is a cartesian closed category with finite coproducts such that the canonical double dual embedding

$$b \to (b \Rightarrow 0) \Rightarrow 0$$

is an isomorphism (excluded middle). Then $B$ is equivalent (as a category) to a poset, and hence to a Boolean algebra.

Proof: First, in a cartesian closed category with $0$, for any object $b$ there exists a morphism $i: b \to 0$ only if $i$ is an isomorphism. For given $i$, the composite

$$b \stackrel{\langle i, 1_b \rangle}{\to} 0 \times b \stackrel{\pi_2}{\to} b$$

is an isomorphism. But $\pi_1: 0 \times b \to 0$ is an isomorphism since $- \times b$ preserves colimits by cartesian closure. Thus the composite of $i: b \to 0$ followed by the unique map $0 \to b$ is $1_b$. Since $0$ is initial, the composite of $0 \to b$ followed by $i: b \to 0$ is $1_0$. Hence $i$ is an isomorphism. In particular, there can be at most one morphism $b \to 0$ (again by initiality).

Next, for any two objects $b, c$ there can be at most one morphism $b \to c \Rightarrow 0$, since there are in bijective correspondence with morphisms $b \times c \to 0$, of which there is at most one. Finally, taking $c = b' \Rightarrow 0$ and assuming excluded middle, we have that for any two objects $b, b'$ there is at most one morphism $b \to b'$. $\Box$

The property of existence of $b \to 0$ forcing $b$ to be initial is called strictness of the initial object, and I think Mac Lane-Moerdijk prove that an initial object is strict in a cartesian closed category. I know this is in my notes on ETCS.

Edit: Qiaochu's instincts are correct. There is an old tradition in category theory, going back essentially to Lawvere's thesis, whereby one forms syntactic categories associated to theories and to various fragments of logic, and these are typically free categorical structures of various sorts. For example, the theory of groups is the free (initial) category with products containing a group object; the morphisms are well-formed terms in the equational language modulo the equational axioms imposed by the theory. A model of the theory will be a functor which preserves the categorical structure needed to express the logic (finite products in the case of finitary equational theories). A completeness theorem for a certain class of models says that whenever the semantic interpretations of two syntactic terms (or morphisms in the free categorical structure) are equal in each of the models of the class, then the syntactic terms are provably equivalent.

From the viewpoint of categorical logic, such completeness theorems can be seen as embedding or representation theorems. In spirit these go back to the Freyd-Mitchell embedding theorems; for example, each module category is a model of the abelian category axioms, and if a diagram commutes when interpreted in each such model, then it provably commutes on the basis of the abelian category axioms. Or, in categorical logic there is a notion of 'coherent theory' whose syntactic category is effectively its classifying topos, and there is a theorem due to Deligne that such a theory has 'enough points' (which are left exact left adjoints from the classifying topos to the category of sets). This can be interpreted either as saying that the classifying topos of the theory can be faithfully embedded (lex left-adjointly) into a product of copies of $Set$, or as saying that two morphisms are provably equivalent in the theory if their values under any set-theoretic model are equal.

Qiaochu's question has to do with bicartesian closed categories, seen as a natural categorification of the concept of Heyting algebra (the algebraic formalization of intuitionistic propositional logic, as Boolean algebras are the algebraic formalization of classical propositional logic). Here one can form appropriate syntactic categories as free bicartesian closed categories generated by a given set of sorts, or even by a given category of sorts. Now, there is still another tradition in categorical logic, due to Lambek and his school, whereby such free structures are constructed explicitly by taking suitable equivalence classes of formal Gentzen sequent deductions pertaining to the given fragment of logic, which here is intuitionistic propositional logic. The equivalence classes are dictated by naturality considerations and other compatibility conditions, reflecting the key conversions one sees in cut-elimination; see Girard's Proofs and Types. One can consult Manfred Szabo's Algebra of Proofs for a careful description of how this is done for quite a variety of logics, including, I believe, the case Qiaochu is interested in.

Off hand I am not sure what sort of completeness theorems there are for bicartesian closed categories (e.g., is there a faithful structure-preserving functor from a free bicartesian closed category to some power of $Set$? I have a sneaking suspicion finite sets are not enough). But perhaps the answer can be found in Freyd-Scedrov's Categories, Allegories, which contains a wealth or representation/embedding/completeness theorems [one of the great scientific themes of Freyd's career].

• Thanks, Todd. This answers one of my questions, but I'm also curious whether there is a natural way to talk about syntactic implication in this category-theoretic framework. – Qiaochu Yuan Oct 23 '10 at 13:56
• By syntactic implication you mean formal proofs? Proofs (or more carefully, Lambek-equivalence classes of proofs) can be viewed as morphisms in free structures such as the free bicartesian closed category on a set of variables you mentioned (and of course this will be much richer than just the free Heyting algebra on the set of variables). Is that the kind of thing you mean? In that case one can talk about completeness theorems by associating them with embedding theorems a la Freyd. – Todd Trimble Oct 23 '10 at 14:44
• @Todd: yes, that sounds right. If you could briefly comment on how that works in your answer I'd be happy to accept. – Qiaochu Yuan Oct 23 '10 at 21:48
• Hm, wasn't too brief it seems, but maybe some worthwhile suggestions for further reading. – Todd Trimble Oct 24 '10 at 0:31
• @Todd: regarding completeness, I think Dougherty and Subrahmanyan's "Equality Between Functionals in the Presence of Coproducts" establishes that lambda-calculus with coproducts (and hence biCCCs) are complete for the equations valid for any set-theoretic model with an infinite base type. I don't know what the state of the art is for finite models, though. – Neel Krishnaswami Oct 24 '10 at 9:43

This paper by Abramsky relates Joyal's Lemma on the collapse of a cartesian closed category with a dualizing object to no cloning theorems and no deleting theorems in quantum mechanics.