Cfrgtkky

This is an easy consequence (Doets calls it Compactness Theorem (version 2)) in Kees Doets' Basic Model theory:

Let $Sigma$ a set of sentences and $phi$ a sentence.

If $Sigma models phi$, then for some finite $Delta subsetSigma$, $Delta models phi$.

The proof by contradiction reads:

"If $phi$ does not logically follow from some $Delta subset Sigma$, then the set $Sigma cup {neg phi}$ is finitely satisfiable and therefore, by compactness, satisfiable."

How do we know that $Sigma cup {neg phi}$ is finitely satisfiable?

From the fact that $phi$ does not logically follow from some $Delta$, we know that $neg phi$ follows from every $Delta subset Sigma$. But how does this imply that there's a model for every finite subset of the set of sentences?

First, a quick comment. Your statement "From the fact that $varphi$ does not logically follow from some $Delta$, we know that $negvarphi$ follows from every $Deltasubseteq Sigma$." is incorrect: when $A$ is a set of sentences, "$Anotmodels b$" is different from "$Amodelsneg b$." We could have $b$ be independent of $A$ - that is, $Anotmodels b$ and $Anotmodelsneg b$.

What is true is that since $varphi$ isn't entailed by any finite $DeltasubseteqSigma$, $negvarphi$ must be compatible with every finite $DeltasubseteqSigma$ in the sense that, for every $DeltasubseteqSigma$, the set $Deltacup{negvarphi}$ will be satisfiable. (It's arguably more natural to say "consistent with" instead of "compatible with," but consistency is a syntactic property which isn't needed in this purely semantic question, so I want to avoid using language which might bring in confusion.)

This is in fact the crux of the problem!

Saying "$Sigmacup{negvarphi}$ is finitely satisfiable" just means "$Deltacup{negvarphi}$ is satisfiable for every finite $DeltasubseteqSigma$." But "$Deltacup{negvarphi}$ is satisfiable" just means "there is some model of $Deltacup{negvarphi}$," which is to say $$Deltanotmodelsvarphi$$ ("$Deltamodelsvarphi$" means exactly "every model of $Delta$ satisfies $varphi$," which can't be true if there is some model of $Deltacup{negvarphi}$).

All that is to say that the statement "$Sigmacup{negvarphi}$ is finitely satisfiable" is equivalent to "For every finite $DeltasubseteqSigma$, we have $Deltanotmodelsvarphi$." But this latter statement is precisely our hypothesis "$varphi$ does not logically follow from some [finite] $DeltasubseteqSigma$!"

Note that the phrase "logically follow from" could confuse things here: it's meant in the semantic sense ($models$), not the syntactic sense ($vdash$).

My intuition about this does not (directly) use contradiction. Rather, it follows from the soundness and completeness of first-order logic:

If $SigmavDashphi$, then there is a proof of $Sigmavdashphi$ (completeness), and since that proof is a finite object it mentions at most finitely many of the axioms of $Sigma$. Therefore the same proof proves $Deltavdashphi$ for some finite $DeltasubseteqSigma$, and thus $DeltavDashphi$ (soundness).

Every $Delta$ finite have $DeltavDashlnotvarphi$, so every model of $Delta$ is a model of $Deltacup{lnotvarphi}$, and there is a model for every $Delta$, namely, the model of $Sigma$