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 = (b → c) → (a → b) → a → c, B' = (a → b) → (b → c) → a → c, I = a → a with the rules of modus ponens and substitution. The P-W problem is a problem asking whether α = β holds if α → β and β → α 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 λ-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) λ-term of type α → α is βη-reducible to λ x.x. Here the HRML λ-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: 93,296

External links

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

Through your library

Similar books and articles


Added to PP

15 (#976,359)

6 months
54 (#89,269)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

The Lambda Calculus. Its Syntax and Semantics.E. Engeler - 1984 - Journal of Symbolic Logic 49 (1):301-303.
A Constructive Proof of a Theorem in Relevance Logic.Aleksandar Kron - 1985 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 31 (25-28):423-430.
A Constructive Proof of a Theorem in Relevance Logic.Aleksandar Kron - 1985 - Mathematical Logic Quarterly 31 (25‐28):423-430.
Normalization theorem for P-W.Misao Nagayama - 1999 - Bulletin of the Section of Logic 28 (2):83-88.

Add more references