BCI-ALGEBRAS FROM THE POINT OF VIEW OF LOGIC
Jacek Kabziński · 2008
The following logics are the most noteworthy from the perspective of the calculus of combinators: the Hilbert’s positive implicational logic (i.e. purely implicational fragment of the intuitionistic propositional calculus), the Church’s weak theory of implication (i.e. purely implicational fragment of the relevant system R), the BCK-logic, and the BCI-logic. Their significance is due to a certain correspondence between combinators and implicational formulas (see for example [1]). The first three logics mentioned have been immensely investigated but it was not so in case of the remaining one. The BCI-logics was mentioned by A. N. Prior in the second edition of his Formal Logic of 1962 where it was credited to C. A. Meredith and dated in 1956 (see [4]). According to the definition the BCI-logic is determined by the following rules: