It seems possible to generalize this OpportunisticBot idea and port it to the UDT framework (where “opponents” and “the rest of the environment” are not provided separately). I’m not sure if this leads anywhere interesting, but I better write it down before I forget.
Define UDT-OB(input) as follows: (Define “U”, “us”, “actions”, and “mappings” as in Benja’s recent post.) For each u in us in descending order, for each m in mappings, check if “UDT-OB(i) == m[i] for every i in actions.keys() AND U() >= u” is provable in PA-j, with j incrementing by 1 each time. If it is provable in PA-j, then return m[input].
This works in simple cases where “UDT-OB(i) == m[i] for every i in actions.keys() IMPLIES U() >= u” is easily provable for optimal m* and u*, because assuming PA is sound, UDT-OB will reach the step with m=m* and u=u*, and since PA-j can prove that it reaches this step, it can (using the above IMPLIES statement) prove ‘if “UDT-OB(i) == m[i] for every i in actions.keys() AND U() >= u” is provable in PA-j then UDT-OB(i) == m[i] for every i in actions.keys() AND U() >= u’.
This also works for some cases where Löbian circles are needed, provided that when each agent tries to prove the necessary statements, they are using proof systems that are strong enough to prove that both agents reach that step. I’m not sure how to arrange this in general.
It seems possible to generalize this OpportunisticBot idea and port it to the UDT framework (where “opponents” and “the rest of the environment” are not provided separately). I’m not sure if this leads anywhere interesting, but I better write it down before I forget.
Define UDT-OB(input) as follows: (Define “U”, “us”, “actions”, and “mappings” as in Benja’s recent post.) For each u in us in descending order, for each m in mappings, check if “UDT-OB(i) == m[i] for every i in actions.keys() AND U() >= u” is provable in PA-j, with j incrementing by 1 each time. If it is provable in PA-j, then return m[input].
This works in simple cases where “UDT-OB(i) == m[i] for every i in actions.keys() IMPLIES U() >= u” is easily provable for optimal m* and u*, because assuming PA is sound, UDT-OB will reach the step with m=m* and u=u*, and since PA-j can prove that it reaches this step, it can (using the above IMPLIES statement) prove ‘if “UDT-OB(i) == m[i] for every i in actions.keys() AND U() >= u” is provable in PA-j then UDT-OB(i) == m[i] for every i in actions.keys() AND U() >= u’.
This also works for some cases where Löbian circles are needed, provided that when each agent tries to prove the necessary statements, they are using proof systems that are strong enough to prove that both agents reach that step. I’m not sure how to arrange this in general.