That Logic Blog

September 28, 2005


The conference schedule has turned out to be rather full, so I haven't had time to blog details (as you may have noticed). I've decided to make some posts at the end of the conference covering mainly the stuff that I understood the best. This will probably be some time next week. There have been some nice talks on algebra, proof theory and nonclassical logic so far, with more to come. One rather curious question was raised: Does anybody in Australia do classical logic? I couldn't think of anybody...

September 24, 2005

Substructurally Yours

There has been a lot of interesting work on substructural logics coming out of Japan for a while now. The class of logics which has received the most attention are the so-called FL logics. FL stands for Full Lambek Calculus and is what you get if you drop the structural rules of weakening, exchange and contraction from intuitionistic logic. If you prefer other terminology, this is the same as noncommutative multiplicative additive linear logic.

What makes FL particularly nice is that it has a perspicuous algebraic semantics given by residuated lattices. Briefly, a residuated lattice is a set that carries both a monoid and a lattice structure such that the monoid has both right and left residuals. These may be seen as left and right division operators and satisfy the properties that x.y &le z iff x &le z/y iff y &le x\z. Categorically, this corresponds to saying that we have a biclosed monoidal category with both finite sums and finite products. A residuated lattice is the special case where the category is a poset.

Given FL as a base, we can build up other substructural logics by adding structural rules. These may be the standard weakening, contraction and exchange rules or more exotic rules with cute names like mingle and expansion.

So, what counts as a structural rule? And in what way does the property of an extension of FL rely on the structure of the additional structural rules? These questions and much more are answered in the following paper:

Which Structural Rules Admit Cut Elimination? - An Algebraic Criterion. Kazushige Terui

This paper is chock full of interesting stuff, so I will only sketch bits of it. In order to keep you reading, I'll state one of the main results in grandiose wording. Every substructural logic over FL has cut elimination! Wowzer!

Let's try make this a bit more precise. First, an example. Say we take FL and add contraction but not exchange. Then, the resulting calculus is quite easily seen to not have cut elimination. So the grandiose statement needs some refinement. Specifically, if we identify a logic with its set of provable formulae/sequents, then the result says that any such logic over FL can be given a cut free sequent calculus. Still cool.

How does this all work? It pushes through in a way that is very familiar from exotic structural proof theory, such as the calculus of structures. First, say that a structural rule satisfies the syntactic propagation property if it propagates from atomic formulae to all formulae. In other words, all instances of the rule can be reduced to atomic instances.

Returning to our example of FL with contraction but no exchange, let's extend contraction to act on arbitrary sequences of formulae. Then, this modified version satisfies the syntactic propagation property, while the version with standard exchange does not. We may be onto something here!

As it so happens, Terui shows that every extension of FL having cut elimination satisfies the syntactic propagation property on all of its structural rules. What about the converse? It turns out that this is true also, but in order to prove it, Terui introduces a semantic propagation property. This property is stated in terms of, you guessed it, fancy sorts of residuated lattices.

So, a structural extension of FL has cut elimination iff it satisfies the syntactic propagation property iff it satisfies the semantic propagation property. Our tweaked version of FL with contraction satisfies syntactic propagation, so has cut elimination. This is a special case of a more general phenomenon. Given any collection of structural rules, we can complete them (in the Knuth-Bendix sense) to another set of structural rules that results in cut elimination. Moreover, this completion preserves provability. Now that is super cool!

Anyway, I'll stop there and point you to the paper for lots more juicy details!

On a side note, I am in Perth now for the Australasian Association of Logic annual conference, as well as the Australian Mathematical Society annual conference (since the movie was boring, I read the above paper and wrote this post on the plane flight over). The latter has streams in logic and algebra, which I will generally be hanging around. I'll even be giving talks in each conference (the things they let me get away with!). I'll be blogging details as the conferences progress. Whether this will be liveblogging depends on whether I can leech some wireless. Otherwise, I'll try to do daily posts.

September 13, 2005

Axis Roundup

I'm back in Canberra now and, as promised, here is a roundup of the weekend Logic Axis meeting. The amount of detail varies for different talks, mainly based on how tired I was (I had just spent 12 hours on a bus, arriving only an hour or so before the workshop began) and the level of my ignorance of the area... First, Saturday!

Koji Tanaka: Logical Pluralism, Non-Euclidean Geometry and Kant's a Priori. The basic goal was to understand precisely what claim Beall and Restall are making about logical pluralism. The thrust of the talk is that B+R do not have a proper notion of what a "logic" is and so, while there is no objection to there being different a priori accounts of validity, it is not clear how this leads to different logics. One strange feature that came up is that B+R seem to be monist when it comes to metaphysical necessity. If that is the case, argue Goddu and Wyatt, then one must wonder what makes classical logic so different that we ought to be pluralists in this case. Question time for this talk cleared up some things for me. It was pointed out that a pluralist attitude with respect to pure logics is perfectly reasonable, with little to object over. So, the case of applied logics is where the meat is. That is, when we want our logic to capture a certain notion such as, say, metaphysical necessity. If this is the case, then it is not clear that B+R have clearly delineated pure and applied logic, given their stance on metaphysical necessity.

Allen Hazen: Theories of Sets, Theories of Numbers. The thrust here was to seek out the correct restrictions of axiomatic set theory that capture various weak theories of arithmetic. That is, such that each theory can interpret the other. The focus was on Robisnson Arithmetic (Q) and accounts of weak set theories due to Tarski and Lewis, repsecitvely, were analysed with respect to Q.

Thomas Forster: Delinearising Ehrenfeucht-Mostowski. The kick off point is a theorem of Ehrenfeucht-Mostowski, which says that if T is a theory with infinite models, then for any total order I, there is some model of T in which I embeds as a set of indescernables (SOI). A SOI is basically a collection of variables such that the logic cannot descide between them. That is, if one has a property, then they all have that property. Notice the amount that my arms are waving here! Anyway, Thomas made the point that there does not seem to be a good reason why this result should rely on embedding a total order. What about other orders? After sketching how to do this for circular orders, we went on to see how to generalise to arbitrary structures. The thorny part of stating the definition seems to be the bit I waved my arms over above - defining what it means to be a set of indiscernables. This is easy enough in the total order case, but a lot more care needs to be taken in the general setting.

Ed Coleman: Argumentum ad Nauseum. This was an extended discussion of logical fallacies of the "ad whatnot" kind. It was pointed out that there is no good collection of possible logical fallacies out there and, those that are in existence, are inconsistent even in what the various fallacies mean. It was proposed that one ought to create the "Book of Objections", which contains a good theory of fallacies and outlines all possible fallacies. Of course, it is not clear that such a book would be finite in length...

Graham Priest: The Language of Dialetheism 1: Dialetheism, Language and the World. I found this talk vary useful, since it went quite some way to making clear to me what dialetheism is actually all about. Dialetheism is the belief that there can be true contradications. It was pointed out that there are two possible flavours of contradiction: contradictions in language and contradictions in the world. Contradictions in language tend to play on word level ambiguity. As such, it is not overly clear to me that there can be something of a proper linguistic dialethea, which does not rely on the underlying ambiguity. The world level dialetheism is slightly more reasonable. As far as I understand it, an example would be that of moving bodies, since they are in motion and yet, at any given instant of time, they are at rest. Personally, I feel that this is just another case of ambiguity, since motion is usually taken to mean changes/movement through time.

After all that, it was time for wine, dinner and a merry old time before gathering back on Sunday. What happened on Sunday? Read on to find out...

Kieren Nanasi: Mathematical Objects and the Makes-No-Difference Argument. The makes-no-difference argument goes something like this. Pretend that you are at least a little bit of a platonist, for the moment. Suppose now that all mathematical objects suddenly blinked out of existence. Since mathematical objects are a-causal, their disappearing would make no difference to the physical world. As a resultm an ontology in which they feature would be untenable. Therefore, even if mathematical objects did exist, an ontology in which they feature would be untenable. Now thinking about objects suddenly blinking out of existence is incoherent. So, it seems reasonable to weaken the argument to saying that if there were no mathematical objects, then this would make no difference to the physical world. We were taken through several more refinements of the argument, ending with a version which only applies to abstract mathematical objects. Whatever those are...

Demetrios Bastiras: Politis on Aristotle and the Law of Non Contradiction. My ignorence is at its highest here, since I am not very familiar with Aristotle's writings. We were introduced to some writings of Politis, wherein he analyses Aristotle's stance on the law of non contradiction. Aristotle believed that if we accept that some contradictions are true, then we must accept that all contradictions are true. Politis disagreed with this entailment which, I guess, would make him an Australian philosopher! Politis further argued that metaphysics is prior to logic and must be analysed in this light. I guess that this is reasonble for philosophical logic, where it seems that logic is used mainly as a tool for trying to analyse metaphysical arguments. Well, that's my impression anyway.

Peter Quigley: Structure and inconsistency. Quite hard for me to give a summary of this talk, since it mainly consisted of analysing various animations of rotating objects, wherein an inconsistency was added. The thrust of the talk was seeing how these inconsistencies affect our perceptions. It certainly worked, most of the audience was quite disturbed as their perceptions of what was going on flipped between alternative views as the objects rotated!
Edit:Peter's animations can be found here.

Chris Mortensen: Analysis of inconsistent and incomplete Necker Cubes. More geometric inconsistencies here, though this talk covered a classification of possible inconsistencies. At the first level are inconsistencies taht arise in the two dimensional case. That is, ambiguities that arise by virtue of the projection of an object onto the plane. At the second level are inconstencies that arise in three dimensions where we only look at the vertices and edges of the object in question (that is, at the edges). Finally, the third level of inconsistency is again at the three dimensional level but this time we look at the faces of the object in question.

Jon Cohen: Notions of Proof Equivalence. Hey, that's me! I spoke about the problem of analysing ambiguity in natural language. There are two levels of ambiguity here. In the first instance is word level ambiguity, which is not terribly interesting. The second case is structural ambiguity, where the meanings of the words are fixed, but the ambiguity arises due to vagueness as to the scope of words. This type of ambiguity is a lot more interesting. Working under the assumption that language is compositional, structural ambiguity must arise due to different possible ways of composing the meaning of a sentence together. I used this as a jumping off point to give an introduction to the category theory approach to logic, framed in terms of gadgets arising in quantum gravity. One thing that comes out of this is that it is actually possible to account for some phenomena that are usually taken to be semantic using syntactic constructs. I need to think about this aspect a bit more, since it seems to say that the syntax/semantics distinction is even more blurry than commonly assumed. If you're a sucker for technical details, I squibbed up a broad overview over here.

Ross Brady: Classical Deduction and Relevant Deduction. The basic plot was to analyse Fitch-style natural deduction from the point of view that each step of the deduction should be "relevant" in some sense. I was quite tired by this stage, so did not follow along very well. From where I was sitting, it looked like Ross was talking about the sorts of concerns that those people doing "deep inference" proof theory care about. I'll have to chat with him at the AAL!

That's it for the workshop. It's a bit of a shame that Ross and I are the only attendees of the workshop that will also be going to the AAL. It just shows up how fragmented the australian logic community is, which is a pity.

September 06, 2005

Travel Time

I'm off to Sydney tomorrow to visit the Centre of Australian Category Theory. I'll be speaking in The Australian Category Seminar about categorical and algebraic logic as well as giving a department seminar. I'm looking forward to finding out a bit more about their research activities, since they have a very impressive number of experts!

After that, I'll be going to Melbourne for the weekend, home of logic blogger Greg Restall. I suspect that he may not be there. Over the weekend is a rather intense philosophical logic workshop, with very many interesting looking talks. My little talk will be on proof equivalence (what else?). While there, I'll also see a bit about dialetheism, relations between Kant's a priori and logical pluralism, relations between relevant and classical deduction and much much more. Should be fun.

Oh yes, thanks to Kenny for telling me about the Melbourne workshop and putting me in contact with Graham Priest.

I'm not sure if I'll have any internet access while I am away. I'll take lots of notes though and post details of the workshop when I get back.