Title: When Rules Define Logical Operators: Rules as Second-Order Definitions
Abstract: Logical inferentialists hold that the meaning of logical operators is given by their rules of inference. Arthur Prior cast doubt on this by introducing rules for his so-called tonk operator that seemed to allow for the derivation of any sentence whatsoever from any sentence whatsoever. The obvious inferentialist reply was to require constraints on the defining rules, such as conservativeness (Belnap) or harmony (Dummett). In my talk, I will propose a different criterion for when rules define logical operators that (i) is philosophically principled in taking the idea of rules as definitions perfectly seriously, (ii) explains how the semantic meaning of the operators can be determined from their rules, (iii) is local in a similar sense as harmony is, (iv) validates the intuitionistic natural deduction rules and the intuitionistic/classical sequent calculus rules as defining the classical logical operators while ruling out Prior’s rules for tonk, (v) makes clear why already the intuitionistic natural deduction rules define the classical meaning of logical operators so long as metavariables are interpreted as expressing arbitrary classical propositions, (vi) validates the classical natural deduction rules as analytic, and (vii) does not guarantee conservativeness in Belnap’s sense but in a closely related one that still entails consistency. The basic idea will be: rules define a classical logical operator just in case they translate into an explicit definition in pure classical second-order logic.