User:Nisan/Can anyone see this?

Nesov introduced an agent that searches for statements of the form A=a -> U=u with proofs up to a maximum length N. PA oracle. Default D. Acts correctly in 5-and-10 (C and D dominant) as long as N is reasonably big. I guess it behaves incorrectly in PD (except trivially in (D, D) Nash).

Nesov introduced "playing chicken" for programs, although the chicken idea is due to Nesov. Nisan adapted it to arithmetic. PA oracle. C, D chicken. Default D. In that post, it's criterion for action is pretty strict, but can be relaxed. Compares actions to the default. Acts correctly in 5-and-10 (C and D dominant) and PD ((D,D) Nash, (C, C) Nash). But it doesn't behave well on the PD with the (C, D) or (D, C) Nash equilibria. I'd guess that this is all true if the payoffs are asymmetric.