David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Journal of Symbolic Logic 65 (4):1841-1849 (2000)
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)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Jan Krajíček (1998). Discretely Ordered Modules as a First-Order Extension of the Cutting Planes Proof System. Journal of Symbolic Logic 63 (4):1582-1596.
Daniele Mundici (1994). A Constructive Proof of McNaughton's Theorem in Infinite-Valued Logic. Journal of Symbolic Logic 59 (2):596-602.
Anita Wasilewska (1984). DFC-Algorithms for Suszko Logic and One-to-One Gentzen Type Formalizations. Studia Logica 43 (4):395 - 404.
Hiroakira Ono (1986). Craig's Interpolation Theorem for the Intuitionistic Logic and its Extensions—a Semantical Approach. Studia Logica 45 (1):19 - 33.
Ken-etsu Fujita (1998). On Proof Terms and Embeddings of Classical Substructural Logics. Studia Logica 61 (2):199-221.
Sachio Hirokawa (1992). The Converse Principal Type-Scheme Theorem in Lambda Calculus. Studia Logica 51 (1):83 - 95.
Yuichi Komori (1994). Syntactical Investigations intoBI Logic andBB′I Logic. Studia Logica 53 (3):397 - 416.
Takahito Aoto (1999). Uniqueness of Normal Proofs in Implicational Intuitionistic Logic. Journal of Logic, Language and Information 8 (2):217-242.
Sachio Hirokawa (1996). The Proofs of Α→Α in P - W. Journal of Symbolic Logic 61 (1):195-211.
Added to index2009-01-28
Total downloads6 ( #218,325 of 1,168,875 )
Recent downloads (6 months)1 ( #140,419 of 1,168,875 )
How can I increase my downloads?