A lambda proof of the P-W theorem

The logical system P-W is an implicational non-commutative intuitionistic l ogic 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 p onens and substitution. The P-W problem is a problem asking whether alpha b eta holds if alpha --> beta and beta --> alpha are both provable in P-W. Th e answer is affirmative. The first to prove this was E. P. Martin by a sema ntical method. In this paper, we give the first proof of Martin's theorem based on the the ory of simply typed lambda -calculus. This proof is obtained as a corollary to the main theorem of this paper, shown without using Martin's Theorem, t hat any closed hereditary right-maximal linear (HRML) lambda -term of type alpha --> alpha is beta eta -reducible to lambda .x.x. Here the HRML lambda -terms correspond, via the Curry-Howard isomorphism, to the P-W proofs in natural deduction style.