In the proof-theoretic semantics approach to meaning, harmony , requiring a balance between introduction-rules (I-rules) and elimination rules (E-rules) within a meaning conferring natural-deduction proof-system, is a central notion. In this paper, we consider two notions of harmony that were proposed in the literature: 1. GE-harmony , requiring a certain form of the E-rules, given the form of the I-rules. 2. Local intrinsic harmony : imposes the existence of certain transformations of derivations, known as reduction and expansion . We propose (...) a construction of the E-rules (in GE-form) from given I-rules, and prove that the constructed rules satisfy also local intrinsic harmony. The construction is based on a classification of I-rules, and constitute an implementation to Gentzen’s (and Pawitz’) remark, that E-rules can be “read off” I-rules. (shrink)

The idea of an ?inversion principle?, and the name itself, originated in the work of Paul Lorenzen in the 1950s, as a method to generate new admissible rules within a certain syntactic context. Some fifteen years later, the idea was taken up by Dag Prawitz to devise a strategy of normalization for natural deduction calculi (this being an analogue of Gentzen's cut-elimination theorem for sequent calculi). Later, Prawitz used the inversion principle again, attributing it with a semantic role. Still working (...) in natural deduction calculi, he formulated a general type of schematic introduction rules to be matched ? thanks to the idea supporting the inversion principle ? by a corresponding general schematic Elimination rule. This was an attempt to provide a solution to the problem suggested by the often quoted note of Gentzen. According to Gentzen ?it should be possible to display the elimination rules as unique functions of the corresponding introduction rules on the basis of certain requirements?. Many people have since worked on this topic, which can be appropriately seen as the birthplace of what are now referred to as ?general elimination rules?, recently studied thoroughly by Sara Negri and Jan von Plato. In this study, we retrace the main threads of this chapter of proof-theoretical investigation, using Lorenzen's original framework as a general guide. (shrink)

The framework of natural deduction is extended by permitting rules as assumptions which may be discharged in the course of a derivation. this leads to the concept of rules of higher levels and to a general schema for introduction and elimination rules for arbitrary n-ary sentential operators. with respect to this schema, (functional) completeness "or", "if..then" and absurdity is proved.

A logical constant is weakly disharmonious if its elimination rules are weaker than its introduction rules. Substructural weak disharmony is the weak disharmony generated by structural restrictions on the eliminations. I argue that substructural weak disharmony is not a defect of the constants which exhibit it. To the extent that it is problematic, it calls into question the structural properties of the derivability relation. This prompts us to rethink the issue of controlling the structural properties of a logic by means (...) of harmony. I argue that such a control is possible and desirable. Moreover, it is best achieved by global tests of harmony. (shrink)

The paper proposes a semantic value for the logical constants (connectives and quantifiers) within the framework of proof-theoretic semantics, basic meaning on the introduction rules of a meaning conferring natural deduction proof system. The semantic value is defined based on Fregecontributions” to sentential meanings as determined by the function-argument structure as induced by a type-logical grammar. In doing so, the paper proposes a novel proof-theoretic interpretation of the semantic types, traditionally interpreted in Henkin models. The compositionality of the resulting attribution (...) of semantic values is discussed. Elsewhere, the same method was used for defining proof-theoretic meaning of subsentential phrases in a fragment of natural language. Doing the same for (the simpler and clearer case of) logic sheds more light on the proposal. (shrink)

The paper proposes an extension of the definition of a canonical proof, central to proof-theoretic semantics, to a definition of a canonical derivation from open assumptions. The impact of the extension on the definition of (reified) proof-theoretic meaning of logical constants is discussed. The extended definition also sheds light on a puzzle regarding the definition of local-completeness of a natural-deduction proof-system, underlying its harmony.

The structure of derivations in natural deduction is analyzed through isomorphism with a suitable sequent calculus, with twelve hidden convertibilities revealed in usual natural deduction. A general formulation of conjunction and implication elimination rules is given, analogous to disjunction elimination. Normalization through permutative conversions now applies in all cases. Derivations in normal form have all major premisses of elimination rules as assumptions. Conversion in any order terminates.Through the condition that in a cut-free derivation of the sequent Γ⇒C, no inactive weakening (...) or contraction formulas remain in Γ, a correspondence with the formal derivability relation of natural deduction is obtained: All formulas of Γ become open assumptions in natural deduction, through an inductively defined translation. Weakenings are interpreted as vacuous discharges, and contractions as multiple discharges. In the other direction, non-normal derivations translate into derivations with cuts having the cut formula principal either in both premisses or in the right premiss only. (shrink)