I'm trying to understand this proof in Shawn Hedman's book, "A First Course in Logic":
Proposition 1.19: For any formulas F and G, G is a consequence of F if and only if F → G is a tautology.
Proof: We show that $F → G is not a tautology if and only if G is not a consequence of F. By the definition of “tautology,” F → G is not a tautology if and only if there exists an assignment A such that A ⊨ ¬(F → G). By the definition of “→,” A ⊨ ¬(F → G) if and only if A ⊨ ¬(¬F ∨ G). By the semantics of propositional logic, A |= ¬(¬F ∨ G) if and only if both A ⊨ F and A ⊨ ¬G.
Finally, by the definition of “consequence,” there exists an assignment A such that A ⊨ F and A ⊨ ¬G if and only if G is not a consequence of F.
I was able to follow the proof until the last sentence. By definition, A ⊨ F and A ⊨ ¬G would mean that F ⊨ ¬G, right? Is this the same as "G is not a consequence of F"?
It's important to distinguish types of object here; I'll use script for assignments and normal font for formulas.
You say (modulo notational tweaking) that
However, that's false: "$F\models\neg G$" is an extremely strong statement, namely that every assignment making $F$ true makes $G$ false. All we can conclude from seeing an $\mathscr{A}$ with $\mathscr{A}\models F$ and $\mathscr{A}\models\neg G$ is that some assignment making $F$ true makes $G$ false; this is the much weaker (unless $F$ has no satisfying assignments at all!) statement $F\not\models G$.
As to your question, "$G$ is not a consequence of $F$" means "$F\not\models G$" simply by definition. Basically, we can't conclude (from the little we've already seen) that $F\models\neg G$, but we can conclude $F\not\models G$, and that latter (generally weaker) claim is what we're trying to prove.