It may or may not be proven that TDT settles on answers to questions involving TDT. If TDT doesn’t get an answer, then TDT can’t get an answer.
Presumably it is true that TDT settles but if it isn’t proven, it may not be true; or it could be that the proof (i.e. a formalization of TDT) will provide insight that is currently lacking (such as cutting off after a certain level of resource use; can Omega emulate how many resources the current TDT agent will use? Can the TDT agent commit to using a random number of resources? Do true random-number generators exist? These problems might all be inextricable. Or they might not. I, for one, don’t know.)
Having several formalizations is 90% of a proof, not 100% of a proof. Turn the formalization into a computer program AND either prove that it halts or run this simulation on it in finite time.
I believe that it’s true that TDT will get an answer and hence Omega will get an answer, but WHY this is true relies on facts about TDT that I don’t know (specifically facts about its implementation; maybe facts about differential topology that game-theoretic equilibrium results rely on.)
The linked posts have proofs that the programs halt and return the correct answer. Do you understand the proofs, or could you point out the areas that need more work? Many commenters seemed to understand them...
I do not understand the proofs, primarily because I have not put time in to trying to understand them.
I may have become somewhat defensive in these posts (or withdrawn I guess?) but looking back my original point was really to point out that, naively, asking whether the problem is well-defined is a reasonable question.
The questions in the OP set off alarm bells for me of “this type of question might be a badly-defined type of question” so asking whether these decisions are in the “halting domain” (is there an actual term for that?) of TDT seems like a reasonable question to ask before putting too much thought into other issues.
I believe the answer to be that yes these questions are in the “halting domain” of TDT, but I also believe that understanding what that is and why these questions are legitimate and the proofs that TDT halts will be central to any resolution of these problems.
What I’m really trying to say here is that it makes sense to ask these questions, but I don’t understand why, so I think Davorak’s question was reasonable, and your answer didn’t feel complete to me. Looking back, I don’t think I’ve contributed much to this conversation. Sorry!
It may or may not be proven that TDT settles on answers to questions involving TDT. If TDT doesn’t get an answer, then TDT can’t get an answer.
Presumably it is true that TDT settles but if it isn’t proven, it may not be true; or it could be that the proof (i.e. a formalization of TDT) will provide insight that is currently lacking (such as cutting off after a certain level of resource use; can Omega emulate how many resources the current TDT agent will use? Can the TDT agent commit to using a random number of resources? Do true random-number generators exist? These problems might all be inextricable. Or they might not. I, for one, don’t know.)
We have several formalizations of UDT that would solve this problem correctly.
Having several formalizations is 90% of a proof, not 100% of a proof. Turn the formalization into a computer program AND either prove that it halts or run this simulation on it in finite time.
I believe that it’s true that TDT will get an answer and hence Omega will get an answer, but WHY this is true relies on facts about TDT that I don’t know (specifically facts about its implementation; maybe facts about differential topology that game-theoretic equilibrium results rely on.)
The linked posts have proofs that the programs halt and return the correct answer. Do you understand the proofs, or could you point out the areas that need more work? Many commenters seemed to understand them...
I do not understand the proofs, primarily because I have not put time in to trying to understand them.
I may have become somewhat defensive in these posts (or withdrawn I guess?) but looking back my original point was really to point out that, naively, asking whether the problem is well-defined is a reasonable question.
The questions in the OP set off alarm bells for me of “this type of question might be a badly-defined type of question” so asking whether these decisions are in the “halting domain” (is there an actual term for that?) of TDT seems like a reasonable question to ask before putting too much thought into other issues.
I believe the answer to be that yes these questions are in the “halting domain” of TDT, but I also believe that understanding what that is and why these questions are legitimate and the proofs that TDT halts will be central to any resolution of these problems.
What I’m really trying to say here is that it makes sense to ask these questions, but I don’t understand why, so I think Davorak’s question was reasonable, and your answer didn’t feel complete to me. Looking back, I don’t think I’ve contributed much to this conversation. Sorry!