The proofs of α → α in P - W

Sachio Hirokawa

    研究成果: Contribution to journalArticle査読

    2 被引用数 (Scopus)

    抄録

    The syntactic structure of the system of pure implicational relevant logic P - W is investigated. This system is defined by the axioms B = (b → c) → (a → b) → a → c, B′ = (a - b) → (b → c) → a → c, I = a → a, and the rules of substitution and modus ponens. A class of λ-terms, the closed hereditary right-maximal linear λ-terms, and a translation of such λ-terms M to BB′ I-combinators M+ is introduced. It is shown that a formula α is provable in P - W if and only if α is a type of some λ-term in this class. Hence these λ-terms represent proof figures in the Natural Deduction version of P - W. Errol Martin (1982) proved that no formula with form α → α is provable in P - W without using the axiom I. We show that a β-normal form λ-term M in the class is η reducible to λx.x if the translated BB′ I-combinator M+ contains I. Using this theorem and Martin's result, we prove that a λ-term in the class is βη-reducible to λx.x if the λ-term has a type α → α. Hence the structure of proofs of α → α in P - W is determined.

    本文言語英語
    ページ(範囲)195-211
    ページ数17
    ジャーナルJournal of Symbolic Logic
    61
    1
    出版ステータス出版済み - 3 1 1996

    All Science Journal Classification (ASJC) codes

    • Logic

    フィンガープリント 「The proofs of α → α in P - W」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

    引用スタイル