Saturday, April 26, 2008

Logical and structural

One of the key components of display logic is the distinction between structural connectives and logical connectives. It is an important distinction, but I don't think I have a good way of describing it. This makes me uncomfortable.

The structural connectives are connectives which take the place of structural rules. The display property, isolating a certain structural part in a way based on its polarity, only needs structural rules. In isolating the structural part, the polarity is preserved by the structural rules. The logical connectives have left- and right-introduction rules that involve no structure on that side. Different versions of a single connective, say →, have the same intro rules modulo differences in structure.

What are the differences between the two sorts of connective? The structural connectives are usually overloaded while the logical connectives are not. That is to say that a structural connective like º will behave differently depending on the context. It will act conjunctively when in an antecedent context but disjunctively when in a succedent one. Logical connectives will not change their behavior depending on context. Although, Restall claims (there wasn't a proof in of this in the article I read but it seems straightforward) that one can provide disambiguated structural connectives that are not overloaded and so do not change depending on context. This involves creating two versions of the structural connective, one for antecedent contexts and one for succedent ones. Overloading won't let us distinguish the two then.

Sometimes the logical connectives mimic structure, to use Restall's phrase. An example of this is conjunction mimicking º in antecedent context. This notion of mimicking can be made more precise, as Restall does in his "Display Logic and Gaggle Theory." The basic idea is that a logical connective f mimics a structural connective s iff two sorts of rules are admissible ('A' denotes formulae, 'X' structures): the rule, from X ⇒ s(A1,...,An) to X ⇒ f(A1,...,An), and the rule, from proofs of Xi ⇒ Ai (or Ai ⇒ Xi, depending on the polarities of the connectives involved) for 1≤i≤n to f(A1,...,An) ⇒ s(A1,...,An). Some logical connectives don't mimic structure. For example, [] may not, depending on the conditions placed on it.

Formulae contain only atomic formulae and logical connectives, whereas as structures are built out of formulae and structural connectives. Cut can be used only on formulae, not structures.

This gives a bit of a feel for the difference between the two, but it doesn't seem like a succinct enough explanation. They have different inductive definitions, one that builds things up using structural connectives and one that builds things up using logical connectives. But, given that some of the logical connectives mimic the structural connectives, this doesn't seem like the best route for explaining their difference. Maybe what I am after is a more philosophical explanation of the difference. Are the structural connectives logical in a way that makes them of the same kind as the more standardly logical connectives? Are º and classical conjunction members of the same kind of philosophically important kind?

4 comments:

Greg Restall said...

If I were you, I'd ask Nuel. I'd be interested in what he has to say about philosophically salient difference between connectives and punctuation (structure).

When I think about it, I can see a philosophically salient difference in the case of Gentzen's sequent calculus. The structure here is the punctuation mark of the comma, which on the left parallels conjunction and on the right parallels disjunction. But that doesn't explain the type difference -- the way one can nest connectives inside punctuation but not vice versa. What I like in thinking about this case is the way we can think of the sequent XY as saying something about the statements in X (asserted) combined with the statements in Y (denied). The comma is clearly doing the same kinds of things in both cases (combining) but doing it differently. A combination of assertions has the same sort of effect as the assertion of the conjunction. A combination of denials has the same sort of effect as the denial of the (inclusive) disjunction. This explains the type nesting -- it's the difference between contents (things that can be asserted or denied) and the kinds of ways of combining acts (assertion and denial) with those contents.

It doesn't tell us, however, the negation structural operator * -- is there a way of conceiving a way of modifying the act of assertion to make it a denial (and vice versa)? Perhaps there is. But I've not seen a way to clearly articulate it.

Ole Thomassen Hjortland said...

Very interesting stuff, Shawn. I think some of the terminology here was very helpful. Some thoughts:

"That is to say that a structural connective like ยบ will behave differently depending on the context. It will act conjunctively when in an antecedent context but disjunctively when in a succedent one. Logical connectives will not change their behavior depending on context."

Not sure what you mean with the last sentence? Of course, there is a sense in which they do behave differently, in an antecedent context they have left-rules, in a succedent context right-rules. Only some story (like harmony) about the relationship between right- and left-rules will ensure that we are in fact dealing with one (well-defined) logical constant.

Regarding Greg's comment, I think there is some interesting stuff in the literature. Greg's own 'Multiple Conclusion', but also Smiley and Rumfitt on assertion and denial (see Smiley 1996, Rumfitt 1997, 2000). There is an interesting idea of adding signed formulae which indicate the force of the proposition (i.e., whether it is assertoric or rejective). There is a sense in which the denial operator works like a structural negation.

I've been working with these papers quite a lot lately, but with what Smiley calls the categoricity problem. I don't know if you've already looked into it, but let me know what you think.

Shawn said...

Greg,
I am going to talk to Nuel about it soon.

I like your way of formulating what is happening with the comma. It seems like the comma is combining differently in a way that & is not.

Ole,
I think I saw your comments right after I got to Japan and didn't have time to respond. Sorry for the delay.

I didn't realize that the last sentence of the quoted paragraph was as confusing as it is. I was thinking that logical connectives do not depend on whether the context is antecedent or succedent in a way that structural connectives do. As you point out, there is a problem with this in that we have different intro rules depending on whether we have an antecedent or succedent context. (I was understanding your point about the different intro rules as a challenge to the claim that logical connectives are context-independent.) I'm using antecedent/succedent here instead of left/right since in display logic we can always isolate the formula on the left or the right, i.e. isolate it as an antecedent/succedent formula. The two results, cut and identity, that I indicated are ones that Belnap takes to indicate sameness of meaning or harmony. This needs to be spelled out some more though.

To return to the point I started with, how do logical connectives not depend on context? I want to appeal to elimination rules, but we don't have those in a sequent calculus. I'm not sure what to say. If my hunch turns out to be wrong that logical connectives are context-independent, then it will be more obscure to me what the distinction is between logical and structural connectives. Although, Greg's explanation above for the comma gets at the idea I wanted to articulate.

I have not looked at the papers by Smiley and Rumfitt. I will try to check them out. Do you happen to have titles for those papers?

Ole Thomassen Hjortland said...

Hi Shawn,
Thanks for the reply. Hope you had a great time in Japan.

Smiley's paper is 'Rejection' (Analysis). Rumfitt's are 'The Categoricity Problem and Truth value gaps' (Analysis) and ''Yes' and 'No'' (Mind).