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

  • 7
    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
  • 5
    @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.

Henning Makholm adds, in a comment,

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

  • 1
    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

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.