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 = (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
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2307/2695080
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 47,385
Through your library

References found in this work BETA

The Lambda Calculus. Its Syntax and Semantics.E. Engeler - 1984 - Journal of Symbolic Logic 49 (1):301-303.
Normalization Theorem for P-W.Misao Nagayama - 1999 - Bulletin of the Section of Logic 28 (2):83-88.
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.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Analytics

Added to PP index
2009-01-28

Total views
29 ( #324,628 of 2,291,102 )

Recent downloads (6 months)
5 ( #233,100 of 2,291,102 )

How can I increase my downloads?

Downloads

My notes

Sign in to use this feature