防操纵社会选择机制逻辑研究述评

李 娜，孙 雯

(南开大学哲学院，天津 300071)

目前，防操纵社会选择机制在许多领域被独立研究，国内防操纵的研究主要集中在社会选择的理论领域，关于防操纵社会选择机制的逻辑研究还比较少，于是我们介绍了国外在这方面的最新研究成果，希望由此激发我国逻辑学界对这一领域感兴趣的学者作进一步的探究。

一、什么是防操纵社会选择机制

从直观上讲，防操纵(non-manipulability)或防策略(Strategy-proofness)通常被认为是一种非常理想的属性，它要求投票者不能从谎报他们的真实偏好中获益，进而可以抑制社会选择中的策略投票，促使投票者都投出自己的真实选票，使选举结果能够体现人们的真实意愿。

自20世纪70年代以来，Gibbard-Satterthwaite防策略不可能定理确立后，人们对如何避免策略操纵，即防策略操纵问题开始了广泛的研究。此后，出现了大量的数学定理，用来处理和解决投票程序的操纵性，并从理论上论证了防策略不可能性定理。从本质上讲，Gibbard-Satterthwaite防策略不可能性定理意味着任何投票选择程序在一定条件下，要么是可被操纵的，要么是独裁的。这在理论界引起了很大的震动，特别是对经济领域的资源合理配置理论的存在性和合理性提出了巨大的挑战。

防操纵社会选择机制设计的目的，一是为了抑制社会选择中的“策略投票”，避免个人欺骗;二是防止垄断的出现。然而，社会选择中各成员之间因各种原因会形成联盟，决策时联盟中各成员根据集体意志采取行动，而非根据单纯的个人偏好。因此，在存在利益集团的情况下，选择规则的防策略性等问题仅依靠社会选择理论本身难以完成，有鉴于此，Gibbard-Satterthwaite防策略不可能性定理已经引起了数学、计算机科学、逻辑学，以及哲学等领域中研究者的广泛注意。

二、防操纵社会选择机制的研究状况

防操纵社会选择理论的研究最早可以追溯到20世纪60年中后期关于投票理论的研究，维克瑞(Vickery)、达米特(Dummett)和法夸尔森(Farquharson)等都对防操纵问题进行过研究，但他们都未能对投票程序的可被操纵性从理论上加以解释和证明。之后，吉伯德(Allan Gibbard)和萨特斯韦特(Mark Satterthwaite)扩展了阿罗不可能定理的思想，分别于1973年和1975年提出了著名的Gibbard-Satterthwaite防策略不可能性定理。正如前文所述及，该定理意味着从本质上讲，防策略投票不可能性定理意味着在一定条件下，任何投票选择程序要么是可被操纵的，要么是独裁的。这一定理从理论上证明了社会决策过程中策略投票行为的普遍存在性。

21世纪初，泰勒(Alan D.Taylor)2005年在其著作《社会选择和操纵的数学》中用公理化的方法，首次严谨系统地给出了Gibbard-Satterthwaite防策略不可能定理、Duggan-Schwartz定理、Barberá-Kelly定理这三个定理的统一证明［1］。其中，Gibbard-Satterthwaite防策略不可能定理在社会选择中是非常重要的，在过去的30年里，有许多关于这个定理的证明。泰勒借助集合论，通过大量的谓词演算，对Gibbard-Satterthwaite防策略不可能性定理进行了精致的逻辑刻画，这对化解操纵问题提供了很大的帮助。基于上述工作，范艾吉克(Jan van Eijck)2011年借助Saari方法将三角型分为六个区域，分别代表六种不同的投票类型，通过从一个区域移动到另一个区域来改变其投票类型。三角形的三个顶点分别代表不同的选票，越接近一个区域的顶点，越偏好于这个顶点所代表的选票。这种方法很巧妙地简化了Gibbard-Satterthwaite防策略不可能性定理的证明，从新的角度论证了防策略不可能性定理［2］。

不难看出，社会选择理论最初引入逻辑只是其公理化方法的严格使用，而不是作为一个正规的形式系统的应用。对此，艾格特尼斯(Thomas gotnes)、特罗卡尔(Nicolas Troquard)、帕瑞曼(Erik Parmann)等人做了进一步研究。

艾格特尼斯等2006年基于模态逻辑，设计了一种可以刻画社会福利函数的逻辑，这种逻辑在语法上是简单的，但足以表达社会福利函数的属性，如量化偏好关系，从而刻画阿罗定理［3］。特罗卡尔等2011年设计了一种逻辑，用于推理社会选择函数。这个逻辑也是基于模态逻辑的，想法来源于命题控制联盟逻辑(CL-PC)［4］。CL-PC逻辑包括可以表示策略稳定性的算子。特罗卡尔等扩展了这种逻辑，增加了表示个体偏好的算子，个体的策略稳定性由CL-PC-like算子表示。由此，更精确地确立了社会选择函数的属性和逻辑公式之间的联系，表明使用逻辑语言可以很好地刻画社会选择函数。每一个社会选择函数都可以由一个逻辑公式来描述，并且这个逻辑是可判定的，这种处理在判断社会选择函数是否防操纵这一问题上起了相当大的作用。

同年，艾格特尼斯等提出了偏好和判断聚合的逻辑，判断聚合是从逻辑的角度研究聚合，考虑如何将多组逻辑公式聚合为一个单个一致集。判断聚合也可以看作是偏好聚合的子集。他们提出的判断聚合逻辑(JAL)，可以直接解释判断聚合规则［5］。

帕瑞曼和艾格特尼斯2012年基于乘积逻辑S5m，提出了一种投票逻辑(voting logic)，增加了算子□U，用于量化所有真实的情境，即个体如实表达他们偏好的真实世界。进而刻画了独裁、防策略等属性，并完整地表述了Gibbard-Satterthwaite防策略不可能定理。另外，帕瑞曼和艾格特尼斯还讨论了该逻辑的表达力问题，说明当存在多个个体(投票者)时，它是不可判定的，然而，也有特例，即当有两个个体时，是可判定的［6］。

可以看出，上述工作都是基于模态逻辑，以设计适合的逻辑系统来模型社会选择中防操纵问题。其实，逻辑和博弈(logic and games)领域中有很多这方面的研究，如可以用模态逻辑来刻画博弈理论中的概念，如策略、偏好、联盟等，这些概念也是社会选择中的重要概念。然而，在逻辑和博弈中，关注的是个体如何在一个情境中行为，而不是关注于如何模型一个机制，以实现社会选择。

另外，还有一些逻辑学家，利用已有的逻辑框架，如高阶逻辑、命题逻辑、一阶逻辑来研究社会选择问题及刻画防策略不可能性定理。

尼普科夫(T.Nipkow)2009年通过用高阶逻辑对阿罗定理和防策略不可能性定理进行了论证［7］。同年，唐平中和林方真在命题逻辑的基础上，设计了一种社会选择的逻辑语言，引入了一元谓词情境的概念，并令4元谓词p来模型个体偏好，3元谓词w来模型集体偏好。此外，还引入了行动swap(x，a，b)，表示在个体x的偏好序下，将a和b交换位置。基于上述工作，最终将社会选择中的阿罗不可能性定理翻译成相应的逻辑语言，然后使用可满足解析器(SAT solver)来对之进行验证，从而完整自动地证明不可能性定理［8］。

在此基础之上，唐平中2010年用同样的逻辑语言，通过归纳法将防策略不可能性定理的条件减化到基本条件(The base case)，基本条件是指有两个投票者和三个候选人的情况，即当|N|=2并且|O|=3时，社会选择函数是一个映射，它是防策略的当且仅当它是独裁的。另外，唐平中还使用了计算程序来验证这个部分，他把这个问题看成是一个限制可满足问题(CSP)，并且使用所谓的深度搜索策略(depth-first search algorithm)，先找到满足前两个条件的社会选择函数，然而再验证它们都是独裁的。最后，在基本事例下，可以验证有17个防策略社会选择函数是独裁的［9］。在某种程度上，借助逻辑来辅助分析和设计社会选择过程，形式地刻画社会选择中一些重要的不可能性定理，从而为自动定理证明打下基础，从计算机科学的观点来看，这个问题是很有趣的。

格兰迪(U.Grandi)和安迪瑞斯(U.Endriss)2009年用一阶逻辑来模型化社会选择中的理论，将社会选择中的社会福利函数嵌入到古典一阶逻辑中，用一阶逻辑成功地刻画了阿罗不可能定理［10］。继而，格兰迪和安迪瑞斯2012年又用一阶逻辑来刻画偏好聚合中的不可能性定理，提出了社会福利函数的一阶定理，成功地形式化了社会选择中的三个重要的结论，即对 Arrow定理(1963)、Sen定理(1972)、Kirman-Sondermann定理(1972)进行了逻辑刻画，并用prover 9，最终实现自动推理证明［11］。

不难看出，对于验证社会选择中的不可能定理，一个完整的形式化更能保证结果的正确性，并且还可以为自动推理的实现建立很好的基础。笔者认为，这种方法可以作为研究社会选择理论中的古典定理及发现新定理的一种不错的方法。

总之，对于社会选择学家来说，可能最大的受益就是从逻辑中可以借助纯形式语言来研究和推理社会选择中的重要问题。因此，对社会选择理论中的防策略不可能性定理，提供一个纯形式化表述，以最终实现自动定理证明，以及设计一个适合的逻辑系统来模型社会选择中防操纵问题，这都是逻辑作为工具应用到社会选择中的重要价值。

三、结语

综上所述，从国外学者对防操纵社会选择理论研究的状况可以看出，借助逻辑工具对防操纵问题的研究，已经引起了逻辑学、计算机科学、经济学等领域中学者的广泛注意。用逻辑的方法来研究防操纵社会选择机制，可以最终完美地刻画和解决防操纵问题，因而其在实践上是可行的，这在今天具有重要的现实意义。然而，对于逻辑学家来说，用现代逻辑模型社会选择中的问题，找到适合的逻辑系统来解决防操纵问题，仍还有许多问题亟待解决。但随着更多的新技术被国内学者所掌握，我们相信，逻辑学界关于防操纵社会选择理论的研究必将逐步丰富起来，并能解决更多的实际问题，研究获得的原创性理论成果也必将推动我国逻辑学理论的发展，使我们的相关研究站在国际的前沿。

［1］Taylor A D.Social choice and the mathematics of manipulation［M］.Cambridge:Cambridge University Press，2005.

［2］Eijck J van .A geometric look at manipulation［J］.Computational Logic in Multi-Agent Systems，2011:92 －104.

［3］Gotnes Thomas，Wooldridge Michael，Hoek Wiebe van der.Towards a logic of social welfare［C］//Proceedings of The 7th Conference on Logic and the Foundations of Game and Decision Theory(LOFT)，2006:1 －10.

［4］Troquard N W，Hoek van der，Wooldridge.Reasoning about social choice functions［J］.Journal of philosophical logic，2011:1 －26.

［5］Gotnes Thomas，Hoek Wiebe van der，Wooldridge Michael.On the logic of preference and judgment aggregation［J］.Autonomous Agents and Multi-Agent Systems，2011.

［6］Parmann Erik，Agotnes Thomas.Modal Logics for Social Choice and Undecidability［Z］.LOFT，2012.

［7］Nipkow T.Social Choice Theory in HOL:Arrow and Gibbard——Satterthwaite［J］.Journal of Automated Reasoning，2009.

［8］Tang P，Lin F.Computer-aided proofs of Arrow’s and other impossibility theorems［D］.Artificial Intelligence，2009，173(11):1041 －1053.

［9］Tang P.Computer-aided Theorem Discovery-A New Adventure and its Application to Economic Theory［J］.PhD dissertation，HKUST，2010.

［10］Grandi U，Endriss U.First-order logic formalisation of Arrow’s theorem［M］.［S.L］:Springer-Verlag，2009.

［11］Grandi U，Endriss U.First-Order Logic Formalisation of Impossibility Theorems in Preference Aggregation［J］.To appear in the Journal of Philosophical Logic，2012:1.