A few things.

a) I'm a little confused by the discussion of Cantor's argument. As I understand it, the argument is valid in first-order logic, it's just that the conclusion may have different semantics in different models. That is, the statement "the set X is uncountable" is cashed out in terms of set theory, and so if you have a non-standard model of set theory, then that statement may have non-standard sematics.

This is all made horrendously confusing by the fact that when we do model theory we tend to model our domains using sets. So even in a non-standard model of set theory we'll usually be talking about sets doing the modelling, and so we may actually be using a set that is countable in the "outer" set theory in which we're working, but not in the "inner" theory which we're modelling.

What the requirement to use set theory to talk about first-order logic says about the status of logic is a whole other hopelessly circular kettle of fish.

Anyway, I think that's basically what you were saying, but I actually found your explanation harder to follow than the usual one. Which is unusual, since I normally think your explanations of mathsy stuff are very good!

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.

c) The Compactness theorem is the best reason not to use first-order logic. Seriously, it's weird as hell. We're all so used to it from doing model theory etc, but it's pretty counter-intuitive full stop; doesn't correspond to how we normally use logic; and leads to most of the "remarkable" properties of first-order logic.

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