ABSTRACT. In the setting of classical first-order logic with inductive predicates, we give as example a theory for which the conjectures that cannot be proved without induction reasoning are still not provable by adding non-trivial explicit induction reasoning.