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 :-)
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 education consists of Godel, Escher, Bach. And a wikipedia education in game theory.
Do you have any suggestions on how to get started in this area? Like, introductory sources or even just terms that I should look up on wikipedia or google?
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.
If the outlined proof is less than N symbols long (which is true if N is large enough), the predictor will find it because it enumerates all proofs up to that length. Since the predictor’s proof system is consistent, it won’t find any other proofs contradicting this one.
The N < M is necessary to guarantee that the agent predicts the predictor’s proof, right?
Yeah. Actually, N must be exponentially smaller than M, so the agent’s proofs can completely simulate the predictor’s execution.
What happens if the outlined proof is more than N symbols long?
No idea. :-) Maybe the predictor will fail to prove anything, and fall back to filling only one box, I guess? Anyway, the outlined proof is quite short, so the problem already arises for not very large values of N.
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 education consists of Godel, Escher, Bach. And a wikipedia education in game theory.
Do you have any suggestions on how to get started in this area? Like, introductory sources or even just terms that I should look up on wikipedia or google?
If the outlined proof is less than N symbols long (which is true if N is large enough), the predictor will find it because it enumerates all proofs up to that length. Since the predictor’s proof system is consistent, it won’t find any other proofs contradicting this one.
The N < M is necessary to guarantee that the agent predicts the predictor’s proof, right?
What happens if the outlined proof is more than N symbols long?
Yeah. Actually, N must be exponentially smaller than M, so the agent’s proofs can completely simulate the predictor’s execution.
No idea. :-) Maybe the predictor will fail to prove anything, and fall back to filling only one box, I guess? Anyway, the outlined proof is quite short, so the problem already arises for not very large values of N.