[1] Every SOL (second order logic axiom system) has a corresponding Turing machine that verifies SOL statements, given a proof and axioms. (If this weren't the case, how could we be sure that our SOL proofs are correct?)
[3] From [1] and [2] every SOL has a corresponding FOL that verifies its proofs (meaning for each SOL axiom system, there is a FOL that verifies that a (SOL proof) proves a (SOL statement)).
How then can SOL be really different than FOL? Is SOL just FOL in disguise? Can we re-formulate SOL as FOL?
Short answer: Second order logic with full semantics is not recursively axiomatizable. In other words, a given recursively axiomatized second order proof system (one whose proofs a Turing machine could check) always falls short of capturing all the valid second order logical consequences. That's why SOL is essentially different from FOL, and why e.g. second order Peano arithmetic is essentially stronger than first order Peano arithmetic.
Long answer: look at a standard treatment of SOL such as Stewart Shapiro's classic text in the Oxford Logic Guides -- or, for a headline version, this encyclopedia article.