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.
I absolutely agree that this will help people stop being confused about Godel’s theorem, I just don’t know why EY does it in this particular post.
Do you have any basis for this claim?
Nope, it’s pure polemic ;) Intuitively I feel like it’s a realism/instrumentalism issue: claiming that the only things which are true are provable feels like collapsing the true and the knowable. In this case the decision is about which tool to use, but using a tool like first-order logic that has these weird properties seems suspicious.
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.
Do you have any basis for this claim?
I absolutely agree that this will help people stop being confused about Godel’s theorem, I just don’t know why EY does it in this particular post.
Nope, it’s pure polemic ;) Intuitively I feel like it’s a realism/instrumentalism issue: claiming that the only things which are true are provable feels like collapsing the true and the knowable. In this case the decision is about which tool to use, but using a tool like first-order logic that has these weird properties seems suspicious.