  In this article, we deal with propositional calculi over a signature
containing the classical implication $\to$ with the rules of modus ponens and
substitution. For these calculi we consider few recognizing problems such as
recognizing derivations, extensions, completeness, and axiomatizations. The
main result of this paper is to prove that the problem of recognizing
extensions is undecidable for every propositional calculus, and the problems of
recognizing axiomatizations and completeness are undecidable for propositional
calculi containing the formula $x \to ( y \to x )$. As a corollary, the problem
of derivability of a fixed formula $A$ is also undecidable for all $A$.
Moreover, we give a historical survey of related results.
