{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T05:06:43Z","timestamp":1648962403602},"reference-count":12,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":6585,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1996,3]]},"abstract":"Abstract<\/jats:title>The syntactic structure of the system of pure implicational relevant logic P<\/jats:italic> \u2212 W<\/jats:italic> is investigated. This system is defined by the axioms B<\/jats:italic> = (b<\/jats:italic> \u2192 c<\/jats:italic>) \u2192 (a<\/jats:italic> \u2192 b<\/jats:italic>) \u2192 a<\/jats:italic> \u2192 c<\/jats:italic>, B<\/jats:italic>\u2032 = (a<\/jats:italic> \u2192 b<\/jats:italic>) \u2192 (b<\/jats:italic> \u2192 c<\/jats:italic>)\u2192 a<\/jats:italic> \u2192 c<\/jats:italic>, I<\/jats:italic> = a<\/jats:italic> \u2192 a<\/jats:italic>, and the rules of substitution and modus ponens. A class of \u03bb<\/jats:italic>-terms, the closed hereditary right-maximal linear<\/jats:italic>\u03bb<\/jats:italic>-terms, and a translation of such \u03bb<\/jats:italic>-terms M<\/jats:italic> to BB\u2032 I<\/jats:italic>-combinators M<\/jats:italic>+<\/jats:sup> is introduced. It is shown that a formula a is provable in P<\/jats:italic> \u2212 W<\/jats:italic> if and only if \u03b1<\/jats:italic> is a type of some \u03bb<\/jats:italic>-term in this class. Hence these \u03bb<\/jats:italic>-terms represent proof figures in the Natural Deduction version of P<\/jats:italic> \u2212 W<\/jats:italic>.<\/jats:p>Errol Martin (1982) proved that no formula with form \u03b1<\/jats:italic> \u2192 \u03b1<\/jats:italic> is provable in P<\/jats:italic> \u2212 W<\/jats:italic> without using the axiom I<\/jats:italic>. We show that a \u03b2<\/jats:italic>-normal form \u03bb<\/jats:italic>-term M<\/jats:italic> in the class is \u03b7<\/jats:italic> reducible to \u03bbx<\/jats:italic>.x<\/jats:italic> if the translated BB\u2032 I<\/jats:italic>-combinator M<\/jats:italic>+<\/jats:sup> contains I<\/jats:italic>. Using this theorem and Martin's result, we prove that a \u03bb<\/jats:italic>-term in the class is \u03b2\u03b7<\/jats:italic>-reducible to \u03bbx<\/jats:italic>.x<\/jats:italic> if the \u03bb<\/jats:italic>-term has a type \u03b1<\/jats:italic> \u2192 \u03b1<\/jats:italic>. Hence the structure of proofs of \u03b1<\/jats:italic> \u2192 \u03b1<\/jats:italic> in P<\/jats:italic> \u2212 W<\/jats:italic> is determined.<\/jats:p>","DOI":"10.2307\/2275604","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T22:57:36Z","timestamp":1146956256000},"page":"195-211","source":"Crossref","is-referenced-by-count":2,"title":["The proofs of \u03b1<\/i> \u2192 \u03b1<\/i> in P<\/i> \u2013 W<\/i>"],"prefix":"10.1017","volume":"61","author":[{"given":"Sachio","family":"Hirokawa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200017709_ref010","first-page":"95","volume-title":"Proceedings of the summer school and conference on mathematical logic, Heyting '88","author":"Ono","year":"1990"},{"key":"S0022481200017709_ref008","volume-title":"Introduction to combinators and lambda-calculus","author":"Hindley","year":"1986"},{"key":"S0022481200017709_ref007","first-page":"90","volume":"55","author":"Hindley","year":"1990","journal-title":"Principal type-schemes and condensed detachment"},{"key":"S0022481200017709_ref006","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90100-X"},{"key":"S0022481200017709_ref005","unstructured":"Hindley J. R. , A uniqueness lemma for linear lambda-terms, personal communication, 05 1987."},{"key":"S0022481200017709_ref003","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(76)90085-2"},{"key":"S0022481200017709_ref001","volume-title":"Entailment","volume":"1","author":"Anderson","year":"1975"},{"key":"S0022481200017709_ref009","first-page":"867","volume":"47","author":"Martin","year":"1982","journal-title":"Solution to the p\u2013w problem"},{"key":"S0022481200017709_ref012","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90114-7"},{"key":"S0022481200017709_ref011","first-page":"131","article-title":"On p-w","volume":"1","author":"Powers","year":"1976","journal-title":"The Relevance Logic Newsletter"},{"key":"S0022481200017709_ref004","unstructured":"Helman G. H. , Restricted lambda abstraction and the interpretation of some non-classical logics, Ph.D. thesis , University of Pittsburg, 1977."},{"key":"S0022481200017709_ref002","volume-title":"The lambda calculus","author":"Barendregt","year":"1984"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200017709","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T19:06:57Z","timestamp":1557774417000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200017709\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,3]]},"references-count":12,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1996,3]]}},"alternative-id":["S0022481200017709"],"URL":"https:\/\/doi.org\/10.2307\/2275604","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,3]]}}}