Harmony in Proof-Theoretic Semantics: A Reductive Analysis

Abstract

We distinguish between the foundational analysis of logical constants, which treats all connectives in a single general framework, and the reductive analysis, which studies general connectives in terms of the standard operators. With every list of introduction or elimination rules proposed for an n -ary connective c, we associate a certain formula of second-order intuitionistic propositional logic. The formula corresponding to given introduction rules expresses the introduction meaning, the formula corresponding to given elimination rules the elimination meaning of c. We say that introduction and elimination rules for c are in harmony with each other when introduction meaning and elimination meaning match. Introduction or elimination rules are called flat, if they can discharge only formulas, but not rules as assumptions. We can show that not every connective with flat introduction rules has harmonious flat elimination rules, and conversely, that not every connective with flat elimination rules has harmonious flat introduction rules. If a harmonious characterisation of a connective is given, it can be explicitly defined in terms of the standard operators for implication, conjunction, disjunction, falsum and (propositional) universal quantification, namely by its introduction meaning or (equivalently) by its elimination meaning. It is argued that the reductive analysis of logical constants implicitly underlies Prawitz’s (1979) proposal for a general schema for introduction and elimination rules.