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.

Screenshot of BananaCats


2 Answers 2


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

  • $\begingroup$ I like the big way since I'm 2-3 chapters into Goldblatt's Topoi. However, how does one "work in a topos" in regards to programming an actual proof assistant. For example, is the topos a drop-down menu setting, etc. I would like most of the logic of my proof assistant to be written in the language of categories itself (using diagrams). That is opposed to the instead having to code every piece of math known to man approach. Should I just stick to the topos Set for now, and then expand to other topoi later? Also, since I have blocks in my visual language these blocks can contain sub-blocks $\endgroup$ Oct 1, 2020 at 0:59
  • $\begingroup$ which could be considered elements of a type or a set. In that way, not everything one does has to be topoized (or turned into an all-arrows-approach). $\endgroup$ Oct 1, 2020 at 1:02
  • 1
    $\begingroup$ @AlgebraicGeometryStudent: that I don't know. Maybe look at how the Prop type is handled in existing proof assistants such as Lean: leanprover.github.io/theorem_proving_in_lean/… $\endgroup$ Oct 1, 2020 at 1:02
  • $\begingroup$ Thanks, I'm going to read all the links before I check an answer here. This is a deep subject, but I can't get too deep into it myself and neglect to code something, but why code something the same way that has already been done, etc. What I'm really after is a proof assistant that talks to the user in plain mathematical language, and that exhibits CD's wherever it can, because these are beautiful condensations of math content. One can easily recall a 3x3 commutative diagram (CD) grid but rarely will they care to recall all the possible equalities encoded in that grid in a textual format. $\endgroup$ Oct 1, 2020 at 1:12
  • 2
    $\begingroup$ @AlgebraicGeometry: $\Rightarrow$ here denotes the exponential object, as I mentioned above. It can happen that the exponential object $a \Rightarrow b$ exists even though there are no morphisms $a \to b$; this just means that the set of points $\text{Hom}(1, a \Rightarrow b) \cong \text{Hom}(a, b)$ is empty. In the smallest case of the Boolean algebra $B = \{ \top, \bot \}$ regarded as a Heyting algebra $\Rightarrow$ is exactly what you'd expect from propositional logic, e.g. $(\top \Rightarrow \top) = \top$ and so forth. $\endgroup$ Oct 1, 2020 at 1:46

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.

  • $\begingroup$ There's a lot involved in "whipping up" something like that :) I honestly am not a student of logic, so anything I do I'd like it to be at the level that we are discussing math right this moment on MSE. "Let $G$ be a group." etc. The user should not have to learn an entire programming language to be proficient in the upcoming world of computerized maths. I've looked into Coq and although it is logically sound and complete and you can do research with it, it's incredibly incompatible with the way we talk about math to each other, say on MSE. $\endgroup$ Oct 1, 2020 at 1:16
  • $\begingroup$ I like the idea that the idea of a proof is open ended. Think about all the visual geometric proofs you can google. There is no practical way to tie those into a proof system other than a community of users voting yes/no that the proof is complete. Therefore, it's hard for me to consider specific proofs as arrows at the moment. A proof will be a collection of user-drawn diagrams that are partially generated by diagram transformation rules (say). Then there are some rules in there such that when the proof is complete, an arrow between the respective propositions $A$ and $B$ can b drawn $\endgroup$ Oct 1, 2020 at 1:21
  • 1
    $\begingroup$ Well, if you talk about specific proofs then this is essentially just a category of functions, via Curry-Howard. $\endgroup$ Oct 1, 2020 at 11:15

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .