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!
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!