BCK and BCI logics, condensed detachment and the $2$-property.
J. Roger Hindley · Notre Dame Journal of Formal Logic · 1993
Some of the main properties of the BCK and BCI logics of implication are summarized, focusing on their connections with their condensed logics and with combinators and lambda-calculus.(A condensed logic is the set of all formulas deducible from the logic's axioms by the condensed detachment rule of Carew Meredith.)A full proof is given of the preservation of the 2-and 1-2-properties by condensed detachment, based on ideas of S. Jaskowski.