The incompleteness of first-order arithmetic is relatively easy to wrap your head around -- there are non-standard models of PA in which Godel's sentence has a non-standard Godel number and so is "provable" in the model, and therefore false. So us "understanding that Godel's sentence is actually true" is just us operating in a stronger system, like ZFC or second-order arithmetic, in which the standard model of $\mathbb{N}$ is uniquely pinned down.
But with second-order logic, we have statements which are actually true but unprovable under standard semantics.
This I'm confused by. What is the "stronger system" that proves Godel's sentence for SOL? Surely there is one, since we know that Godel's sentence is "true but unprovable" in SOL? What system are we operating in?
"How" do we know/what kind of system knows that there is no model in which Godel's sentence is false?
Be careful with the definitions, and the answer should fall out nicely. We say that an FOL theory is syntactically complete iff it proves or disproves every sentence over its language. We say that FOL is semantically complete because for every set $A$ of FOL axioms over language $L$ and sentence $Q$ over $L$ such that every model of $A$ satisfies $Q$, we can prove (within the deductive system for FOL) $Q$ from $A$. These are two completely different concepts, but the qualifier before "complete" is often dropped because the first is about theories and the second is about logics (with associated deductive systems).
SOL (second-order logic) has two main flavours, one being Henkin semantics and the other being full semantics. SOL has a computable deductive system that is complete for Henkin semantics (since it can be reduced to FOL), but does not have any computable deductive system for full semantics. So although PA2 (second-order PA) under full semantics has a unique model under isomorphism, there is no computable deductive system that proves all and only its true statements.
So "provable in SOL" is not a well-defined notion for full semantics, because there is no computable notion of "proof" for full semantics. We could say that $\text{Th}(ℕ)$ proves all arithmetical sentences that are truths of PA2 under full semantics, but that is useless since $\text{Th}(ℕ)$ is not computable. Also, there is no such thing as "the Godel sentence for SOL", because Godel's theorems (even when generalized) are about computable formal systems. See here for the question about the Godel sentence for PA2 under Henkin semantics; of course it fails to prove it.
And all these can be proven in a meta-system like ZFC. That is, ZFC proves that every model of PA2 under full semantics is isomorphic to $ℕ$ (constructed from the minimal inductive set), and so on...