Categories of logical formulae - MathOverflow

Categories of logical formulae

2011-01-01T23:47:57Z

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)?

Answer by Daniel Litt for Categories of logical formulae

2011-01-02T00:22:50Z

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.

Answer by Joel David Hamkins for Categories of logical formulae

2011-01-02T00:39:56Z

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

Answer by Zhen Lin for Categories of logical formulae

2011-01-02T03:01:55Z

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.

Answer by Hans Stricker for Categories of logical formulae

2011-01-11T08:02:48Z

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

Answer by Ross Duncan for Categories of logical formulae

2012-09-06T14:57:34Z

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.