General-elimination harmony and higher-level rules

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

8 Citations (Scopus)
4 Downloads (Pure)


Michael Dummett introduced the notion of harmony in response to Arthur Prior's tonkish attack on the idea of proof-theoretic justification of logical laws (or analytic validity). But Dummett vacillated between different conceptions of harmony, in an attempt to use the idea to underpin his anti-realism. Dag Prawitz had already articulated an idea of Gerhard Gentzen's into a procedure whereby elimination-rules are in some sense functions of the corresponding introduction-rules. The resulting conception of general-elimination harmony ensures that the rules are transparent in the meaning they confer, in that the elimination-rules match the meaning the introduction-rules confer. The general-elimination rules which result may be of higher level, in that the assumptions discharged by the rule may be of (the existence of) derivations rather than just of formulae. In many cases, such higher-level rules may be "flattened" to rules discharging only formulae. However, such flattening is often only possible in the richer context of so-called ''classical" or realist negation, or in a multiple-conclusion environment. In a constructivist context, the flattened rules are harmonious but not stable.
Original languageEnglish
Title of host publicationDag Prawitz on Proofs and Meaning
Subtitle of host publicationOutstanding Contributions to Logic: Volume 7
EditorsHeinrich Wansing
Place of PublicationBerlin
Number of pages20
ISBN (Electronic)978-3-319-11041-7
ISBN (Print)978-3-319-11040-0
Publication statusPublished - 2015

Publication series

NameOutstanding Contributions to Logic
ISSN (Print)2211-2758


  • Harmony
  • 'Tonk'
  • Generalized-elimination rules
  • Higher-level rules
  • Flattening
  • Reduction
  • Local completeness
  • Classical logic
  • Intuitionistic logic
  • Negation
  • Gentzen
  • Dummet
  • Prawitz


Dive into the research topics of 'General-elimination harmony and higher-level rules'. Together they form a unique fingerprint.

Cite this