A Reduction Rule for Peirce Formula

Sachio Hirokawa, Yuichi Komori, Izumi Takeuti

Research output: Contribution to journalArticle


A reduction rule is introduced as a transformation of proof figures in implicational classical logic. Proof figures are represented as typed terms in a λ-calculus with a new constant p((α→β)→α)→α. It is shown that all terms with the same type are equivalent with respect to β-reduction augmented by this P-reduction rule. Hence all the proofs of the same implicational formula are equivalent. It is also shown that strong normalization fails for βP-reduction. Weak normalization is shown for βP-reduction with another reduction rule which simplifies α of ((α → β) → α) → α into an atomic type.

Original languageEnglish
Pages (from-to)419-426
Number of pages8
JournalStudia Logica
Issue number3
Publication statusPublished - Jan 1 1996

All Science Journal Classification (ASJC) codes

  • Logic
  • History and Philosophy of Science

Fingerprint Dive into the research topics of 'A Reduction Rule for Peirce Formula'. Together they form a unique fingerprint.

  • Cite this

    Hirokawa, S., Komori, Y., & Takeuti, I. (1996). A Reduction Rule for Peirce Formula. Studia Logica, 56(3), 419-426. https://doi.org/10.1007/BF00372774