A Reduction Rule for Peirce Formula

Sachio Hirokawa, Yuichi Komori, Izumi Takeuti

    Research output: Contribution to journalArticlepeer-review

    1 Citation (Scopus)


    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


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

    Cite this