Eliezer, I'm starting to think you're obsessed with Caledonian.

It's pretty astonishing that you would censor him and then accuse him of misrepresenting you. Where are all these false claims by Caledonian about your past statements? I haven't seen them.

For what it's worth, the censored version of Caledonian's comment didn't persuade me.

Larry D'Anna: Thanks, I think I understand the Deduction Theorem now.

Okay, I still don't see why we had to pinpoint the flaw in your proof by pointing to a step in someone else's valid proof.

Larry D'Anna identified the step you were looking for, but he did it by trying to transform the proof of Lob's Theorem into a different proof that said what you were pretending it said.

I think, properly speaking, the flaw is pinpointed by saying that you were misusing the theorems, not that the mean old theorem had a step that wouldn't convert into what you wanted it to be.

I've been looking more at the textual proof you linked (the cartoon was helpful, but it spread the proof out over more space) which is a little different and has an all-ascii notation that I'm going to borrow from.

I think if you used Lob's Theorem correctly, you'd have something like:

if PA |- []C -> C then PA |- C [Lob]

PA |- ([]C -> C) -> C [Deduction]

PA |- (not []C) -> C [Definition of implication]

(PA |- ((not []C) -> C) and (PA |- not []C) [New assumption]

PA |- ((not []C) -> C) and (not []C) [If you can derive two things, you can derive the conjunction]

PA |- C [Definition of implication]

And conclude that all provably unprovable statements are also provable, not that all unprovable statements are true.

(Disclaimer: I am definitely not a mathematician, and I skipped over your meta-ethics because I only like philosophy in small doses.)

I think the error is that you didn't prove it was unprovable -- all provably unprovable statements are also provable, but unprovable statements aren't necessarily true.

In other words, I think what you get from the Deduction Theorem (which I've never seen before, so I may have it wrong) is Provable((Provable(C) -> C) -> C). I think if you want to "reach inside" that outer Provable and negate the provability of C, you have to introduce Provable(not Provable(C)).

Eliezer, please don't ban Caledonian.

He's not disrupting anything, and doesn't seem to be trying to.

He may describe your ideas in ways that you think are incorrect, but so what? You spend a lot of time describing ideas that you disagree with, and I'll bet the people who actually hold them often disagree with your description.

Caledonian almost always disagrees with you, but treats you no differently than other commenters treat each other. He certainly treats you better than you treat some of your targets. For example, I've never seem him write a little dialog in which a character named "Goofus" espouses exaggerated versions of your ideas.

In this case, Caledonian seems to think that your four criteria are aimed at reconciling the two clashing intuitions and that it's a mistake to set such a goal. Well, so what? If that's not what you're trying to do, you fooled me as well.

To me, Caledonian just seems to have a very different take on the world than you and express it bluntly.

Unlike most of the others who've commented so far, I actually would have a very different outlook on life if you did that to me.

But I'm not sure how much it would change my behavior. A lot of the things you listed -- what to eat, what to wear, when to get up -- are already not based on right and wrong, at least for me. I do believe in right and wrong, but I don't make them the basis of everything I do.

For the more extreme things, I think a lot of it is instinct and habit. If I saw a child on the train tracks, I'd probably pull them off no matter what you'd proved to me. Even for more abstract things, like fraud, the thought that it would be wrong if there were a basis for right and wrong might be enough to make me feel I didn't want to do it.

"On the other hand, it is really hard for me to visualize the proposition that there is no kind of mind substantially stronger than a human one. I have trouble believing that the human brain, which just barely suffices to run a technological civilization that can build a computer, is also the theoretical upper limit of effective intelligence."

I don't think visualization is a very good test of whether a proposition is true. I can visualize an asteroidal chocolate cake much more easily than an entire cake-free asteroid belt.

But what about other ways for your Singularity to be impossible?

That was interesting, but I think you misunderstand time as badly as you expect us to misunderstand non-time

In regular time, the past no longer exists -- so there's no issue of whether it is changing or not -- and when we talk about the future changing, we're really referring to what is likely to happen in a future that doesn't exist yet.

A person living in a block universe could mistakenly think they have time by only perceiving the present. On the other hand, a person living in a timed universe could mistakenly think they live in a block by writing down their memories and expectations in a little diagram.

Eliezer, why doesn't the difficulty of creating this AGI count as a reason to think it won't happen soon?

You've said it's extremely, incredibly difficult. Don't the chances of it happening soon go down the harder it is?

Did Hofstadter explain the remark?

Maybe he felt that the difference between Einstein and a village idiot was larger than between a village idiot and a chimp. Chimps can be pretty clever.

Or, maybe he thought that the right end of the scale, where the line suddenly becomes dotted, should be the location of the rightmost point that represents something real. It's very conventional to switch from a solid to a dotted line to represent a switch from confirmed data to projections.

But I don't buy the idea of intelligence as a scalar value.