Category theory with objects as logical expressions over $\{\vee,\wedge,\neg\}$ and morphisms as?

I am wondering if there is a standard definition for a category with objects as first order logical (FOL) expressions e.g. $\neg x \vee y$. It seems to me that these logical expressions would be part of a concrete category as they can be mapped (forgetfully) to sets, and as many concrete categories (groups etc.) have homomorphisms as morphisms that perhaps homomorphisms are the morphisms in this FOL category. I am having difficulties visualizing what these homomorphisms would look like - perhaps just some operation $(\circ,\bullet)$ such that

$f((x \wedge y) \vee z) \rightarrow (f(x) \bullet f(y)) \circ f(z)$ where $(\vee,\wedge) \rightarrow (\circ,\bullet)$ ?

Thanks,

Brian

• There is a category whose objects are logical formulae and where each morphism $A \to B$ is a proof that $A$ implies $B$. Composition is concatenation of proofs; identity morphisms are trivial (empty) proofs. You could restrict the category to only the formulae over $\{\lor, \land, \lnot\}$. – MJD Jun 10 '15 at 19:01
• @MJD: Make that an answer. If you quotient out the difference between "essentially equivalent" proofs (according to a suitable definition) you get a cartesian closed category for which there's a rich theory with strong connections to computer science. The product of objects $A$ and $B$ is the formula $A\land B$; the exponential $B^A$ is $A\to B$. – Henning Makholm Jun 10 '15 at 19:42

One can take any family of formulas and turn it into a category where each formula is an object and there is an arrow $A\to B$ when there is a proof that $A$ implies $B$. The identity arrows are trivial (empty) proofs and two proofs can be composed by concatenating them.
If you quotient out the difference between "essentially equivalent" proofs (according to a suitable definition) you get a cartesian closed category for which there's a rich theory with strong connections to computer science. The product of objects $A$ and $B$ is the formula $A∧B$; the exponential $B^A$ is $A→B$.
• Also, taking its underlying poset ($A\le B$ iff $\ \models (A\to B)$) gives another standard such category. – Berci Jun 11 '15 at 9:38