Second order induction could hardly be called a formal system: There is no complete, effective proof system for it. This is the basically the same limitation on first order PA. The standard model for second order arithmetic involves the power set of the naturals which is immediately a far more complex object than any computable system; it essentially presupposes the object that you're trying to formalize in the first place.
I don't see why the lack of a complete effective proof system for it should be a problem.
I do in fact consider the power set of the naturals to exist, so I'm not sure I see the problem? Is it just that uncountable sets have elements that we cannot pick out? I don't have a problem with that.
It matters because it means second order arithmetic isn't a finite object in the same way first order effective theories are where you might have "infinitely" many axioms but they are packaged up in a finite object, an algorithm.
The whole point of a formal system, its formality, is that it doesn't require any semantic notions to describe it. Second order arithmetic with its full model is no such thing. It is inherently infinitary and therefore not formal at all.
And it's a treacherous object. C.f. Richard's paradox which demonstrates that "subset of the integers" is by no means a naive idea.
