A Reduction Rule for Peirce Formula

Sachio Hirokawa, Yuichi Komori, Izumi Takeuti

    研究成果: 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.

    本文言語英語
    ページ(範囲)419-426
    ページ数8
    ジャーナルStudia Logica
    56
    3
    DOI
    出版ステータス出版済み - 1 1 1996

    All Science Journal Classification (ASJC) codes

    • 論理
    • 科学史および科学哲学

    フィンガープリント

    「A Reduction Rule for Peirce Formula」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

    引用スタイル