That's not how arguments from contradiction work. You've assumed H (halting problem is decidable), prove B (beauty decidable), then say "but actually !H, therefore !B". All you've proven is that H => B. An actual argument from contradiction is "assume H, using H we can prove an obviously false statement, therefore not-H". And indeed, you have assumed something false (H), and shown a contradiction (various proofs for !H), so your original assumption was wrong (!H).

A concrete example: say Beauty(R,D) is trivially decidable (say it returns (popcount(R)+popcount(D))%2. Your argument "proves" this property is undecidable, but it's definitely decidable. So some step in your argument is wrong.

Another concrete example: Assume the halting problem is decidable. I would like a cookie. But the halting problem is not decidable. Therefore I would not like a cookie.

You are just repeating my critique. I am not the one making the mistake.

So you mean your frustration is warranted then?

If that is the kind of work published by academics associated with the MIT and La Pontificia Universidad de Madrid, then maybe I should not feel frustrated after all by not being an academic.

But you said in your first comment that you were an academic.

"I confess I am a frustrated academic"

if you're not being facetious,

in English vernacular being a frustrated X (as in a frustrated academic, frustrated poet, etc.) means that the person is actually not that, but have in some way been prevented from being the thing (frustrated) and have perhaps rancor in regards to the frustration and towards those who actually are the thing (this second feature being sometimes implied depending on who is doing the description of the person as frustrated)

on edit: formatting, clarification

Thanks, I wasn't aware of the 2nd meaning. I also interpreted the "frustrated academic" as "an annoyed academic", rather than "an unsuccesfull academic".

I'm thinking maybe it is no longer as common an expression as I thought, given the people who've mistaken it here.

I think it didn't help that they used both meanings of the word "frustrated" in the same sentence. By adding "perhaps my frustration is unwarranted", it puts emphasis on the fact they are frustrated, not that they failed to become an academic. It leads the reader to believe they are in fact still an active academic.

I was only dimly aware of the second meaning of the word so I'm not sure how you would interpret it if you had a good understanding of the multiple interpretations.

As an English speaker, my only interpretation was that you were an academic frustrated about academia.

https://www.ldoceonline.com/dictionary/a-frustrated-artist-a... - came up if I search for 'meaning of frustrated poet' which is the kind of thing where the phrasing most often comes up.

That isn't even the same user.

He is proving his point by contradicting himself, a true mathematician.

Ah, I misunderstood you! I apologize. :)

I think maybe you made a typo in your OP? The authors assume beauty is decidable and use that to show that would imply that the halting problem is undecidable. It applies to anything, like you say, and to me it seems like a silly argument, but I think it’s a valid proof given the premises.

But it's not an argument from the paper. The idea is that superintelligence have to understand a consequence of any program to check for harm. And this is undecidable due to the halting problem. This argument is correct, but trivial and not worth a paper, in my opinion.

The harming algorithm is just used in the paper's proof as a simple wrapper around the halting algorithm.

I think the typographical similarity of "halting" and "harming" may be causing some confusion. The contradictory assumption in the paper is not the decidability of the halting problem, but rather the decidability of the harming problem.

I got that point (in your comment and in the paper), but that is just a lousy argument, the _harming_ problem is fed the _halting_ problem, and since the second is undecidable the first it also is. So in essence the argument boils down to my original point.

How to prove your pizza is poisonous.

Let's put some cyanide in your pizza. Now let's assume by contradiction your pizza is not poisonous, but alas, in contains cyanide which is poisonous then so it is the pizza.

It's more like "it's impossible to prove that every pizza isn't poisonous, because here's a proof that a certain pizza contains cyanide."

Some particular pizza might very well be non-poisonous, but this is a statement about all pizzas.

No, you are confusing the metaphor. In this case the pizza is the harming algo, the cyanide the halting problem and the poisonous quality the fact they are undecidable or not. You are not reasoning about a set of pizzas , just one pizza in particular.

What about many-valued logic like in balanced ternary where you have -1 for false, 0 for something like don't care(in this context/tbd), and 1 for true?