防操縱社會選擇機制邏輯研究述評

李 娜，孫 雯

(南開大學哲學院，天津 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.