Comparing LICDT and LIEDT

At­tempted ver­sions of CDT and EDT can be con­structed us­ing log­i­cal in­duc­tors, called LICDT and LIEDT. It is shown, how­ever, that LICDT fails XOR Black­mail, and LIEDT fails New­comb. One in­ter­pre­ta­tion of this is that LICDT and LIEDT do not im­ple­ment CDT and EDT very well. I ar­gue that they are in­deed forms of CDT and EDT, but stray from ex­pec­ta­tions be­cause they also im­ple­ment the rat­ifi­a­bil­ity con­di­tion I dis­cussed pre­vi­ously. Con­tin­u­ing the line of think­ing from that post, I dis­cuss con­di­tions in which LICDT=LIEDT, and try to draw out broader im­pli­ca­tions for de­ci­sion the­ory.

Thanks to Scott and Sam for dis­cus­sions shap­ing this post. Also thanks to many par­ti­ci­pants at AISFP for dis­cus­sions shap­ing my cur­rent view of coun­ter­fac­tu­als.

I’m not sure who gets credit for LICDT and LIEDT, but they’ve been dis­cussed around MIRI since shortly af­ter log­i­cal in­duc­tion it­self. LIEDT was sort of the ob­vi­ous first thing to try; LICDT is a slight vari­a­tion. (Scott thinks Jes­sica may have come up with LICDT.) They might be thought of as the punch­ing bag for bet­ter log­i­cal in­duc­tion DTs to be con­trasted with (al­though, Tsvi wrote up a likely-bet­ter baseline pro­posal).

Both LICDT and LIEDT use a log­i­cal in­duc­tor which has been run for steps, . I’ll ab­bre­vi­ate an agent as (pa­ram­e­ter­iz­ing by the same as for the in­duc­tor), with to say that the agent takes ac­tion from some ac­tion set . We can define self-refer­en­tial sen­tences . Both LICDT and LIEDT ex­plore when such sen­tences are true. We can take whichever ac­tion the agent least ex­pects it­self to do con­di­tioned on its ex­plor­ing. This forces the agent to take ev­ery ac­tion with fre­quency at least in the limit, and also makes the ex­plo­ra­tion pseu­do­ran­dom in the sense that the log­i­cal in­duc­tor can­not pre­dict it much bet­ter than to as­sign prob­a­bil­ity to ex­plo­ra­tion (and there­fore, nei­ther can any poly-time com­putable pre­dic­tor).

When it isn’t tak­ing an ac­tion due to the ex­plo­ra­tion clause, LIEDT chooses ac­tions based on the ex­pected util­ity con­di­tion­ing on each ac­tion. Utility is defined as a log­i­cally un­cer­tain vari­able (LUV), in the ter­minol­ogy of the log­i­cal in­duc­tion pa­per. Let be the LUV for the util­ity of , and be the con­di­tional ex­pec­ta­tion of in given that the agent takes ac­tion . The con­di­tional ex­pec­ta­tion is always well-defined thanks to the ex­plo­ra­tion, which en­sures that the prob­a­bil­ity of each ac­tion re­mains above zero.

LICDT is similar, but rather than tak­ing the ex­pec­ta­tion con­di­tioned on each ac­tion, it takes the ex­pec­ta­tion con­di­tioned on ex­plor­ing and tak­ing that ac­tion. Judg­ing ac­tions by what would hap­pen if you took those ac­tions ran­domly, rather than re­li­ably, is sup­posed to re­move the kind of cor­re­la­tion which makes EDT co­op­er­ate in pris­oner’s dilemma, one-box in New­comb, et cetera. We will see that this only party works.

Both LICDT and LIEDT in­clude any ob­ser­va­tions in their de­duc­tive state. (There can be spe­cial pred­i­cates rep­re­sent­ing sen­sory states.) So, they are up­date­ful de­ci­sion the­o­ries.

LICDT and LIEDT aren’t very differ­ent, and mostly we just talk about LIEDT, call­ing it LIDT. How­ever, I’m re­cently re­al­iz­ing just how similar LICDT and LIEDT re­ally are.

LIEDT two-boxes in New­comb.

Sup­pose we have an LIEDT agent fac­ing New­comb’s prob­lem. We can spec­ify a se­quence of New­comb prob­lems (for log­i­cal in­duc­tors of in­creas­ing power) by the util­ity func­tion , where is the propo­si­tion stat­ing that the agent (of power ) one-boxes, and is the in­di­ca­tor func­tion which re­turns 1 for true propo­si­tions and 0 for false. This is a New­comb prob­lem where Omega is fal­lible; in fact, Omega can only pre­dict the agent as well as the agent can pre­dict it­self, since both use the same log­i­cal in­duc­tor. (And, New­comb deals with the un­cer­tainty by putting the money in the box with prob­a­bil­ity equal to its es­ti­ma­tion of the prob­a­bil­ity LIEDT one-boxes.) The best re­ward the agent can get is if Omega pre­dicts one-box­ing, but the agent un­ex­pect­edly two-boxes. Of course, a log­i­cal in­duc­tor can’t be fooled like this re­li­ably; so the agent is in­cen­tivised to one-box.

The­o­rem. LIEDT con­verges to two-box on non-ex­plo­ra­tion rounds as in­creases.

Proof. The log­i­cal in­duc­tor comes to pre­dict and with in­creas­ing ac­cu­racy as in­creases, since it has ac­cess to , and since the con­di­tion­ing is always well-defined thanks to ex­plo­ra­tion. There­fore, two-box­ing even­tu­ally be­comes the most ap­peal­ing op­tion.

So, LIEDT does not come to see Omega as cor­re­lated with its ac­tion, be­cause it knows its own gen­eral policy, and the gen­eral policy screens off all the cor­re­la­tion be­tween Omega and its ac­tion.

Now, it’s true that if Omega was a more pow­er­ful pre­dic­tor than the agent, LIEDT could one-box—but, so could LICDT. In par­tic­u­lar, if Omega sim­ply knows the ac­tion pre­cisely, then , and both LICDT and LIEDT one-box.

LICDT is XOR-black­mailed.

On the other hand, con­sider the XOR Black­mail let­ter, which is sup­posed to be a case where CDT does bet­ter than EDT. There is a difficult-to-pre­dict dis­aster, , with pseu­do­ran­dom prob­a­bil­ity 0.01. How­ever, an AI re­searcher can pre­dict both the dis­aster and the AI, and will use that knowl­edge to try and ex­tract money from the AI. Let’s call the AI send­ing money to the re­searcher , and not send­ing money . The AI re­searcher sends a let­ter ask­ing for money if and only if [they pre­dict the AI will re­spond by send­ing money XOR ]. Let’s say the AI re­searcher asks for half the cost of the dis­aster. . More­over, the de­duc­tive state in­cludes knowl­edge of the let­ter, .

The­o­rem. LICDT con­verges to send­ing the black­mailer money when a let­ter is re­ceived, on non-ex­plo­ra­tion rounds.

Proof. LICDT bases its de­ci­sion on the util­ity ob­served in ex­plo­ra­tion rounds. Con­di­tional on its re­ceiv­ing the let­ter and ex­plor­ing into send­ing the money, no dis­aster has oc­curred. Con­di­tional on its re­ceiv­ing the let­ter and ex­plor­ing into not send­ing money, the dis­aster has oc­curred. It will come to pre­dict both of these things ac­cu­rately, and its con­di­tional ex­pec­ta­tions will be con­sis­tent with them. There­fore, it will send the money.

In­ter­pre­ta­tion of the two ex­per­i­ments.

It ap­pears that these aren’t very good im­ple­men­ta­tions of CDT and EDT. The at­tempted CDT fails black­mail let­ter; the at­tempted EDT fails New­comb. But, if we look a lit­tle closer, some­thing more in­ter­est­ing is go­ing on. I didn’t prove it here, but both of them will one-box when Omega is a perfect pre­dic­tor, and two-box when Omega is fal­lible. Both of them will send the black­mail let­ter when the black­mailer is a perfect pre­dic­tor, and re­fuse when the black­mailer is fal­lible. They ap­pear to be fol­low­ing my “Law of Log­i­cal Causal­ity” from SLS III.

When peo­ple ar­gue that EDT one-boxes in New­comb and that CDT two-boxes, and that EDT sends the money in XOR Black­mail but EDT ab­stains, they of­ten aren’t care­ful that EDT and CDT are be­ing given the same prob­lem. CDT is sup­posed to be tak­ing a phys­i­cal-cau­sa­tion coun­ter­fac­tual, mean­ing it rep­re­sents the prob­lem in a Bayesian net­work rep­re­sent­ing its phys­i­cal un­cer­tainty, in which the di­rec­tion of links lines up with phys­i­cal causal­ity. If we give EDT the same Bayesian net­work, it will dis­re­gard the causal in­for­ma­tion con­tained therein, and com­pute con­di­tional util­ities of ac­tions. But, it is un­clear that EDT will then one-box in New­comb. Rea­son­ing about the phys­i­cal situ­a­tion, will it re­ally con­clude that con­di­tion­ing on one ac­tion or an­other changes the ex­pected pre­dic­tion of Omega? How does the con­di­tional prob­a­bil­ity flow from the ac­tion to Omega? Omega’s pre­dic­tion is based on some ob­ser­va­tions made in the past. It may be that the agent knows equally well what those ob­ser­va­tions were; it just doesn’t know ex­actly what Omega con­cluded from them. The knowl­edge of the ob­ser­va­tions screens off any prob­a­bil­is­tic re­la­tion­ship. Or, even worse, it may be that the phys­i­cal in­for­ma­tion which the agent has in­cludes its own source code. The agent can’t try to run its own source code on this very de­ci­sion; it would go into an in­finite loop. So, we get stuck when we try to do the rea­son­ing. Similar prob­lems oc­cur in XOR black­mail.

I claim that rea­son­ing about what CDT and EDT do in New­comb’s prob­lem and XOR black­mail im­plic­itly as­sume some solu­tion to log­i­cal un­cer­tainty. The cor­re­la­tion which EDT is sup­posed to con­clude ex­ists be­tween its ac­tion and the pre­dic­tor’s guess at its ac­tion is a log­i­cal cor­re­la­tion. But, log­i­cal in­duc­tion doesn’t nec­es­sar­ily re­solve this kind of log­i­cal un­cer­tainty in the in­tu­itive way.

In par­tic­u­lar, log­i­cal in­duc­tion im­ple­ments a ver­sion of the rat­ifi­a­bil­ity con­di­tion. Be­cause LIEDT agents know their own poli­cies, they are screened off from would-be cor­re­lates of their de­ci­sions in much the same way LICDT agents are. And be­cause LICDT agents are learn­ing coun­ter­fac­tu­als by ex­plo­ra­tion, they treat pre­dic­tors who have more in­for­ma­tion about their own ac­tions than they them­selves do as causally down­stream—the law of log­i­cal causal­ity which I con­jec­tured would, to­gether with rat­ifi­a­bil­ity, im­ply CDT=EDT.

When does LICDT=LIEDT?

It’s ob­vi­ous that LIEDT usu­ally equals LICDT when LIEDT con­verges to tak­ing just one of the ac­tions on non-ex­plo­ra­tion rounds; the other ac­tions are only taken when ex­plor­ing, so LIEDT’s ex­pec­ta­tion of those ac­tions just equals LICDT’s. What about the ex­pec­ta­tion of the main ac­tion? Well, it may differ, if there is a re­li­able differ­ence in util­ity when it is taken as an ex­plo­ra­tion vs de­liber­ately cho­sen. How­ever, this seems to be in some sense un­fair; the en­vi­ron­ment is bas­ing its pay­off on the agent’s rea­sons for tak­ing an ac­tion, rather than on the ac­tion alone. While we’d like to be able to deal with some such en­vi­ron­ments, al­low­ing this in gen­eral al­lows an en­vi­ron­ment to pun­ish one de­ci­sion the­ory se­lec­tively. So, for now, we rule such de­ci­sion prob­lems out:

Defi­ni­tion: De­ci­sion prob­lem. A de­ci­sion prob­lem is a func­tion which takes an agent and a step num­ber, and yields a LUV which is the pay­out.

Defi­ni­tion: Fair de­ci­sion prob­lem. A fair de­ci­sion prob­lem is a de­ci­sion prob­lem such that the same limit­ing ac­tion prob­a­bil­ities on the part of the agent im­ply the same limit­ing ex­pec­ta­tions on util­ity per ac­tion, and these ex­pec­ta­tions do not differ be­tween ex­plo­ra­tion ac­tions and plain ac­tions. For­mally: if ex­ists for all , and a sec­ond agent has limit­ing ac­tion prob­a­bil­ities which also ex­ist and are the same, then also ex­ist and are the same as the cor­re­spond­ing quan­tities for ; and fur­ther­more, ex­ist and are the same as the limits with­out .

I don’t ex­pect that this defi­ni­tion is par­tic­u­larly good; al­ter­na­tives wel­come. In par­tic­u­lar, us­ing the in­duc­tor it­self to es­ti­mate the ac­tion prob­a­bil­ity in­tro­duces an un­for­tu­nate de­pen­dence on in­duc­tor.

Com­pare to the no­tion of fair­ness in Asymp­totic DT.

Defi­ni­tion: A con­tin­u­ous fair de­ci­sion prob­lem is a fair prob­lem for which the func­tion from limit­ing ac­tion prob­a­bil­ities to limit­ing ex­pected util­ities is con­tin­u­ous.

Ob­ser­va­tion. Con­tin­u­ous fair de­ci­sion prob­lems have “equil­ibrium” ac­tion dis­tri­bu­tions, where the best re­sponse to the ac­tion util­ities which come from those is con­sis­tent with the ac­tion dis­tri­bu­tion. Th­ese are the same whether “best-re­sponse” is in the LICDT or LIEDT sense, since the ex­pected util­ity is re­quired to be the same in both senses. If ei­ther LICDT or LIEDT con­verge on some such prob­lem, then clearly they con­verge to one of these equil­ibria.

This doesn’t nec­es­sar­ily mean that LICDT and LIEDT con­verge to the same be­hav­ior, though, since it is pos­si­ble that they fail to con­verge, and that they con­verge to differ­ent equil­ibria. I would be some­what sur­prised if there is some es­sen­tial differ­ence in be­hav­ior be­tween LICDT and LIEDT on these prob­lems, but I’m not sure what con­jec­ture to state.

I’m more con­fi­dent in a con­jec­ture for a much nar­rower no­tion of fair­ness (I wasn’t able to prove this, but I wouldn’t be very sur­prised if it turned out not to be that hard to prove):

Defi­ni­tion. Deter­minis­ti­cally fair de­ci­sion prob­lem: A de­ci­sion prob­lem is de­ter­minis­ti­cally fair if the pay­out on in­stance are only a func­tion of the ac­tion prob­a­bil­ities ac­cord­ing to and of the ac­tual ac­tion taken (where is the log­i­cal in­duc­tor used by the agent it­self).

Con­jec­ture. Given a con­tin­u­ous de­ter­minis­ti­cally fair de­ci­sion prob­lem, the set of mixed strate­gies which LICDT may con­verge to and LIEDT may con­verge to, vary­ing the choice of log­i­cal in­duc­tor, are the same. That is, if LICDT con­verges to an equil­ibrium, we can find a log­i­cal in­duc­tor for which LIEDT con­verges to that same equil­ibrium, and vice versa.

This seems likely to be true, since the nar­row­ness of the de­ci­sion prob­lem class leaves very lit­tle room to wedge the two de­ci­sion the­o­ries apart.

The difficulty of prov­ing com­par­i­son the­o­rems for LICDT and LIEDT is closely re­lated to the difficulty of prov­ing op­ti­mal­ity the­o­rems for them. If we had a good char­ac­ter­i­za­tion of the con­ver­gence and op­ti­mal­ity con­di­tions of these two de­ci­sion the­o­ries, we would prob­a­bly be in a bet­ter po­si­tion to study the re­la­tion­ship be­tween them.

At least we can prove the fol­low­ing fairly bor­ing the­o­rem:

The­o­rem. For a de­ci­sion prob­lem in which the util­ity de­pends only on the ac­tion taken, in a way which does not de­pend on or on the agent, and for which all the ac­tions have differ­ent util­ities, LIEDT and LICDT will con­verge to the same dis­tri­bu­tion on ac­tions.

Proof. Ep­silon ex­plo­ra­tion en­sures that there con­tinues to be some prob­a­bil­ity of each ac­tion, so the log­i­cal in­duc­tor will even­tu­ally learn the ac­tion util­ities ar­bi­trar­ily well. Once the util­ities are ac­cu­rate enough to put the ac­tions in the right or­der­ing, the agent will sim­ply take the best ac­tion, with the ex­cep­tion of ex­plo­ra­tion rounds.

Law of Log­i­cal Counterfactuals

The in­ter­est­ing thing here is that LIEDT seems to be the same as LICDT un­der an as­sump­tion that the en­vi­ron­ment doesn’t speci­fi­cally mess with it by do­ing some­thing differ­ently on ex­plo­ra­tion rounds and non-ex­plo­ra­tion rounds. This is sort of ob­vi­ous from the defi­ni­tions of LICDT and LIEDT (de­spite the difficulty of ac­tu­ally prov­ing the re­sult). How­ever, no­tice that it’s much differ­ent from usual state­ments of the differ­ence be­tween EDT and CDT.

I claim that LIEDT and LICDT are more-or-less ap­pro­pri­ately re­flect­ing the spirit of EDT and CDT un­der (1) the con­di­tion of rat­ifi­a­bil­ity, which is en­forced by the self-knowl­edge prop­er­ties of log­i­cal in­duc­tors, and (2) the “law of log­i­cal coun­ter­fac­tu­als” (LLC) I posited last time, which is en­forced by the way LICDT learns causal­ity via ex­per­i­men­ta­tion. You can’t learn that some­thing which knows more about your ac­tion than you do is up­stream of you if you make the as­sump­tion that you can perform ran­dom­ized con­trol­led tri­als!

Since the law of log­i­cal coun­ter­fac­tu­als was vaguely stated, I had hoped to learn some­thing about what shape it has to take by ex­am­in­ing this case. Un­for­tu­nately, this case is a bit in­tractable. How­ever, it did sug­gest an ad­di­tional con­di­tion: (3) the en­vi­ron­ment’s be­hav­ior doesn’t de­pend on whether you ex­plore. (1), (2), and (3) are stated rather in­for­mally for now, but to­gether are sup­posed to im­ply CDT=EDT, in a for­mal anal­y­sis which is yet-to-be.

Ac­tu­ally, as­sump­tion (3) is a sort of “ran­dom­ized con­trol­led tri­als” as­sump­tion, which seems to jus­tify (2). You as­sume that you can ar­range for ac­tions to be un­cor­re­lated with any­thing in the world, and that jus­tifies your use of ex­plo­ra­tion to learn about coun­ter­fac­tu­als.

It’s not ob­vi­ous at first, but ex­plo­ra­tion-based coun­ter­fac­tu­als are very similar to coun­ter­fac­tu­als based on the chicken rule in proof-based de­ci­sion the­o­ries such as MUDT. The chicken rule re­quires that if you can prove what your own ac­tion will be, you take a differ­ent ac­tion. This al­lows the proofs from al­ter­na­tive ac­tions to be well-be­haved, rather than ex­plod­ing in con­tra­dic­tion.

You can see how that’s analo­gous to the way ep­silon-ex­plo­ra­tion makes sure that LICDT and LIEDT can con­di­tion on their own ac­tions with­out di­vid­ing by zero. It’s also analo­gous for a deeper rea­son. Re­mem­ber the trick of us­ing self-refer­en­tial sen­tences for ex­plo­ra­tion, at the be­gin­ning of this writeup? A very similar trick is to take any ac­tion which the log­i­cal in­duc­tor cur­rently as­signs prob­a­bil­ity . In other words, do any­thing you strongly be­lieve you won’t do. This is very close to the chicken rule; just sub­sti­tute prob­a­bil­is­tic be­lief for proof.

In fact, we can go a bit fur­ther. One of the short­com­ings of MUDT is that it doesn’t do what we’d like in the Agent Si­mu­lates Pre­dic­tor sce­nario, and a host of other prob­lems where a more pow­er­ful logic is re­quired. We can ad­dress these is­sues by giv­ing it a more pow­er­ful logic, but that does not ad­dress the in­tu­itive con­cern, that it seems as if we should be able to solve these prob­lems with­out fully trust­ing a more pow­er­ful logic: if we strongly sus­pect that the more pow­er­ful logic is con­sis­tent, we should be able to mostly do the same thing.

And in­deed, we can ac­com­plish this with log­i­cal in­duc­tion. What we do is play chicken against any­thing which seems to pre­dict our ac­tion be­yond a cer­tain tol­er­able de­gree. This gives us ex­actly the pseu­do­ran­dom ep­silon-ex­plo­ra­tion of LICDT/​LIEDT. Un­for­tu­nately, there’s a ver­sion of Agent Si­mu­lates Pre­dic­tor which trips these up as well. Alas. (Asymp­totic De­ci­sion The­ory, on the other hand, gets Agent Si­mu­lates Pre­dic­tor right; but, it is bad for other rea­sons.)

It’s in­ter­est­ing that in proof-based de­ci­sion the­ory, you never have to take the ac­tion; you just threaten to take it. (Or rather: you only take it if your logic is in­con­sis­tent.) It’s like be­ing able to learn from an ex­per­i­ment which you never perform, merely by virtue of putting your­self in a po­si­tion where you al­most do it.

Troll Bridge

Con­di­tion (3) is a sort of “no Troll Bridge”con­di­tion. The write-ups of the Troll Bridge on this fo­rum are some­what in­ad­e­quate refer­ences to make my point well (they don’t even call it Troll Bridge!), but the ba­sic idea is that you put some­thing in the en­vi­ron­ment which de­pends on the con­sis­tency of PA, in a way which makes a MUDT agent do the wrong thing via a very cu­ri­ous Löbian ar­gu­ment. There’s a ver­sion of Troll Bridge which works on the self-refer­en­tial ex­plo­ra­tion sen­tences rather than the con­sis­tency of PA. It seems like what’s go­ing on in troll bridge has a lot to do with part of the en­vi­ron­ment cor­re­lat­ing it­self with your in­ter­nal ma­chin­ery; speci­fi­cally, the in­ter­nal ma­chin­ery which en­sures that you can have coun­ter­fac­tu­als.

Troll Bridge is a coun­terex­am­ple to the idea of proof-length coun­ter­fac­tu­als. The hy­poth­e­sis be­hind proof-length coun­ter­fac­tu­als is that A is a le­gi­t­i­mate coun­ter­fac­tual con­se­quence of B if a proof of A from B is much shorter than a proof of ¬A from B. It’s in­ter­est­ing that my con­di­tion (3) rules it out like this; it sug­gests a pos­si­ble re­la­tion­ship be­tween what I’m do­ing and proof-length coun­ter­fac­tu­als. But I sus­pected such a re­la­tion­ship since be­fore writ­ing SLSIII. The con­nec­tion is this:

Proof-length coun­ter­fac­tu­als are con­sis­tent with MUDT, and with var­i­ants of MUDT based on bounded-time proof search, be­cause what the chicken rule does is put proofs of what the agent does ju­u­ust out of reach of the agent it­self. If the en­vi­ron­ment is tractable enough that there ex­ist proofs of the con­se­quences of ac­tions which the agent will be able to find, the chicken rule pushes the proofs of the agent’s own ac­tions far enough out that they won’t in­terfere with that. As a re­sult, you have to es­sen­tially step through the whole ex­e­cu­tion of the agent’s code in or­der to prove what it does, which of course the agent can’t do it­self while it’s run­ning. We can re­fine proof-length coun­ter­fac­tu­als to make an even tighter fit: given a proof search, A is a le­gi­t­i­mate coun­ter­fac­tual con­se­quence of B if the search finds a proof of A from B be­fore it finds one for ¬A.

This makes it clear that the no­tion of coun­ter­fac­tual is quite sub­jec­tive. Log­i­cal in­duc­tors ac­tu­ally make it sig­nifi­cantly less so, be­cause an LI can play chicken against all proof sys­tems; it will be more effec­tive in the short-run at play­ing chicken against its own proof sys­tem, but in the song run it learns to pre­dict the­o­rems as fast as any proof sys­tem would, so it can play chicken against them all. Nonethe­less, LIDT still plays chicken against a sub­jec­tive no­tion of pre­dictabil­ity.

And this is ob­vi­ously con­nected to my as­sump­tion (3). LIDT tries vali­antly to make (3) true by decor­re­lat­ing its ac­tions with any­thing which can pre­dict them. Sadly, as for Agent Si­mu­lates Pre­dic­tor, we can con­struct a var­i­ant of Troll Bridge which causes this to fail any­way.

In any case, this view of what ex­plo­ra­tion-based coun­ter­fac­tu­als are makes me re­gard them as sig­nifi­cantly more nat­u­ral than I think oth­ers do. Nonethe­less, the fact re­mains that nei­ther LIDT nor MUDT do all the things we’d like them to. They don’t do what we would like in multi-agent situ­a­tions. They don’t solve Agent Si­mu­lates Pre­dic­tor or Troll Bridge. It seems to me that when they fail, they fail for largely the same rea­sons, thanks to the strong anal­ogy be­tween their no­tions of coun­ter­fac­tual.

(There are some dis­analo­gies, how­ever; for one, log­i­cal in­duc­tor de­ci­sion the­o­ries have a prob­lem of se­lect­ing equil­ibria which doesn’t seem to ex­ist in proof-based de­ci­sion the­o­ries.)