What theory of logic or types considers the "category of propositions"?

Question

Was wondering if there was a theory already out there that considers the "category $\text{Prop}$ of propositions". It is a preorder (at most one arrow between two propositions), in which $A \to B$ means that if the proposition $A$ is proved, assumed, or defined true then $B$ is a (similarly) true proposition. Arrows compose associatively when the objects take on positive truth values. And so a category is formed.

Note that the category contains not just true propositions but any proposition. An arrow will connect two possibly false propositions when assuming one would prove the other true. I guess this would come in handy when doing a long proof-by-contradiction.

Question. Was wondering what theory most closely mimics this situation, since usally in proof assistants $A \implies B \implies C$ is read right-associatively: $A \implies (B \implies C)$. Or in other words we can't speak of a category where $\implies$ is data of an arrow (since associativity of composition is dropped for (mostly) philosophical reasons).

In $\text{Prop}$, given two propositions $A, B$, we have that ($A$ and $B$) is their categorical product and that similarly ($A$ or $B$) is their categorical coproduct. Thus this category has finite products and coproducts.

Answer 1

There is a "small" way to do this and a "big" way to do this that I'm aware of. The "small" way is to axiomatize what properties you'd want a category of propositions to satisfy and see what pops up. If you require that

• the category of propositions is a poset
• in which every finite set of propositions has a product ("and") and coproduct ("or"), including the empty set, meaning there is a terminal object ("true") and an initial object ("false")

then the categories you get this way are precisely the bounded lattices. If you further require that

• every pair of propositions $a, b$ has an exponential object $a \Rightarrow b$ ("implies")

then you get precisely the Heyting algebras. These are a setting for doing intuitionistic logic, in which the law of excluded middle doesn't necessarily hold. See this blog post for a bit more detail.

(The fact that $\Rightarrow$ isn't associative has nothing to do with whether or not composition is associative.)

In a Heyting algebra you can define the negation $\neg a$ of a proposition to be the exponential $a \Rightarrow \bot$. Every proposition admits a canonical double negation map $a \to \neg \neg a$, and the condition that this map is always an isomorphism (equivalently, that $a = \neg \neg a$) is satisfied for precisely the Boolean algebras. For every set $X$ the powerset $2^X$ is a Boolean algebra whose elements can be interpreted as propositions about elements of $X$, and when $X$ is finite the double powerset $2^{2^X}$ can be interpreted as the free Boolean algebra on a set of propositional variables indexed by $X$. (In general I think it's the free complete atomic Boolean algebra on $X$.)

That's the "small" way to do it. The "big" way to do it is to work in a topos, regarded as a category of types, and think of the subobject classifier $\Omega$ as being the object corresponding to the type of propositions. Hence a proposition is a morphism $1 \to \Omega$, or equivalently a subobject of the terminal object $1$ (a subterminal object). The relationship between "small" and "big" is that the subobject classifier of a topos is an internal Heyting algebra object and so $\text{Hom}(1, \Omega)$ is a Heyting algebra (in sets).

Answer 2

What you're describing is basically the Lindenbaum order/algebra. Basically, for any theory $T$ in any logic $\mathcal{L}$ we get a partial preorder of $\mathcal{L}$-sentences with respect to $T$-provable entailment. Quotienting out by the right notion of "equivalence modulo $T$" - which is usually, but not always, just $\varphi\sim_T\psi\iff T\cup\{\varphi\}\models\psi$ and $T\cup\{\psi\}\models\varphi$ - yields a genuine partial order, and basic syntactic operations lift to algebraic operations on this partial order. For example, the Lindenbaum algebra of any first-order theory is a Boolean algebra.

• The general study of logics from such an algebraic viewpoint is, unsurprisingly, called algebraic logic. A good starting point in my opinion (given an existing understanding of the relationship between Boolean algebras and classical propositional logic and between Heyting algebras and intuitionistic propositional logic) is Blok/Pigozzi's book Algebraizable logics - the big question of that book is "When does a logic have an 'algebraic counterpart'?," and the key idea is a deep analysis of what the right notion of "equivalence modulo $T$" is in general.

Now the above isn't really category theoretic per se since category theory really shines when we can have multiple morphisms between the same objects: the simpler order-theoretic language suffices. However, things change when we consider specific proofs rather than mere provability: we can whip up categories whose objects are sentences and where a morphism $A\rightarrow B$ is a proof of the sentence $A\implies B$, with "proof composition" given via a fixed method of combining conditional proofs (e.g. maybe we have a single rule in our system which lets us do this). We may alternatively want to look at proofs "up to equivalence" in some sense, although it's not at all clear when two proofs are the same. There's a fair amount of material here, although I'm not familiar with it myself; the discussion here seems like it might be a good starting point.