b) I kind of feel like Godel's theorem could be dropped from this post. While it's nice to reiterate the general point that "If you're using Godel's theorem in an argument and you're not a professional logician, you should probably stop", I don't think it actually helps the thrust of this post much. I'd just use Compactness.

Disagree. I actually understand Godel's incompleteness theorem, and started out misunderstanding it until a discussion similar to the one presented in this post, so this may help clear up the incompleteness theorem for some people. And unlike the Compactness theorem, Godel's completeness theorem at least seems fairly intuitive. Proving the existence of nonstandard models from the Compactness theorem seems kind of like pulling a rabbit out of a hat if you can't show me why the Compactness theorem is true.

Your semantics is impoverished if you can prove everything with finite syntactical proofs.

Do you have any basis for this claim?