Proof-theoretic harmony (Pistone-Tranchini)
The notion of harmony was introduced to described the perfect match that ought to hold between two centrale features of the practice of assertion. These are (i) the capability of speakers of recognising when the conditions for correctly asserting a proposition are satisfied; and (ii) the capability of correctly reacting to (or more generally drawing consequences from) assertions made by other speakers.
Although it seems indisputable that the conditions for asserting a proposition and the consequences that can be drawn from it cannot be determined independently of each other, little agreement has been found both on the significance and on the precise characterization of harmony.
In the setting of natural deduction, the introduction rules for the logical connectives express the conditions for correctly asserting logically complex sentences and the elimination rules are the consequences that can be drawn form these assertions. One may therefore expect that, at least for logically complex propositions, the notion of harmony could be made precise in this formal setting.
In the first part of this course, after introducing the notion of harmony and discussing various views with regards to its normativity, we will focus on the notion of harmony as it applies to logical connectives and present the traditional account of harmony as conservativity. In the second par of the course we will describe some more recent characterizations of this notion based on second-order intuitionistic propositional logic and we will illustrate the possibility of accounting for "intensional" features of harmony using the notion of identity of proofs.