## Question regarding relationship of propositional logic to category theory

I am by no means deeply educated in regards to category theory, but I wanted to see if my thinking is on the right track.

Can I construct a category consisting of propositions as its objects and inference rules as structure preserving morphisms between these objects? Does this category in some way offer an operational semantics for a top level predication that asserts this complex of propositions?

## Comment viewing options

### I don't understand what your

I don't understand what your question about "operational semantics for a top level predication" means, but I can tell you something about the interpretation of propositional logic in category theory.

Basically, the relationship between category theory and intuitionistic propositional logic is very nearly perfect, and it's one of the jewels of categorical logic. If you are of a mathematical bent, it will fill your heart with delight.

You can construct a category in which the propositions of IPL are the objects, and the arrows are the proofs witnessing the entailments between them. Conjunction corresponds to products, implication to the exponential, and disjunction corresponds to coproducts, the terminal object corresponds to truth, and the initial object corresponds to falsity. The universal properties of these limits correspond to the inference rules, composition corresponds to modus ponens/cut, and all proofs are identified up to beta-eta equality, so the fact there are multiple arrows corresponds to the multiple possible proofs between two propositions.

Google Cartesian closed categories for more details.