You have finally proven to me that Lob’s theorem is as absurd as it sounds on the face of it.
When math seems absurd to you, this is generally a signal that you’ve got something interesting to learn, rather than that you’ve got a superior epistemic vantage point to mathematics.
No, seriously, this stuff is awesome and you should check it out. I’m realizing that I need a better grasp of it in order to write it up, so I’m checking out The Logic of Provability on Monday.
Oh, I agree that it’s true in mathematics. I just recognize that things which are proven within a strict construction of mathematics might not apply outside that strict interpretation.
It’s the intersection between Godel and Lob’s theorems that really throws me off- anything which is not false in PA can be proven in PA, including nonce statements, but there are things that are true in PA which cannot be proven in PA, and there is a mechanism for generating such statements.
Consider the statement G: “G cannot be proven in PA”. G is proven in PA+1, because if PA were to have a proof of G, then G would be false and PA would prove something which is false. So far, so good- but PA proves that PA+1 proves G; since the only axiom in PA+1 not in PA is “PA is sound”, PA proves that “PA is sound->G is true”.
If PA is not sound, then PA proves G is true. (trivial, since an unsound system proves everything)
PA is either (sound or not sound).
PA proves (if PA is sound, G is true.)
PA proves that (if PA is not sound, PA proves that G is true)
(PA proves that G is true) within PA implies G is true.
PA proves that G is true If PA is (sound or unsound).
PA proves that G is true.
PA proves that PA is not sound.
I’m not sure if I’m literally only using the axiom “S is either sound or not sound” to prove “S proves that S is not sound”. I’m sure that the principle of explosion requires a few axioms more, and that I’ve made a (common?) fatal error somewhere, but I’m comfortable with calling mathematical constructions “Absurd” without calling them false.
The best response to “X is absurd” is “Reality is absurd”, a point with which I will readily agree.
EDIT: Corrected a couple of major typos resulting in GCE, other errors are probably still present.
When math seems absurd to you, this is generally a signal that you’ve got something interesting to learn, rather than that you’ve got a superior epistemic vantage point to mathematics.
No, seriously, this stuff is awesome and you should check it out. I’m realizing that I need a better grasp of it in order to write it up, so I’m checking out The Logic of Provability on Monday.
Oh, I agree that it’s true in mathematics. I just recognize that things which are proven within a strict construction of mathematics might not apply outside that strict interpretation.
It’s the intersection between Godel and Lob’s theorems that really throws me off- anything which is not false in PA can be proven in PA, including nonce statements, but there are things that are true in PA which cannot be proven in PA, and there is a mechanism for generating such statements.
Consider the statement G: “G cannot be proven in PA”. G is proven in PA+1, because if PA were to have a proof of G, then G would be false and PA would prove something which is false. So far, so good- but PA proves that PA+1 proves G; since the only axiom in PA+1 not in PA is “PA is sound”, PA proves that “PA is sound->G is true”.
If PA is not sound, then PA proves G is true. (trivial, since an unsound system proves everything)
PA is either (sound or not sound).
PA proves (if PA is sound, G is true.)
PA proves that (if PA is not sound, PA proves that G is true)
(PA proves that G is true) within PA implies G is true.
PA proves that G is true If PA is (sound or unsound).
PA proves that G is true.
PA proves that PA is not sound.
I’m not sure if I’m literally only using the axiom “S is either sound or not sound” to prove “S proves that S is not sound”. I’m sure that the principle of explosion requires a few axioms more, and that I’ve made a (common?) fatal error somewhere, but I’m comfortable with calling mathematical constructions “Absurd” without calling them false.
The best response to “X is absurd” is “Reality is absurd”, a point with which I will readily agree.
EDIT: Corrected a couple of major typos resulting in GCE, other errors are probably still present.