In this paper we study (in some cases) the relationship between the
combinatory completeness of a set of typable combinators, with simple types,
for a system of lambda calculus and the axiomatic completeness, under
substitution and modus ponens, of the respective set of principal types for
the corresponding logical system. We show that combinatory completeness is a
necessary, but not sufficient, condition for axiomatic completeness in the
lambda-K-calculus and in the lambda-I-calculus, while the two problems become
equivalent for the BCK-lambda-calculus as well as for the BCI-lambda-calculus.
Furthermore, we present an algorithm which, whenever (B,alpha) is a principal
pair for some normal BCK-lambda-term M, reconstructs M up to alpha-conversion
and which fails if there is no normal BCK-lambda-term for which (B,alpha) is a
principal pair. From the correctness proof of the algorithm we also obtain
another proof for the fact that each BCK-lambda-term in normal form is
completely determined by its principal pairs.