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!
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.
More clearly—“X is uncountable” means “there is no bijection between X and a subset of N”, but “there” stilll means “within the given model”.
Exactly (I’m assuming by subset you mean non-strict subset). Crucially, a non-standard model may not have all the bijections you’d expect it to, which is where EY comes at it from.
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.
Sure. So you’re not going to be able to prove (and hence know) some true statements. You might be able to do some meta-reasoning about your logic to figure some of these out, although quite how that’s supposed to work without requiring the context of set theory again, I’m not really sure.
bryjnar: I think the point is that the metalogical analysis that happens in the context of set theory is still a finite syntactical proof. In essense, all mathematics can be reduced to finite syntactical proofs inside of ZFC. Anything that really, truly, requires infinite proof in actual math is unknowable to everyone, supersmart AI included.
Absolutely, but it’s one that happens in a different system. That can be relevant. And I quite agree: that still leaves some things that are unknowable even by supersmart AI. Is that surprising? Were you expecting an AI to be able to know everything (even in principle)?
No, it is not surprising…
I’m just saying that saying that the semantics is impoverished if you only use finite syntactical proof, but not to any degree that can be fixed by just being really really really smart.
By semantics I mean your notion of what’s true. All I’m saying is that if you think that you can prove everything that’s true, you probably have a an overly weak notion of truth. This isn’t necessarily a problem that needs to be “fixed” by being really smart.
Also, I’m not saying that our notion of proof is too weak! Looking back I can see how you might have got the impression that I thought we ought to switch to a system that allows infinite proofs, but I don’t. For one thing, it wouldn’t be much use, and secondly I’m not even sure if there even is such a proof system for SOL that is complete.
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!
More clearly—“X is uncountable” means “there is no bijection between X and a subset of N”, but “there” stilll means “within the given model”.
Exactly (I’m assuming by subset you mean non-strict subset). Crucially, a non-standard model may not have all the bijections you’d expect it to, which is where EY comes at it from.
I was, but that’s not necessary—a countably infinite set can be bijectively mapped onto {2, 3, 4, …} which is a proper subset of N after all! ;-)
Oh yeah—brain fail ;)
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.
Isn’t the knowable limited to what can be known with finite chains of reasoning, whatever your base logic?
Sure. So you’re not going to be able to prove (and hence know) some true statements. You might be able to do some meta-reasoning about your logic to figure some of these out, although quite how that’s supposed to work without requiring the context of set theory again, I’m not really sure.
bryjnar: I think the point is that the metalogical analysis that happens in the context of set theory is still a finite syntactical proof. In essense, all mathematics can be reduced to finite syntactical proofs inside of ZFC. Anything that really, truly, requires infinite proof in actual math is unknowable to everyone, supersmart AI included.
Absolutely, but it’s one that happens in a different system. That can be relevant. And I quite agree: that still leaves some things that are unknowable even by supersmart AI. Is that surprising? Were you expecting an AI to be able to know everything (even in principle)?
No, it is not surprising… I’m just saying that saying that the semantics is impoverished if you only use finite syntactical proof, but not to any degree that can be fixed by just being really really really smart.
By semantics I mean your notion of what’s true. All I’m saying is that if you think that you can prove everything that’s true, you probably have a an overly weak notion of truth. This isn’t necessarily a problem that needs to be “fixed” by being really smart.
Also, I’m not saying that our notion of proof is too weak! Looking back I can see how you might have got the impression that I thought we ought to switch to a system that allows infinite proofs, but I don’t. For one thing, it wouldn’t be much use, and secondly I’m not even sure if there even is such a proof system for SOL that is complete.