General-elimination stability

Bruno Miguel Jacinto, Stephen Louis Read

Research output: Contribution to journalArticlepeer-review

13 Citations (Scopus)
3 Downloads (Pure)


General-elimination harmony articulates Gentzen's idea that the elimination-rules are justified if they infer from an assertion no more than can already be inferred from the grounds for making it. Dummett described the rules as not only harmonious but stable if the E-rules allow one to infer no more and no less than the I-rules justify. Pfenning and Davies call the rules locally complete if the E-rules are strong enough to allow one to infer the original judgement. A method is given of generating harmonious general-elimination rules from a collection of I-rules. We show that the general-elimination rules satisfy Pfenning and Davies' test for local completeness, but question whether that is enough to show that they are stable. Alternative conditions for stability are considered, including equivalence between the introduction- and elimination-meanings of a connective, and recovery of the grounds for assertion, finally generalizing the notion of local completeness to capture Dummett's notion of stability satisfactorily. We show that the general-elimination rules meet the last of these conditions, and so are indeed not only harmonious but also stable.
Original languageEnglish
Pages (from-to)361-405
JournalStudia Logica
Issue number2
Early online date18 Oct 2016
Publication statusPublished - Apr 2017


  • Harmony
  • General-elimination rules
  • Stability
  • Local completeness
  • Grounds
  • Gentzen


Dive into the research topics of 'General-elimination stability'. Together they form a unique fingerprint.

Cite this