The language is only {->}. Assume we have a random set of propositional axiom schemas A1,..,An. We even know that each Aj is generally valid in classical logic. But we don't know whether we have a complete set of
axiom schemas for classical logic. Besides the axiom schemas we also have the modus ponens rule A, A -> B / B. Is such a Hilbert style calculus decidable. Is there an algorithm given a propositional formula C, that can nevertheless decide whether
C is derivable or not. It might not derive all classical propositional theorems, but can we arrange that some proof search always terminates with either the answer "yes", C is derivable or "no", C is not derivable?