Nothing in your post or the proceeding discussion is of a "rather mathematical nature", let alone a precise specification of a mathematical problem.

Given a problem A, find an analogous problem B with the same payoff matrix for which it can be proven that any possible agent will make analogous decisions, or prove that such a problem B cannot exist.

You do realize that game theory is a branch of mathematics, as is decision theory? That we are trying to prove something here, not by empirical evidence, but by logic and reason alone? What do you think this is, social economics?

It's not the antagonistic tone of your comments that puts me off, it's the way in which you seem to deliberately not understand things. For example my definition of analogous — what else could you possibly have expected in this context? No, don't answer that.

I genuinely don't understand what question you're asking

I believe I have said everything already, but I'll put it in a slightly different way:

Given a problem A, find an analogous problem B with the same payoff matrix for which it can be proven that any possible agent will make analogous decisions, or prove that such a problem B cannot exist.

For instance, how can we find a problem that is analogous to Newcomb, but without Omega? I have described such an analogous problem in my top-level post and demonstrated how CDT agents will in the initial state not make the analogous decision. What we're looking for is a problem in which any imaginable agent would, and we can prove it. If we believe that such a problem cannot exist without Omega, how can we prove that?

The meaning of analogous should be very clear by now. Screw practical and impractical.

As an aside note, I don't know what kind of stuff they teach at US grad schools, but what's of help here is familiarity with methods of proof and a mathematical mindset rather than mathematical knowledge, except some basic game theory and decision theory. As far as I know, what I'm trying to do here is uncharted territory.

Oh wow this is so obvious in hindsight. Trying this asap thank you.

Machines aren't capable of evil. Humans make them that way.

-Lucca, Chrono Trigger

a pill that makes ordinary experience awesome

Psychedelic drugs already exist...

Thanks. Hm. I think I see why that can't be said in first order logic.

...my brain is shouting "if I start at 0 and count up I'll never reach a nonstandard number, therefore they don't exist" at me so loudly that it's very difficult to restrict my thoughts to only first-order ones.

There are two major branches of programming: Functional and Imperative. Unfortunately, most programmers only learn imperative programming languages (like C++ or python). I say unfortunately, because these languages achieve all their power through what programmers call "side effects". The major downside for us is that this means they can't be efficiently machine checked for safety or correctness. The first self-modifying AIs will hopefully be written in functional programming languages, so learn something useful like Haskell or Scheme.

Please be careful about exposing programmers to ideology; it frequently turns into politics kills their minds. This piece in particular is a well-known mindkiller, and I have personally witnessed great minds acting very stupid because of it. The functional/imperative distinction is not a real one, and even if it were, it's less important to provability than languages' complexity, the quality of their type systems and the amount of stupid lurking in their dark corners.

What I was thinking was "would you expect a FAI to do its own research about what it needs to for people to be physically safe enough, or should something on the subject be built in?

Thanks!

I suppose you can't prove a statement like "No matter how many times you expand this infinite family of axioms, you'll never encounter a non-standard number" in first-order logic? Should I not think of numbers and non-standard numbers as having different types? Or should I think of > as accepting differently typed things? (where I'm using the definition of "type" from computer science, e.g. "strongly-typed language")

I am well versed in most of this math, and a fair portion of the CS (mostly the more theoretical parts, not so much the applied bits). Should I contact you now, or should I study the rest of that stuff first?

In any case, this post has caused me to update significantly in the direction of "I should go into FAI research". Thanks.