偏好的无环性、纳什均衡与子博弈完美均衡：一种形式化且构造性的等价关系

1953 年，Kuhn 通过证明博弈论中名为“逆向归纳法”的过程能产生纳什均衡，展示了每个序贯博弈都存在纳什均衡。实际上，该方法产生的纳什均衡构成了纳什均衡的一个真子类。1965 年，Selten 将这个真子类命名为子博弈完美均衡。在博弈论中，收益通常是游戏结束时授予的奖励。虽然传统博弈论主要关注实值收益（隐含地由实数上的通常全序排列），但 Simon 或 Blackwell 的工作已涉及偏序收益。本文通过将实值收益函数替换为称为结果的抽象原子对象，并将实数上的通常全序替换为结果上的任意二元关系（称为偏好），推广了序贯博弈的概念。这引入了一种通用的抽象形式体系，其中仍可定义纳什均衡、子博弈完美均衡和“逆向归纳法”。本文证明了以下三个命题是等价的：1) 对结果的偏好是无环的。2) 每个序贯博弈都有一个纳什均衡。3) 每个序贯博弈都有一个子博弈完美均衡。该结果完全使用 Coq 进行了计算机认证。除了提供额外的正确性保证外，使用 Coq 进行形式化的工作还有助于清晰地识别有用的定义和证明的主要环节。