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.
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.