Blog troubles
I shall certainly be taking Urs' advice to change software when I have the time. At the moment, under the post 'Category theory and ontology' it shows '1 comment'. If you click on this you are shown Kea's comment, making reference to one by John Baez, which doesn't show. Here was John's comment:
David writes:
P -> Q
is implication, and see it as a quotient of some more interesting category where there can be lots of morphisms from P to Q, namely the different proofs that P implies Q.
They've worked this out in great detail in the case of intuitionistic logic, using cartesian closed categories. They've also done it for linear logic, using *-autonomous categories.
Interestingly, it's a lot harder for classical logic! For a long time it was believed that if you take a cartesian closed category and throw in relations that make it classical, it automatically collapses down to a mere poset - namely, a Boolean algebra.
But here in Marseille I've met someone who apparently succeed in getting around this problem: Peter Selinger. In his work on "control categories" (whatever the hell those are), he supposedly succeeded in finding nice categories where the morphisms are proofs in classical logic.
Both he and I will be here all throughout February, so I'm hoping I'll actually learn what this is all about. I'm also hoping he can explain linear logic to me, because I've never understood that. Part of the problem, I now realize, is that I don't have a feel for *-autonomous categories.
David writes:
I strongly suspect that category theory will prove to be the only viable language to cope with the subtle relations of sameness involved here in computer science, and also elsewhere.Lots of category-theoretic computer scientists have felt this for a long time: the way they put it, proof theory should take the poset of propositions, where the order relation
P -> Q
is implication, and see it as a quotient of some more interesting category where there can be lots of morphisms from P to Q, namely the different proofs that P implies Q.
They've worked this out in great detail in the case of intuitionistic logic, using cartesian closed categories. They've also done it for linear logic, using *-autonomous categories.
Interestingly, it's a lot harder for classical logic! For a long time it was believed that if you take a cartesian closed category and throw in relations that make it classical, it automatically collapses down to a mere poset - namely, a Boolean algebra.
But here in Marseille I've met someone who apparently succeed in getting around this problem: Peter Selinger. In his work on "control categories" (whatever the hell those are), he supposedly succeeded in finding nice categories where the morphisms are proofs in classical logic.
Both he and I will be here all throughout February, so I'm hoping I'll actually learn what this is all about. I'm also hoping he can explain linear logic to me, because I've never understood that. Part of the problem, I now realize, is that I don't have a feel for *-autonomous categories.
1 Comments:
If you are interested in categorical models of classical logic, then you should also check out Fuhrmann and Pym's Classical Categories.
Post a Comment
<< Home