Abstract

The logical system P-W is an implicational non-commutative intuitionistic logic defined by axiom schemes $B = \rightarrow \rightarrow a \rightarrow c, B' = \rightarrow \rightarrow a \rightarrow c, I = a \rightarrow$ a with the rules of modus ponens and substitution. The P-W problem is a problem asking whether $\alpha = \beta$ holds if $\alpha \rightarrow \beta$ and $\beta \rightarrow \alpha$ 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 $\lambda$-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 $\lambda$-term of type $\alpha \rightarrow \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.