# A Lambda Proof Of The P-w Theorem

Journal of Symbolic Logic 65 (4):1841-1849 (2000)

# 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.

## PhilArchive

Upload a copy of this work     Papers currently archived: 92,100

Setup an account with your affiliations in order to access resources via your University's proxy server

# Similar books and articles

The Proofs of $alpha rightarrow alpha$ in $P - W$.Sachio Hirokawa - 1996 - Journal of Symbolic Logic 61 (1):195-211.
A lambda proof of the p-w theorem.Sachio Hirokawa, Yuichi Komori & Misao Nagayama - 2000 - Journal of Symbolic Logic 65 (4):1841-1849.
Types of I -free hereditary right maximal terms.Katalin Bimbó - 2005 - Journal of Philosophical Logic 34 (5/6):607 - 620.
On regular reduced products.Juliette Kennedy & Saharon Shelah - 2002 - Journal of Symbolic Logic 67 (3):1169-1177.
Countable structures, Ehrenfeucht strategies, and wadge reductions.Tom Linton - 1991 - Journal of Symbolic Logic 56 (4):1325-1348.
Upper Bounds for Standardizations and an Application.Hongwei Xi - 1999 - Journal of Symbolic Logic 64 (1):291-303.
Universal solutions of a nonlinear heat equation on $\mathbb{R}^N$.Thierry Cazenave, Flávio Dickstein & Fred B. Weissler - 2003 - Annali della Scuola Normale Superiore di Pisa- Classe di Scienze 2 (1):77-117.
Types of $\mathsf{I}$ -Free Hereditary Right Maximal Terms.Katalin Bimbó - 2005 - Journal of Philosophical Logic 34 (5-6):607-620.
On the No-Counterexample Interpretation.Ulrich Kohlenbach - 1999 - Journal of Symbolic Logic 64 (4):1491-1511.

2017-02-21

2 (#1,806,327)

6 months
2 (#1,203,099)