AlexMennen

• AlexMennen 17 Jan 2019 2:11 UTC

  5 points

  on: And My Ax­iom! In­sights from ‘Com­putabil­ity and Logic’

  On sev­eral oc­ca­sions, the au­thors em­pha­size how the in­tu­itive na­ture of “effec­tive com­putabil­ity” ren­ders fu­tile any at­tempt to for­mal­ize the the­sis. How­ever, I’m rather in­ter­ested in for­mal­iz­ing in­tu­itive con­cepts and there­fore won­dered why this hasn’t been at­tempted.

  For­mal­iz­ing the in­tu­itive no­tion of effec­tive com­putabil­ity was ex­actly what Tur­ing was try­ing to do when he in­tro­duced Tur­ing ma­chines, and Tur­ing’s the­sis claims that his at­tempt was suc­cess­ful. If you come up with a new for­mal­iza­tion of effec­tive com­putabil­ity and prove it equiv­a­lent to Tur­ing com­putabil­ity, then in or­der to use this as a proof of Tur­ing’s the­sis, you would need to ar­gue that your new for­mal­iza­tion is cor­rect. But such an ar­gu­ment would in­evitably be in­for­mal, since it links a for­mal con­cept to an in­for­mal con­cept, and there already have been in­for­mal ar­gu­ments for Tur­ing’s the­sis, so I don’t think there is any­thing re­ally fun­da­men­tal to be gained from this.

• AlexMennen 17 Jan 2019 1:57 UTC

  4 points

  on: And My Ax­iom! In­sights from ‘Com­putabil­ity and Logic’

  Con­sider the halt­ing set; … is not enu­mer­able /​ com­putable.
  …
  Here, we should be care­ful with how we in­ter­pret “in­for­ma­tion”. After all, coNP-com­plete prob­lems are triv­ially Cook re­ducible to their NP-com­plete coun­ter­parts (e.g., query the or­a­cle and then negate the out­put), but many be­lieve that there isn’t a cor­re­spond­ing Karp re­duc­tion (where we do a polyno­mial amount of com­pu­ta­tion be­fore query­ing the or­a­cle and re­turn­ing its an­swer). Since we aren’t con­sid­er­ing com­plex­ity but in­stead whether it’s enu­mer­able at all, com­ple­men­ta­tion is fine.

  You’re us­ing the word “enu­mer­able” in a non­stan­dard way here, which might in­di­cate that you’ve missed some­thing (and if not, then per­haps at least this will be use­ful for some­one else read­ing this). “Enu­mer­able” is not usu­ally used as a syn­onym for com­putable. A set is com­putable if there is a pro­gram that de­ter­mines whether or not its in­put is in the set. But a set is enu­mer­able if there is a pro­gram that halts if its in­put is in the set, and does not halt oth­er­wise. Every com­putable set is enu­mer­able (since you can just use the out­put of the com­pu­ta­tion to de­cide whether or not to halt). But the halt­ing set is an ex­am­ple of a set that is enu­mer­able but not com­putable (it is enu­mer­able be­cause you can just run the pro­gram coded by your in­put, and halt if/​when it halts). Enu­mer­able sets are not closed un­der com­ple­men­ta­tion; in fact, an enu­mer­able set whose com­ple­ment is enu­mer­able is com­putable (be­cause you can run the pro­grams for the set and its com­ple­ment in par­allel on the same in­put; even­tu­ally one of them will halt, which will tell you whether or not the in­put is in the set).

  The dis­tinc­tion be­tween Cook and Karp re­duc­tions re­mains mean­ingful when “polyno­mial-time” is re­placed by “Tur­ing com­putable” in the defi­ni­tions. Any set that an enu­mer­able set is Tur­ing-Karp re­ducible to is also enu­mer­able, but an enu­mer­able set is Tur­ing-Cook re­ducible to its com­ple­ment.

  The rea­son “enu­mer­able” is used for this con­cept is that a set is enu­mer­able iff there is a pro­gram com­put­ing a se­quence that enu­mer­ates ev­ery el­e­ment of the set. Given a pro­gram that halts on ex­actly the el­e­ments of a given set, you can con­struct an enu­mer­a­tion of the set by run­ning your pro­gram on ev­ery in­put in par­allel, and adding an el­e­ment to the end of your se­quence when­ever the pro­gram halts on that in­put. Con­versely, given an enu­mer­a­tion of a set, you can con­struct a pro­gram that halts on el­e­ments of the set by go­ing through the se­quence and halt­ing when­ever you find your in­put.

• AlexMennen 18 Dec 2018 7:33 UTC

  2 points

  in reply to: Chris_Leong's comment on: An Ex­ten­sive Cat­e­gori­sa­tion of In­finite Paradoxes

  I don’t fol­low the anal­ogy to 1/​x be­ing a par­tial func­tion that you’re get­ting at.

  Maybe a bet­ter way to ex­plain what I’m get­ting at is that it’s re­ally the same is­sue that I pointed out for the two-en­velopes prob­lem, where you know the amount of money in each en­velope is finite, but the uniform dis­tri­bu­tion up to an in­finite sur­real would sug­gest that the prob­a­bil­ity that the amount of money is finite is in­finites­i­mal. Sup­pose you say that the size of the ray $[0,\infty )$ is an in­finite sur­real num­ber $n$. The size of the por­tion of this ray that is dis­tance at least $r$ from $0$ is $n-r$ when $r$ is a pos­i­tive real, so pre­sum­ably you would also want this to be so for sur­real $r$. But us­ing, say, $r:=\sqrt{n}$, ev­ery point in $[0,\infty )$ is within dis­tance $\sqrt{n}$ of $0$, but this rule would say that the mea­sure of the por­tion of the ray that is farther than $\sqrt{n}$ from $0$ is $n-\sqrt{n}$; that is, al­most all of the mea­sure of $[0,\infty )$ is con­cen­trated on the empty set.

• AlexMennen 16 Dec 2018 19:29 UTC

  3 points

  in reply to: Lanrian's comment on: An Ex­ten­sive Cat­e­gori­sa­tion of In­finite Paradoxes

  The lat­ter. It doesn’t even make sense to speak of max­i­miz­ing the ex­pec­ta­tion of an un­bounded util­ity func­tion, be­cause un­bounded func­tions don’t even have ex­pec­ta­tions with re­spect to all prob­a­bil­ity dis­tri­bu­tions.

  There is a way out of this that you could take, which is to only in­sist that the util­ity func­tion has to have an ex­pec­ta­tion with re­spect to prob­a­bil­ity dis­tri­bu­tions in some re­stricted class, if you know your op­tions are all go­ing to be from that re­stricted class. I don’t find this very satis­fy­ing, but it works. And it offers its own solu­tion to Pas­cal’s mug­ging, by in­sist­ing that any out­come whose util­ity is on the scale of 3^^^3 has prior prob­a­bil­ity on the scale of 1/​(3^^^3) or lower.

• AlexMennen 16 Dec 2018 19:18 UTC

  5 points

  in reply to: Chris_Leong's comment on: An Ex­ten­sive Cat­e­gori­sa­tion of In­finite Paradoxes

  It’s a bad bul­let to bite. Its sym­me­tries are es­sen­tial to what makes Eu­clidean space in­ter­est­ing.

  And here’s an­other one: are you not both­ered by the lack of countable ad­di­tivity? Sup­pose you say that the vol­ume of Eu­clidean space is some sur­real num­ber $n$. Eu­clidean space is the union of an in­creas­ing se­quence of balls. The vol­umes of these balls are all finite, in par­tic­u­lar, less than $\frac{n}{2}$, so how can you jus­tify say­ing that their union has vol­ume greater than $\frac{n}{2}$?

• AlexMennen 15 Dec 2018 19:46 UTC

  2 points

  in reply to: Chris_Leong's comment on: An Ex­ten­sive Cat­e­gori­sa­tion of In­finite Paradoxes

  Why? Plain se­quences are a perfectly nat­u­ral ob­ject of study. I’ll echo gjm’s crit­i­cism that you seem to be try­ing to “re­solve” para­doxes by chang­ing the defi­ni­tions of the words peo­ple use so that they re­fer to un­nat­u­ral con­cepts that have been ger­ry­man­dered to fit your solu­tion, while re­fus­ing to talk about the nat­u­ral con­cepts that peo­ple ac­tu­ally care about.

  I don’t think think your pro­posal is a good one for in­dexed se­quences ei­ther. It is pretty weird that shift­ing the in­dices of your se­quence over by 1 could change the size of the se­quence.

• AlexMennen 15 Dec 2018 19:04 UTC

  2 points

  in reply to: Chris_Leong's comment on: An Ex­ten­sive Cat­e­gori­sa­tion of In­finite Paradoxes

  What about ro­ta­tions, and the fact that we’re talk­ing about de­stroy­ing a bunch of sym­me­try of the plane?

• AlexMennen 15 Dec 2018 17:11 UTC

  2 points

  in reply to: Chris_Leong's comment on: An Ex­ten­sive Cat­e­gori­sa­tion of In­finite Paradoxes

  There are mea­surable sets whose vol­umes will not be pre­served if you try to mea­sure them with sur­real num­bers. For ex­am­ple, con­sider $[0,\infty )\subseteq R$. Say its mea­sure is some in­finite sur­real num­ber $n$. The vol­ume-pre­serv­ing left-shift op­er­a­tion $x\mapsto x-1$ sends $[0,\infty )$ to $[-1,\infty )$, which has mea­sure $1+n$, since $[-1,0)$ has mea­sure $1$. You can do es­sen­tially the same thing in higher di­men­sions, and the shift op­er­a­tion in two di­men­sions ($(x,y)\mapsto (x-1,y)$) can be ex­pressed as the com­po­si­tion of two ro­ta­tions, so ro­ta­tions can’t be vol­ume-pre­serv­ing ei­ther. And since differ­ent ro­ta­tions will have to fail to pre­serve vol­umes in differ­ent ways, this will break sym­me­tries of the plane.

  I wouldn’t say that vol­ume-pre­serv­ing trans­for­ma­tions fail to pre­serve vol­ume on non-mea­surable sets, just that non-mea­surable sets don’t even have mea­sures that could be pre­served or not pre­served. Failing to pre­serve mea­sures of sets that you have as­signed mea­sures to is en­tirely differ­ent. Non-mea­surable sets also don’t arise in math­e­mat­i­cal prac­tice; half-spaces do. I’m also skep­ti­cal of the ex­is­tence of non-mea­surable sets, but the non-ex­is­tence of non-mea­surable sets is a far bolder claim than any­thing else I’ve said here.

• AlexMennen 15 Dec 2018 2:05 UTC

  2 points

  in reply to: Chris_Leong's comment on: An Ex­ten­sive Cat­e­gori­sa­tion of In­finite Paradoxes

  In­deed Pas­cal’s Mug­ging type is­sues are already pre­sent with the more stan­dard in­fini­ties.

  Right, in­finity of any kind (sur­real or oth­er­wise) doesn’t be­long in de­ci­sion the­ory.

  “Sur­real num­bers are not the right tool for mea­sur­ing the vol­ume of Eu­clidean space or the du­ra­tion of for­ever”—why?

  How would you? If you do some­thing like tak­ing an in­creas­ing se­quence of bounded sub­sets that fill up the space you’re try­ing to mea­sure, find a for­mula f(n) for the vol­ume of the nth sub­set, and plug in $f\left(\omega \right)$, the re­sult will be highly de­pen­dent on which in­creas­ing se­quence of bounded sub­sets you use. Did you have a differ­ent pro­posal? It’s sort of hard to ex­plain why no method for mea­sur­ing vol­umes us­ing sur­real num­bers can pos­si­bly work well, though I am con­fi­dent it is true. At the very least, vol­ume-pre­serv­ing trans­for­ma­tions like shift­ing ev­ery­thing 1 me­ter to the left or ro­tat­ing ev­ery­thing around some axis cease to be vol­ume-pre­serv­ing, though I don’t know if you’d find this con­vinc­ing.

• AlexMennen 15 Dec 2018 1:39 UTC

  4 points

  in reply to: Chris_Leong's comment on: An Ex­ten­sive Cat­e­gori­sa­tion of In­finite Paradoxes

  You want to con­ceive of this prob­lem as “a se­quence whose or­der-type is ω“, but from the sur­real per­spec­tive this lacks re­s­olu­tion. Is the num­ber of el­e­ments (sur­real) ω, ω+1 or ω+1000? All of these are pos­si­ble given that in the or­di­nals 1+ω=ω so we can add ar­bi­trar­ily many num­bers to the start of a se­quence with­out chang­ing its or­der type.

  It seems to me that mea­sur­ing the lengths of se­quences with sur­re­als rather than or­di­nals is in­tro­duc­ing fake re­s­olu­tion that shouldn’t be there. If you start with an in­finite con­stant se­quence 1,1,1,1,1,1,..., and tell me the se­quence has size $\omega$, and then you add an­other 1 to the be­gin­ning to get 1,1,1,1,1,1,1,..., and you tell me the new se­quence has size $\omega +1$, I’ll be like “uh, but those are the same se­quence, though. How can they have differ­ent sizes?”

• AlexMennen 14 Dec 2018 20:50 UTC

  14 points

  on: An Ex­ten­sive Cat­e­gori­sa­tion of In­finite Paradoxes

  Sur­real num­bers are use­less for all of these para­doxes.

  In­fini­tar­ian paral­y­sis: Us­ing sur­real-val­ued util­ities cre­ates more in­fini­tar­ian paral­y­sis than it solves, I think. You’ll never take an op­por­tu­nity to in­crease util­ity by $x$ be­cause it will always have higher ex­pected util­ity to fo­cus all of your at­ten­tion on try­ing to find ways to in­crease util­ity by $>\omega x$, since there’s some (how­ever small) prob­a­bil­ity $p>0$ that such efforts would suc­ceed, so the ex­pected util­ity of fo­cus­ing your efforts on look­ing for ways to in­crease util­ity by $>\omega x$ will have ex­pected util­ity $>p\omega x$, which is higher than $x$. I think a bet­ter solu­tion would be to note that for any per­son, a nonzero frac­tion of peo­ple are close enough to iden­ti­cal to that per­son that they will make the same de­ci­sions, so any de­ci­sion that any­one makes af­fects a nonzero frac­tion of peo­ple. Mea­sure the­ory is prob­a­bly a bet­ter frame­work than sur­real num­bers for for­mal­iz­ing what is meant by “frac­tion” here.

  Para­dox of the gods: The in­tro­duc­tion of sur­real num­bers solves noth­ing. Why wouldn’t he be able to ad­vance more than $2^{-\omega }$ miles if no gods erect any bar­ri­ers un­til he ad­vances $2^{-n}$ miles for some finite $n$?

  Two-en­velopes para­dox: it doesn’t make sense to model your un­cer­tainty over how much money is in the first en­velope with a uniform sur­real-val­ued prob­a­bil­ity dis­tri­bu­tion on $[\frac{1}{n},n]$ for an in­finite sur­real $n$, be­cause then the prob­a­bil­ity that there is a finite amount of money in the en­velope is in­finites­i­mal, but we’re try­ing to model the situ­a­tion in which we know there’s a finite amount of money in the en­velope and just have no idea which finite amount.

  Sphere of suffer­ing: Sur­real num­bers are not the right tool for mea­sur­ing the vol­ume of Eu­clidean space or the du­ra­tion of for­ever.

  Hilbert ho­tel: As you men­tioned, us­ing sur­re­als in the way you pro­pose changes the prob­lem.

  Trumped, Trou­ble in St. Peters­burg, Soc­cer teams, Can God choose an in­te­ger at ran­dom?, The Headache: Us­ing sur­re­als in the way you pro­pose in each of these changes the prob­lems in ex­actly the same way it does for the Hilbert ho­tel.

  St. Peters­burg para­dox: If you pay in­finity dol­lars to play the game, then you lose in­finity dol­lars with prob­a­bil­ity 1. Doesn’t sound like a great deal.

  Banach-Tarski Para­dox: The free group only con­sists of se­quences of finite length.

  The Magic Dart­board: First, a nit­pick: that proof re­lies on the con­tinuum hy­poth­e­sis, which is in­de­pen­dent of ZFC. Aside from that, the proof is cor­rect, which means any re­s­olu­tion along the lines you’re imag­in­ing that im­ply that no magic dart­boards ex­ist is go­ing to im­ply that the con­tinuum hy­poth­e­sis is false. Worse, the fact that for any countable or­di­nal, there are countably many smaller countable or­di­nals and un­countably many larger countable or­di­nals fol­lows from very min­i­mal math­e­mat­i­cal as­sump­tions, and is of­ten used in de­scrip­tive set the­ory with­out bring­ing in the con­tinuum hy­poth­e­sis at all, so if you start try­ing to change math to make sense of “the sec­ond half of the countable or­di­nals”, you’re go­ing to have a bad time.

  Par­ity para­doxes: The lengths of the se­quences in­volved here are the or­di­nal $\omega$, not a sur­real num­ber. You might ob­ject that there is also a sur­real num­ber called $\omega$, but this is differ­ent from the or­di­nal $\omega$. Arith­metic op­er­a­tions act differ­ently on or­di­nals than they do on the copies of those or­di­nals in the sur­real num­bers, so there’s no rea­son­able sense in which the sur­re­als con­tain the or­di­nals. Ex­am­ple: if you add an­other el­e­ment to the be­gin­ning of ei­ther se­quence (i.e. flip the switch at $t=-2$, or add a $-1$ at the be­gin­ning of the sum, re­spec­tively), then you’ve added one thing, so the sur­real num­ber should in­crease by $1$, but the or­der-type is un­changed, so the or­di­nal re­mains the same.

When wish­ful think­ing works

• AlexMennen 21 Aug 2018 21:11 UTC

  2 points

  AF

  in reply to: Vanessa Kosoy's comment on: Safely and use­fully spec­tat­ing on AIs op­ti­miz­ing over toy worlds

  The agent could be pro­grammed to have a cer­tain hard-coded on­tol­ogy rather than search­ing through all pos­si­ble hy­pothe­ses weighted by de­scrip­tion length.

• AlexMennen 15 Aug 2018 20:53 UTC

  2 points

  in reply to: capybaralet's comment on: Safely and use­fully spec­tat­ing on AIs op­ti­miz­ing over toy worlds

  I haven’t heard the term “pla­tonic goals” be­fore. There’s been plenty writ­ten on ca­pa­bil­ity con­trol be­fore, but I don’t know of any­thing writ­ten be­fore on the strat­egy I de­scribed in this post (al­though it’s en­tirely pos­si­ble that there’s been pre­vi­ous writ­ing on the topic that I’m not aware of).

• AlexMennen 9 Aug 2018 0:17 UTC

  2 points

  AF

  in reply to: G Gordon Worley III's comment on: Safely and use­fully spec­tat­ing on AIs op­ti­miz­ing over toy worlds

  Are you wor­ried about leaks from the ab­stract com­pu­ta­tional pro­cess into the real world, leaks from the real world into the ab­stract com­pu­ta­tional pro­cess, or both? (Or maybe nei­ther and I’m mi­s­un­der­stand­ing your con­cern?)

  There will definitely be tons of leaks from the ab­stract com­pu­ta­tional pro­cess into the real world; just look­ing at the re­sult is already such a leak. The point is that the AI should have no in­cen­tive to op­ti­mize such leaks, not that the leaks don’t ex­ist, so the ex­is­tence of ad­di­tional leaks that we didn’t know about shouldn’t be con­cern­ing.

  Leaks from the out­side world into the com­pu­ta­tional ab­strac­tion would be more con­cern­ing, since the whole point is to pre­vent those from ex­ist­ing. It seems like it should be pos­si­ble to make hard­ware ar­bi­trar­ily re­li­able by de­vot­ing enough re­sources to er­ror de­tec­tion and cor­rec­tion, which would pre­vent such leaks, though I’m not an ex­pert, so it would be good to know if this is wrong. There may be other ways to get the AI to act similarly to the way it would in the ideal­ized toy world even when hard­ware er­rors cre­ate small differ­ences. This is cer­tainly the sort of thing we would want to take se­ri­ously if hard­ware can’t be made ar­bi­trar­ily re­li­able.

  In­ci­den­tally, that story about ac­ci­den­tal cre­ation of a ra­dio with an evolu­tion­ary al­gorithm was part of what mo­ti­vated my post in the first place. If the evolu­tion­ary al­gorithm had used tests of its os­cilla­tor de­sign in a com­puter model, rather than in the real world, then it would have have built a ra­dio re­ceiver, since ra­dio sig­nals from nearby com­put­ers would not have been in­cluded in the com­puter model of the en­vi­ron­ment, even though they were pre­sent in the ac­tual en­vi­ron­ment.

• AlexMennen 8 Aug 2018 0:17 UTC

  2 points

  AF

  in reply to: Diffractor's comment on: Prob­a­bil­is­tic Tiling (Pre­limi­nary At­tempt)

  What I meant was that the com­pu­ta­tion isn’t ex­tremely long in the sense of de­scrip­tion length, not in the sense of com­pu­ta­tion time. Also, we aren’t do­ing policy search over the set of all tur­ing ma­chines, we’re do­ing policy search over some smaller set of poli­cies that can be guaran­teed to halt in a rea­son­able time (and more can be added as time goes on)

  Wouldn’t the set of all ac­tion se­quences have lower de­scrip­tion length than some large finite set of poli­cies? There’s also the po­ten­tial prob­lem that all of the poli­cies in the large finite set you’re search­ing over could be quite far from op­ti­mal.

• AlexMennen 7 Aug 2018 23:47 UTC

  2 points

  AF

  in reply to: Diffractor's comment on: Prob­a­bil­is­tic Tiling (Pre­limi­nary At­tempt)

  Ok, un­der­stood on the sec­ond as­sump­tion.$U$ is not a func­tion to $[0,1]$, but a func­tion to the set of $[0,1]$-val­ued ran­dom vari­ables, and your as­sump­tion is that this ran­dom vari­able is un­cor­re­lated with cer­tain claims about the out­puts of cer­tain poli­cies. The in­tu­itive ex­pla­na­tion of the third con­di­tion made sense; my com­plaint was that even with the in­tended in­ter­pre­ta­tion at hand, the for­mal state­ment made no sense to me.

  I’m pretty sure you’re as­sum­ing that $\varphi$ is re­solved on day $n$, not that it is re­solved even­tu­ally.

  Search­ing over the set of all Tur­ing ma­chines won’t halt in a rea­son­ably short amount of time, and in fact won’t halt ever, since the set of all Tur­ing ma­chines is non-com­pact. So I don’t see what you mean when you say that the com­pu­ta­tion is not ex­tremely long.

• AlexMennen 7 Aug 2018 23:16 UTC

  2 points

  AF

  in reply to: rohinmshah's comment on: Safely and use­fully spec­tat­ing on AIs op­ti­miz­ing over toy worlds

  This model seems very fatal­is­tic, I guess? It seems some­what in­com­pat­i­ble with an agent that has prefer­ences. (Per­haps you’re sug­gest­ing we build an AI with­out prefer­ences, but it doesn’t sound like that.)

  Ok, here’s an­other at­tempt to ex­plain what I meant. Some­where in the pla­tonic realm of ab­stract math­e­mat­i­cal struc­tures, there is a small world with physics quite a lot like ours, con­tain­ing an AI run­ning on some ideal­ized com­pu­ta­tional hard­ware, and try­ing to ar­range the rest of the small world so that it has some de­sired prop­erty. Hu­mans simu­late this pro­cess so they can see what the AI does in the small world, and copy what it does. The AI could try mess­ing with us spec­ta­tors, so that we end up giv­ing more com­pute to the phys­i­cal in­stan­ti­a­tion of the AI in the hu­man world (which is differ­ent from the AI in the pla­tonic math­e­mat­i­cal struc­ture), which the phys­i­cal in­stan­ti­a­tion of the AI in the hu­man world can use to bet­ter ma­nipu­late the simu­la­tion of the toy world that we are run­ning in the hu­man world (which is also differ­ent from the pla­tonic math­e­mat­i­cal struc­ture). The pla­tonic math­e­mat­i­cal struc­ture it­self does not have a hu­man world with ex­tra com­pute in it that can be grabbed, so try­ing to mess with hu­man spec­ta­tors would, in the pla­tonic math­e­mat­i­cal struc­ture, just end up be­ing a waste of com­pute, so this strat­egy will be dis­carded if it some­how gets con­sid­ered in the first place. Thus a real-world simu­la­tion of this AI-in-a-pla­tonic-math­e­mat­i­cal-struc­ture will, if ac­cu­rate, be­have in the same way.

• AlexMennen 7 Aug 2018 22:57 UTC

  2 points

  AF

  in reply to: Raemon's comment on: Prob­a­bil­is­tic Tiling (Pre­limi­nary At­tempt)

  Thanks, fixed.

• AlexMennen 7 Aug 2018 22:50 UTC

  4 points

  AF

  on: Prob­a­bil­is­tic Tiling (Pre­limi­nary At­tempt)

  I sug­gest stat­ing the re­sult you’re prov­ing be­fore giv­ing the proof.

  You have some un­usual no­ta­tion that I think makes some of this un­nec­es­sar­ily con­fus­ing. In­stead of this un­der­lined vs non-un­der­lined thing, you should have differ­ent func­tions $U:A^{\omega }\to [0,1]$$ and $U_{a_{st}^{1:n-1}}:A\times \Pi \to [0,1]$, where the first maps ac­tion se­quences to util­ities, and the sec­ond maps a pair con­sist­ing of an ac­tion $x$ and a fu­ture policy $\pi$ to the util­ity of the ac­tion se­quence be­gin­ning with $a_{st}^{1:n-1}$, fol­lowed by $x$, fol­lowed by the ac­tion se­quence gen­er­ated by $\pi$. Your first as­sump­tion would then be stated $U_{a_{st}^{1:n-1}}(x,\pi )=U(a_{st}^{1:n-1},x,a_{\pi }^{1:\infty })$. Your sec­ond as­sump­tion (fair­ness of the en­vi­ron­ment) is im­plicit in the type sig­na­ture of the util­ity func­tion $U:A^{\omega }\to [0,1]$. If your util­ity de­pends on some­thing other than the ac­tion se­quence, then it doesn’t make sense to write it as a func­tion of the ac­tion se­quence. It’s good to point out as­sump­tions that are im­plicit in the for­mal­ism you’re us­ing, but by the time you iden­tify util­ity as a func­tion of ac­tion se­quences, you don’t need to as­sume fair­ness of the en­vi­ron­ment as an ad­di­tional ax­iom. I do not un­der­stand what your third as­sump­tion is.

  This is em­phat­i­cally false in gen­eral, but there’s a spe­cial con­di­tion that makes it vi­able, namely that the dis­tri­bu­tion at time n is guaran­teed to as­sign prob­a­bil­ity 1 to $\varphi$ iff $\varphi$. My epistemic state about this is “this seems ex­tremely plau­si­ble, but I don’t know for sure if log­i­cal in­duc­tors at­tain this prop­erty in the limit”

  They don’t. For in­stance, let $\varphi$ be any true un­de­cid­able sen­tence. The log­i­cal in­duc­tor does not as­sign prob­a­bil­ity 1 to $\varphi$ even in the limit. Your fourth as­sump­tion does not seem rea­son­able. Does $E_{n-1}\left(E_n\right(U|\varphi \left)\right)=E_{n-1}\left(U|\varphi \right)$ not give you what you want?

  Note that this only ex­plic­itly writes the start­ing code, and the code that might be mod­ified to, not the past or fu­ture ac­tion se­quence! This is im­por­tant for the agent to be able to rea­son about this com­pu­ta­tion, de­spite it tak­ing an in­finite in­put.

  I think this is ex­actly back­wards. The prop­erty that makes spaces easy to search through and rea­son about is com­pact­ness, not finite­ness. If $A$ is finite, then $A^{\omega }$ is com­pact, and thus easy to search through and rea­son about, pro­vided the rele­vant func­tions on it are con­tin­u­ous. But the space of com­puter pro­grams is an in­finite dis­crete space, hence non-com­pact, and hard to search through and rea­son about, ex­cept by re­mem­ber­ing that the pur­pose of se­lect­ing a pro­gram is so that it will gen­er­ate an el­e­ment of the nice, eas­ily-search­able com­pact space of ac­tion se­quences.