Let's assume that we have a consistent first-order theory, which was derived from a second order theory by replacing universal quantification over second order variables by axiom schemes for first-order definable predicates. Now let's compare this theory to two different second-order theories using Henkin semantics with suitable comprehension axiom schemes.
- If the comprehension axiom scheme allows quantification only over the first-order variables, can the resulting second-order theory be inconsistent? I guess the answer is no, and the resulting theory will be equivalent to the first-order theory with respect to provability of first-order formulas.
- If the comprehension axiom scheme allows quantification over both first and second-order variables, we can no longer be sure that the resulting second order theory is consistent. Is there a simple example, where the first-order theory is "provably consistent", and the second-order theory is "provably inconsistent"?
As already clarified in the comments, "provably (in)consistent" just means that assuming ZFC (or any other foundation) is fine, there is no need to restrict answers to syntactic derivations.