The proofs of α → α in P - W

Research output: Contribution to journalArticle

2 Citations (Scopus)

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 languageEnglish
Pages (from-to)195-211
Number of pages17
JournalJournal of Symbolic Logic
Volume61
Issue number1
Publication statusPublished - Mar 1 1996

Fingerprint

Term
Natural Deduction
Axiom
Axioms
Normal Form
Substitution
Figure
Logic
If and only if
Closed
Class
Theorem
Relevant Logic
Modus Ponens
Syntactic Structure

All Science Journal Classification (ASJC) codes

  • Logic

Cite this

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

In: Journal of Symbolic Logic, Vol. 61, No. 1, 01.03.1996, p. 195-211.

Research output: Contribution to journalArticle

@article{24b99107bd074d4e921e4fc833da2ec2,
title = "The proofs of α → α in P - W",
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.",
author = "Sachio Hirokawa",
year = "1996",
month = "3",
day = "1",
language = "English",
volume = "61",
pages = "195--211",
journal = "Journal of Symbolic Logic",
issn = "0022-4812",
publisher = "Association for Symbolic Logic",
number = "1",

}

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 -