There cannot exist an algorithm to verify a proof in second-order logic, because there is no finitary, complete, and sound set of inference rules. So how exactly do we get results in and about second-order logic?
That is, if a mathematician proves that ZFC with second-order logic implies X in some model, how can I tell whether the proof is correct or makes unjustified leaps?
In addition, if the answer is simply that we use some fixed finitary and sound set of inference rules, but not a complete set, isn't that just equivalent to first order ZFC + some finite collection of axioms, so really we are just proving first order theorems about systems with more axioms than ZFC?