« Low-Res Bloggers At Dinner | Main | Adventures in Flatland »
July 25, 2005
Tea with Lloyd and Su
I went along to the philosophy department at Monash yesterday to hang out with logicians Su Rogerson and Lloyd Humberstone. They have been teaching a rather advanced logic course to a small group of brave undergraduates, and so I got to see them in action before tea.



Here's just one of the things that I learned from Su and Lloyd yesterday:
Some famous Axioms

The system which takes B, C and I as axioms (with uniform substitution and modus ponens as the rules) is known as BCI. BCI is the implicational fragment of Linear Logic. If we add contraction (W) we get BCIW, which is the implicational fragment of the best known relevant logic, R. Adding K (known to relevant logicians as "irrelevance"(!)) instead of W gets us BCK (I follows from K and C.) BCK (under that name, at least) was first studied by Meredith. If we add both K and W we get BCKW, the implicational fragment of intuitionistic logic. To get the implicational fragment of classical logic we need only add Peirce's Law:

So what we have looks like this:

All these axioms possess a confusing multitude of names, so I should mention that B is also known as "prefixing" and C gets called "permutation."
Posted by logican at July 25, 2005 08:42 PM
Trackback Pings
The trackback address for this entry is:
http://www.logicandlanguage.net/trakbak.cgi/91
Comments
Sigh, reading your blog makes me miss academics, but then again, I like what I'm doing now a lot. Either way, keep blogging, it's a great read.
Posted by: Adriaan at July 26, 2005 02:51 AM
When I was TAing intermediate logic this past semester, I noticed that there was an analogy between the propositional rules beginning with "p->" and predicate rules beginning with a universal quantifier. Using a box instead of a quantifier, we see that the axiom B above is analogous to the axiom K of modal logic, the one called K is analogous to necessitation, and the one called W is analogous to the axiom 4 of S4.
I don't know if all this means anything, or if anyone has explored this analogy in much greater detail and explained why it happens.
Posted by: Kenny Easwaran at July 26, 2005 10:04 AM
You mean like this, for the necessitation case?
|- q => |- p-> q
|- Fx => |- VxFx
|- q => |-[]q
Sorry to be dumb, Kenny, but I don't see the analogy in the W/S4 case. Wouldn't the translation of W (putting Boxes for 'P->'s) be the converse of the S4 axiom? From
W: (p->(p->q))->(p->q)
we get:
[][]q->[]q
rather than:
4: []q->[][]q
And doing the same thing to B we get something which isn't even a theorem in S5. Did you mean something different?
Posted by: Gillian Russell at July 26, 2005 09:20 PM
I'm not sure that the analogy holds at this level. Certainly, there is an analogy between the K rule and distribution. A quick note on this is available here. The discussion there has a lot of technical mumbo jumbo, but the analogy should be clear, if not the motivation.
Kenny's example for 4 can be fixed by using diamond instead of box.
There is a connection between the above axioms and substructural logics. For instance, BCW corresponds to dropping weakening (i.e., relevant logic) and BCK to dropping contraction. There are nice algebraic models of these, encompassing things like lattice ordered groups.
Kosta Dosen has considered embeddings of first order variants of these posessing an intuitionistic negation into S4-like extensions where the negation is classical (i.e., involutary):
"Modal translations in substructural logics" K. Dosen, Journal of Philosophical Logic 21:283--336
Posted by: Jon
at July 27, 2005 12:34 AM
In the interests of not confusing budding logicians,I think you got the wrong image, or the wrong brackets, for the amusing Peirce's Law. (Did I post this already?)
((p->q)->p)->p, not (p->q)->p->p
Posted by: andrew at July 19, 2006 12:20 AM