The Proofs of $\alpha \rightarrow \alpha$ in $P - W$
Hirokawa, Sachio
J. Symbolic Logic, Tome 61 (1996) no. 1, p. 195-211 / Harvested from Project Euclid
The syntactic structure of the system of pure implicational relevant logic $P - W$ is investigated. This system is defined by the axioms $B = (b \rightarrow c) \rightarrow (a \rightarrow b) \rightarrow a \rightarrow c, B' = (a \rightarrow b) \rightarrow (b \rightarrow c) \rightarrow a \rightarrow c, I = a \rightarrow a$, and the rules of substitution and modus ponens. A class of $\lambda$-terms, the closed hereditary right-maximal linear $\lambda$-terms, and a translation of such $\lambda$-terms $M$ to $BB'I$-combinators $M^+$ is introduced. It is shown that a formula $\alpha$ is provable in $P - W$ if and only if $\alpha$ is a type of some $\lambda$-term in this class. Hence these $\lambda$-terms represent proof figures in the Natural Deduction version of $P - W$. Errol Martin (1982) proved that no formula with form $\alpha \rightarrow \alpha$ is provable in $P - W$ without using the axiom $I$. We show that a $\beta$-normal form $\lambda$-term $M$ in the class is $\eta$ reducible to $\lambda x.x$ if the translated $BB'I$-combinator $M^+$ contains $I$. Using this theorem and Martin's result, we prove that a $\lambda$-term in the class is $\beta\eta$-reducible to $\lambda x.x$ if the $\lambda$-term has a type $\alpha \rightarrow \alpha$. Hence the structure of proofs of $\alpha \rightarrow \alpha$ in $P - W$ is determined.
Publié le : 1996-03-14
Classification: 
@article{1183744933,
     author = {Hirokawa, Sachio},
     title = {The Proofs of $\alpha \rightarrow \alpha$ in $P - W$},
     journal = {J. Symbolic Logic},
     volume = {61},
     number = {1},
     year = {1996},
     pages = { 195-211},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183744933}
}
Hirokawa, Sachio. The Proofs of $\alpha \rightarrow \alpha$ in $P - W$. J. Symbolic Logic, Tome 61 (1996) no. 1, pp.  195-211. http://gdmltest.u-ga.fr/item/1183744933/