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.
Best Answer
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
then the categories you get this way are precisely the bounded lattices. If you further require that
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).