A simple approach to 5-and-10

post by Gurkenglas · 2018-12-17T18:33:46.735Z · score: 5 (1 votes) · LW · GW · 7 comments

To recap, A is trying to deduce enough about U to maximize it:

A := Find some f with a proof of "U = f(A)", then return argmax f.

If U is A, A can fail by proving f = {(5,5),(10,0)}: If it could prove this, it would be true, for only 5 is checked. Then by Löb's theorem, it can prove this.

I've thrown this problem at some people in my university and a fellow student's idea led to:

A' := Find all f with a proof of "U = f(A')", then return argmax (their pointwise maximum).

The true f is among the found f. Fooling ourselves into a suboptimal action would require us to believe it at least as good as the true maximum, which the single check refutes.

Note that A' can't prove that some f is not found, due to Gödel. Therefore, it can never prove what it is going to do!


Comments sorted by top scores.

comment by cousin_it · 2018-12-18T19:24:50.610Z · score: 3 (1 votes) · LW · GW

With "find some f", it's clear when the algorithm should stop. With "find all f" it's not as clear. If you stop after finding the first f, the problem comes back. If you search for all proofs up to some max length, nobody knows if the problem comes back or not.

comment by Gurkenglas · 2018-12-18T20:52:20.304Z · score: 1 (1 votes) · LW · GW

With "find all f" it ceases to be a classical algorithm. We search all proofs. For finitely many possible f it could be implemented using a halting oracle, for example. Decision theory approaches needn't be computable, right?

comment by cousin_it · 2018-12-19T10:38:38.359Z · score: 3 (1 votes) · LW · GW

Then I think you've reinvented this [LW · GW]. And there were many advances after this, so have heart :-)

comment by Gurkenglas · 2018-12-19T13:21:48.656Z · score: 1 (1 votes) · LW · GW

I think you're right, except I don't think I need the chicken rule. What's "have heart"? What should I read about the advances? Perhaps problems with each that I should try to use to invent each next one?

comment by cousin_it · 2018-12-19T14:17:06.012Z · score: 6 (2 votes) · LW · GW

Yeah, we figured out sometime later that the chicken rule isn't needed. Also we switched to using provability logic (a kind of modal logic), because it leads to a more natural formulation than halting oracles. As a bonus, that logic is decidable, so the whole thing can be implemented on a computer.


That idea is known as "modal UDT" and I'm happy to have come up with it, because it seems to be a local peak in the space of ideas. But unfortunately that's as far as it goes. Our world doesn't look like a modal formula, it's more like a cellular automaton, so we need decision theories that can work with that. Hence all the research on logical inductors etc.

comment by Gurkenglas · 2018-12-22T05:06:28.767Z · score: 1 (1 votes) · LW · GW

(Oh, "have heart" was not "stay strong even though you're 7 years behind", but "be merciful, I wrote that 7 years ago".)

Can the failure of this approach to handle scenarios as complicated as cellular automata be formalized using a problem like 5-and-10?

What do you mean by provability being decidable? Couldn't I ask whether it is provable that a Turing machine halts?

Edit: In Conway's Game of Life, one can build replicators and Turing machines. If we strewed provability oracle interfaces across the landscape, we should be able to implement this reasoner and it could do things like attempting to maximize the number of gliders. Pitted against a honeycomb maximizer, we could investigate whether they would each render themselves unpredictable to the other through the oracle, or whether the fact that war in Life just sends everything into primordial soup would get them to do a values handshake, etc. Doesn't sound like modal logic doesn't apply?

comment by cousin_it · 2018-12-27T23:35:30.992Z · score: 5 (2 votes) · LW · GW

Sorry about the late reply, I'm on vacation and not using the internet much. By have heart I meant stay strong. By decidability I meant this:


Solovay’s theorem is so significant because it shows that an interesting fragment of an undecidable formal theory like Peano Arithmetic—namely that which arithmetic can express in propositional terms about its own provability predicate—can be studied by means of a decidable modal logic, GL, with a perspicuous possible worlds semantics.

The post I linked is based on GL.

In your scenario with two reasoners, I think they will be unpredictable to each other, and both will fail to find enough counterfactuals to choose an action. Modal UDT is single player only.

More generally I think single player decision theory will never make game theory fall out for free - that dream should be abandoned. But that's a different conversation.