Like I said, the Pitt-CMU conference has come and gone. I said before that if my comments on Ole’s paper went over well, I’d put them up here. The comments seem to have gone well, so I’m going to put them up. The comments won’t make much sense without having read the paper, which is on proof-theoretic harmony. 

1. First, a short summary of the paper.
Our initial problem was how to take inferential rules as conferring meaning while avoiding TONK and its ilk, and this was to be done through the notion of harmony. A promising candidate was the natural deduction GE-harmony strategy, but this cannot be the whole story semantically as it looks like one gets different meanings for the logical constants when there are different structural rules. This led us to a sequent calculus strategy, MIN, which takes meaning to be conferred by a proper subset of the rules. The version looked at distinguished the operational meaning, specified by the operational rules, from the global meaning, specified by the set of provable sequents. This runs into two problems: violating constraints set by the inferentialist project and demarcating structural rules. The conclusion is that unless MIN can be patched with a clarification of structural rules or GE-harmony made viable in some other way that gets around the problems with the structural rules then harmony can’t be the complete semantic story for the inferentialist.

2. If we look back at the general thesis of inferentialism, it says that the meaning of logical constants is fully determined by the inferential rules governing their use. If we start by looking at natural deduction, then the first move, as Ole points out, will be to take the the intro- and elim-rules as being those rules. If we follow Dummett, Prawitz, Milne, and Read in this, then it is easy to miss the point that Ole brings to our attention.

If we then shift to sequent calculus, it is natural to look at the corresponding rules, the left and right intro-rules, or the operational rules. In sequent calculus new rules appear, namely the structural rules. These seem to go missing in the natural deduction setting. Really, they are there, but they are implicit, or more implicit, in the discharge policies than in the sequent calculus’s structural rules. They are implicit in the sense that they do not even appear in a propositional form in natural deduction reasoning. Structural rules are more explicit, in the sense that they are at least an instance of a rule. They are not fully explicit since there is no single proposition or even sequent expressing the acceptance of the structural rule. With this in mind, we might want to push a point that Ole brings up at the end of his paper. He mentions that there are systems formulated in terms of hypersequents, systems where derivations are performed on finite multisets of sequents. These allow the formulation of more structural rules. Other systems, like display logic, bring out structure by including structural operators. These are ways of making structural rules explicit that would otherwise be left implicit in how the derivations are carried out. It is possible that in order to make progress on INF, a shift must be made to using these systems in order to get enough structural rules in view to make the necessary distinctions. Another possibility is that there is a need for a formalism that allows us to reason explicitly about structural rules. At the end of the paper, we’re left with a negative conclusion, so I’m curious if Ole has any view about positive morals to draw.

3. Switching gears slightly, the problem with structural assumptions arises when we are dealing with rules that are hypothetical, or discharge assumptions. In standard approaches, this is usually limited to the vee elim-rule or the arrow intro-rule. However, in an effort to make the rules more uniform and general, the GE-approach makes all the rules hypothetical. In the sequent calculus systems, the structural rules are already present, so the problem arises there immediately.
In order to get around this problem, Paoli distinguishes two kinds of meaning for logical constants. There is the operational meaning, which is fully determined by the operational rules, and there are two kinds of global meaning, which are determined by the full set of rules for the system. This minimalism about the meaning picks out a subset of the rules as meaning conferring and claims that only those contribute to meaning while the other rules merely play a role in the logic.

There is then a question of whether one can distinguish the operational and structural rules in terms of use. As Ole points out the prospects of finding a difference in everyday reasoning practices that reflects things like structural rules or discharge policies seems slim. This brings up the question to what extent logic reflects, or should reflect, our practices of reasoning. If we are looking for a difference in use that appears in non-formalized contexts, the prospects are slim. If that is our goal, then there is a question of whether things like the intro and elim rules can viably be maintained if reflecting actual reasoning is our goal. Gilbert Harman thinks not. Others like Prawitz, I think, believe so. If, instead of a difference in everyday inferential practice, we are looking for a difference that comes out in the formalization, prospects are maybe a little better. Which of these was meant will determine how the MIN proponent will proceed. An INF proponent will not want too much space to open up between the two options.

4. The paper closes with a problem for MIN that leads to a general question. What is a structural rule? To put the question another way, what is the role in reasoning of the structural rules? The paper closes by looking at this in the case of intermediate logics. These logics are formulated in terms of hypersequents, so their operational rules are, strictly speaking, different from those of classical logic, which is formulated purely in terms of normal sequents. If one wants to defend MIN, one wants to chalk this difference up to structural assumptions, not a real semantic difference in operational rules. The worry is that any difference in derivational power can be assigned to structural assumptions in order to save sameness of operational meaning. I take it that the shift to derivational power is because we have sameness of operational meaning but difference in global meaning between the logics. It is a little unclear to me where exactly the problem lies. The worry might be that our idea of structural rules might be shaky because formulations of operational rules may build in structural assumptions. (Like some sequent formulations of classical logic.) Or, it might be that different formalisms cover different sorts of structure, e.g. sequents reveal some, hypersequents reveal more, and we can’t tell in advance what is hidden. Or are there just no sharp definitions? (Rules that do not contain any logical constants essentially, perhaps?)

[The next two paragraphs are rougher ideas which weren’t presented] To put the question another way, what is the role in reasoning of the structural rules? Here’s an idea, taken from Belnap, sort of. One might think that the structural rules provide the context of deducibility. Of course, the question about meaning in different contexts of deducibility still comes up and this may be what Paoli’s distinction between operational and global meaning trades on. But, if we are willing to adjust the context suitably, there are even non-trivial systems that have TONK as a connective. Harmony might be a notion that depends on the context of deducibility in a bigger way than expected. When there are fewer structural rules in play, it would be easier for rules to be harmonious.

One question that comes up is how far one can push the MIN move of attributing differences in derivational power to structural rules. Could we, for example, maintain that all conditionals are, really, operationally, at base some minimal conditional, with just that minimal meaning, which is obscured by the semantically insignificant structural assumptions? Suppose I am a fan of the Lambek calculus with its left and right conditionals, which collapse into a single one in the presence of some structural rules. Does it make sense to maintain that all of those classical conditionals are really either the left or the right Lambek conditional, just obscured by structure?

5. To close, a question: The thing that causes problems for the harmony as reduction account is a violation of the side conditions on modal formulae. Is there a connection between side conditions and the discharge policies or structural assumptions? Or, is this possibly a different problem, one that introduces a new sort of restraint that may depend on non-inferential properties.