The concept of general-elimination rules, and general-elimination harmony, is inspired by Gerhard Gentzen‘s famous remark: «The introductions represent, as it were, the ‘definitions’ of the symbols concerned, and the eliminations are no more, in the final analysis, than the consequences of these definitions.» He was alluding to the introduction- (I-) and elimination- (E-)rules of his natural deduction calculi. Logical inferentialism claims that the meaning of the logical constants is given by the rules for their use, and proof-theoretical harmony requires that the grounds for assertion (the I-rules) be «consonant» with the inferences drawn (by the E-rules) from that assertion. Gentzen continued: «It should be possible to display the E-inferences as unique functions of their corresponding I-inferences.» The purpose behind general-elimination rules is to exhibit this functional dependency by casting all the E-rules on the model of the familiar v-rule for disjunction, i.e., proof by cases. What vE encapsulates is the idea that whatever follows both from A and from B must follow from AvB. More generally, whatever follows from the grounds for assertion of some formula must follow from that formula itself. The aim of the tutorial is to explain these concepts in a clear manner and show how effective the method is in defining meaning proof-theoretically.
Session 2: Semantic Pollution and Syntactic Purity
It has been claimed that certain proof-theoretical systems are semantically polluted and suffer from an untoward intrusion of semantics into syntax, most particularly in the case of labelled deductive systems for modal logic. The charge is shown to be mistaken. It is argued on inferentialist grounds that labelled deductive systems are as syntactically pure as any formal system in which the rules define the meanings of the logical constants.