Evidence is given that implication (and its special case, negation) carry the logical strength of a system of formal logic. This is done by proving normalization and cut elimination for a system based on combinatory logic or $\lambda$-calculus with logical constants for and, or, all, and exists, but with none for either implication or negation. The proof is strictly finitary, showing that this system is very weak. The results can be extended to a "classical" version of the system. They can also be extended to a system with a restricted set of rules for implication: the result is a system of intuitionistic higher-order BCK logic with unrestricted comprehension and without restriction on the rules for disjunction elimination and existential elimination. The result does not extend to the classical version of the BCK logic.
@article{1183746170,
author = {Seldin, Jonathan P.},
title = {On the Role of Implication in Formal Logic},
journal = {J. Symbolic Logic},
volume = {65},
number = {1},
year = {2000},
pages = { 1076-1114},
language = {en},
url = {http://dml.mathdoc.fr/item/1183746170}
}
Seldin, Jonathan P. On the Role of Implication in Formal Logic. J. Symbolic Logic, Tome 65 (2000) no. 1, pp. 1076-1114. http://gdmltest.u-ga.fr/item/1183746170/