Paper: Proof-theoretic harmony and structural assumptions

For a while now I've been working on a paper which deals with a core issue in proof-theoretic semantics, namely the role of harmony. (If you don't know what proof-theoretic semantics and harmony is, then here's your chance to find out.) In particular, I've been interested in the relationship between harmony---a concept conceived prior to the substrucural revolution in logic---and discharge policies in natural deduction and structural rules in sequent calculus.

I've just given the paper here in St Andrews and got some real good feedback. An earlier version of the paper (way earlier) was given in May at the Workshop for proof-theoretic semantics. Next stop is the he First Cambridge Graduate Conference in the Philosophy of Logic and Mathematics, in January, so any comments before that will be greatly appreciated. Please keep in mind, this is still work in progress.

Inferentialism about logic is the thesis that the meaning of a logical constant is fully determined by the inferential rules that govern its use. Proof-theoretic harmony is a functional constraint on inferential rules designed to rule out tonk and other ill-behaved logical constants. The paper argues that the best account of harmony, so-called General-Elimination harmony, is insensitive to crucial structural assumptions about our logical constants, for example structural rules in sequent calculus and discharge policies in natural deduction. It is argued that since these structural assumptions ought to affect the meaning of logical constants, there is a semantic lacuna in the inferentialist programme.