A lambda proof of the p-w theorem

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

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

Links

PhilArchive



    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

Analytics

Added to PP
2009-01-28

Downloads
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