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?