The proofs of α→α in P - W

Journal of Symbolic Logic 61 (1):195-211 (1996)

Abstract
The syntactic structure of the system of pure implicational relevant logic P - W is investigated. This system is defined by the axioms B = (b → c) → (a → b) → a → c, B' = (a → b) → (b → c) → a → c, I = a → a, and the rules of substitution and modus ponens. A class of λ-terms, the closed hereditary right-maximal linear λ-terms, and a translation of such λ-terms M to BB'I-combinators M + is introduced. It is shown that a formula α is provable in P - W if and only if α is a type of some λ-term in this class. Hence these λ-terms represent proof figures in the Natural Deduction version of P - W. Errol Martin (1982) proved that no formula with form α → α is provable in P - W without using the axiom I. We show that a β-normal form λ-term M in the class is η reducible to λ x.x if the translated BB'I-combinator M + contains I. Using this theorem and Martin's result, we prove that a λ-term in the class is βη-reducible to λ x.x if the λ-term has a type α → α. Hence the structure of proofs of α → α in P - W is determined
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2307/2275604
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,350
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.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

On the No-Counterexample Interpretation.Ulrich Kohlenbach - 1999 - Journal of Symbolic Logic 64 (4):1491-1511.
A Compact Representation of Proofs.Dale A. Miller - 1987 - Studia Logica 46 (4):347 - 370.
Types of I -Free Hereditary Right Maximal Terms.Katalin Bimbó - 2005 - Journal of Philosophical Logic 34 (5/6):607 - 620.
A Lambda Proof of the P-W Theorem.Sachio Hirokawa, Yuichi Komori & Misao Nagayama - 2000 - Journal of Symbolic Logic 65 (4):1841-1849.

Analytics

Added to PP index
2009-01-28

Total views
46 ( #196,085 of 2,291,129 )

Recent downloads (6 months)
9 ( #99,146 of 2,291,129 )

How can I increase my downloads?

Downloads

My notes

Sign in to use this feature