### 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.

Original language | English |
---|---|

Pages (from-to) | 195-211 |

Number of pages | 17 |

Journal | Journal of Symbolic Logic |

Volume | 61 |

Issue number | 1 |

Publication status | Published - Mar 1 1996 |

### Fingerprint

### All Science Journal Classification (ASJC) codes

- Logic

### Cite this

**The proofs of α → α in P - W.** / Hirokawa, Sachio.

Research output: Contribution to journal › Article

*Journal of Symbolic Logic*, vol. 61, no. 1, pp. 195-211.

}

TY - JOUR

T1 - The proofs of α → α in P - W

AU - Hirokawa, Sachio

PY - 1996/3/1

Y1 - 1996/3/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0038869359&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0038869359&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:0038869359

VL - 61

SP - 195

EP - 211

JO - Journal of Symbolic Logic

JF - Journal of Symbolic Logic

SN - 0022-4812

IS - 1

ER -