A lambda proof of the P-W theorem

Sachio Hirokawa, Yuichi Komori, Misao Nagayama

    Research output: Contribution to journalArticlepeer-review


    The logical system P-W is an implicational non-commutative intuitionistic logic defined by axiom schemes B = (b → c) → (a → b) → a → c. B′ = (a → b) → (b → c) → a → c. I = a → a with the rules of modus ponens and substitution. The P-W problem is a problem asking whether α = β holds if α → β and β → α are both provable in P-W. The answer is affirmative. The first to prove this was E. P. Martin by a semantical method. In this paper, we give the first proof of Martin's theorem based on the theory of simply typed λ-calculus. This proof is obtained as a corollary to the main theorem of this paper, shown without using Martin's Theorem, that any closed hereditary right-maximal linear (HRML) λ-term of type α → α is βη-reducible to λx.x. Here the HRML λ-terms correspond, via the Curry-Howard isomorphism, to the P-W proofs in natural deduction style.

    Original languageEnglish
    Pages (from-to)1841-1849
    Number of pages9
    JournalJournal of Symbolic Logic
    Issue number4
    Publication statusPublished - Dec 2000

    All Science Journal Classification (ASJC) codes

    • Philosophy
    • Logic


    Dive into the research topics of 'A lambda proof of the P-W theorem'. Together they form a unique fingerprint.

    Cite this