Home » forums » LtU Forum

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?

By Nathan Sobo at 2007-07-06 21:14 | LtU Forum | previous forum topic | next forum topic | other blogs | 5721 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

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.

By neelk at Fri, 2007-07-06 21:42 | login or register to post comments

I accidentally replied to

I accidentally replied to the thread instead of to you. I think my reply is a sibling to your comment.

By Nathan Sobo at Fri, 2007-07-06 22:24 | login or register to post comments

Awesome! Thanks!

Very cool. You have confirmed my intuition after reading about categories for the first time, though I have a bit more reading to do before I fully understand products, exponential, etc. What do you think of the notion of modeling the content of a linguistic expression as a category containing propositions and arrows between them. One proposition in the category could be that which asserts the presence of a linguistic sign, and arrows could map that proposition to its model theoretic consequences?

What I was trying to say about operational semantics was basically that the arrows served as a map for proving propositions in the category to other propositions, so they sort of represent the execution of a theorem prover grounding a given proposition in other propositions declared a priori true. Your reply makes me more confident that this is a reasonable characterization, but maybe you can speak to this notion.

By Nathan Sobo at Fri, 2007-07-06 22:22 | login or register to post comments