\input zb-basic
\input zb-ioport
\iteman{io-port 01590619}
\itemau{Hirokawa, Sachio; Komori, Yuichi; Nagayama, Misao}
\itemti{A lambda proof of the P-W theorem.}
\itemso{J. Symb. Log. 65, No.4, 1841-1849 (2000).}
\itemab
Summary: The logical system P-W is an implicational non-commutative intuitionistic logic defined by axiom schemes $B= (b\to c)\to (a\to b)\to a\to c$, $B'= (a\to b)\to (b\to c)\to a\to c$. $I= a\to a$ with the rules of modus ponens and substitution. The P-W problem is a problem asking whether $\alpha= \beta$ holds if $\alpha\to \beta$ and $\beta\to \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 (HRML) $\lambda$-term of type $\alpha\to \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.
\itemrv{~}
\itemcc{}
\itemut{intuitionistic logic; P-W problem; simply typed $\lambda$-calculus}
\itemli{doi:10.2307/2695080}
\end