A Lambda Proof Of The P-w Theorem

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


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.



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

External links

  • This entry has no external links. Add one.
Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

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.


Added to PP

2 (#1,806,327)

6 months
2 (#1,203,099)

Historical graph of downloads

Sorry, there are not enough data points to plot this chart.
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

No references found.

Add more references