Your thinking seems to be sort of correct, but informal. I'm not sure if my proof in the second part of the post was parseable, but at least it's an actual proof of the thing you want to know, so maybe you could try parsing it :-)
Thanks for the response, that was fast.
I can parse it, but I don't really think that I understand it in a mathematical way.
A is a statement that makes sense to me, and I can see why the predictor needs to know that the agent's proof system is consistent.
What I don't get about it is why you specify that the predictor computes proofs up to length N, and then just say how the predictor will do its proof.
Basically, I have no formal mathematics education in fields that aren't a direct prerequisite of basic multivariable calculus, and my informal mathematics edu...
Some people on LW have expressed interest in what's happening on the decision-theory-workshop mailing list. Here's an example of the kind of work we're trying to do there.
In April 2010 Gary Drescher proposed the "Agent simulates predictor" problem, or ASP, that shows how agents with lots of computational power sometimes fare worse than agents with limited resources. I'm posting it here with his permission:
About a month ago I came up with a way to formalize the problem, along the lines of my other formalizations:
Also Wei Dai has a tentative new decision theory that solves the problem, but this margin (and my brain) is too small to contain it :-)
Can LW generate the kind of insights needed to make progress on problems like ASP? Or should we keep working as a small clique?