The proofs of α → α in P – W

Publisher： Cambridge University Press

E-ISSN： 1943-5886|61|1|195-211

ISSN： 0022-4812

Source： The Journal of Symbolic Logic, Vol.61, Iss.1, 1996-03, pp. : 195-211

Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.

Previous Menu Next

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

Related content

α-decompositions of α-spaces

By  

The Journal of Symbolic Logic, Vol. 41, Iss. 2, 1976-06 ,pp. : 483-488 (6)

Cambridge University Press

Access to resources Recommend Favorite

On α-Relation and Transitivity Conditions of α

By Mirvakili S.   Anvariyeh S. M.   Davvaz B.  

Communications in Algebra, Vol. 36, Iss. 5, 2008-05 ,pp. : 1695-1703 (9)

Taylor & Francis Ltd

Access to resources Recommend Favorite

α-degrees of α-theories1

By  

The Journal of Symbolic Logic, Vol. 37, Iss. 4, 1972-12 ,pp. : 677-682 (6)

Cambridge University Press

Access to resources Recommend Favorite

α-Degrees of maximal α-r.e. sets

By  

The Journal of Symbolic Logic, Vol. 43, Iss. 3, 1978-09 ,pp. : 456-474 (19)

Cambridge University Press

Access to resources Recommend Favorite

ON α-LIKE RADICALS

By  

Bulletin of the Australian Mathematical Society, Vol. 84, Iss. 1, 2011-06 ,pp. : 111-115 (5)

Cambridge University Press

Access to resources Recommend Favorite