4
$\begingroup$

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

$\endgroup$
2
  • 8
    $\begingroup$ 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\}$. $\endgroup$
    – MJD
    Jun 10, 2015 at 19:01
  • 5
    $\begingroup$ @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$. $\endgroup$
    – hmakholm left over Monica
    Jun 10, 2015 at 19:42

1 Answer 1

Reset to default
8
$\begingroup$

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

$\endgroup$
1
  • 1
    $\begingroup$ Also, taking its underlying poset ($A\le B$ iff $\ \models (A\to B)$) gives another standard such category. $\endgroup$
    – Berci
    Jun 11, 2015 at 9:38

You must log in to answer this question.

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