李 娜，孫 雯

(南開大學(xué)哲學(xué)院，天津 300071)

目前，防操縱社會選擇機(jī)制在許多領(lǐng)域被獨(dú)立研究，國內(nèi)防操縱的研究主要集中在社會選擇的理論領(lǐng)域，關(guān)于防操縱社會選擇機(jī)制的邏輯研究還比較少，于是我們介紹了國外在這方面的最新研究成果，希望由此激發(fā)我國邏輯學(xué)界對這一領(lǐng)域感興趣的學(xué)者作進(jìn)一步的探究。

一、什么是防操縱社會選擇機(jī)制

從直觀上講，防操縱(non-manipulability)或防策略(Strategy-proofness)通常被認(rèn)為是一種非常理想的屬性，它要求投票者不能從謊報(bào)他們的真實(shí)偏好中獲益，進(jìn)而可以抑制社會選擇中的策略投票，促使投票者都投出自己的真實(shí)選票，使選舉結(jié)果能夠體現(xiàn)人們的真實(shí)意愿。

自20世紀(jì)70年代以來，Gibbard-Satterthwaite防策略不可能定理確立后，人們對如何避免策略操縱，即防策略操縱問題開始了廣泛的研究。此后，出現(xiàn)了大量的數(shù)學(xué)定理，用來處理和解決投票程序的操縱性，并從理論上論證了防策略不可能性定理。從本質(zhì)上講，Gibbard-Satterthwaite防策略不可能性定理意味著任何投票選擇程序在一定條件下，要么是可被操縱的，要么是獨(dú)裁的。這在理論界引起了很大的震動(dòng)，特別是對經(jīng)濟(jì)領(lǐng)域的資源合理配置理論的存在性和合理性提出了巨大的挑戰(zhàn)。

防操縱社會選擇機(jī)制設(shè)計(jì)的目的，一是為了抑制社會選擇中的“策略投票”，避免個(gè)人欺騙;二是防止壟斷的出現(xiàn)。然而，社會選擇中各成員之間因各種原因會形成聯(lián)盟，決策時(shí)聯(lián)盟中各成員根據(jù)集體意志采取行動(dòng)，而非根據(jù)單純的個(gè)人偏好。因此，在存在利益集團(tuán)的情況下，選擇規(guī)則的防策略性等問題僅依靠社會選擇理論本身難以完成，有鑒于此，Gibbard-Satterthwaite防策略不可能性定理已經(jīng)引起了數(shù)學(xué)、計(jì)算機(jī)科學(xué)、邏輯學(xué)，以及哲學(xué)等領(lǐng)域中研究者的廣泛注意。

二、防操縱社會選擇機(jī)制的研究狀況

防操縱社會選擇理論的研究最早可以追溯到20世紀(jì)60年中后期關(guān)于投票理論的研究，維克瑞(Vickery)、達(dá)米特(Dummett)和法夸爾森(Farquharson)等都對防操縱問題進(jìn)行過研究，但他們都未能對投票程序的可被操縱性從理論上加以解釋和證明。之后，吉伯德(Allan Gibbard)和薩特斯韋特(Mark Satterthwaite)擴(kuò)展了阿羅不可能定理的思想，分別于1973年和1975年提出了著名的Gibbard-Satterthwaite防策略不可能性定理。正如前文所述及，該定理意味著從本質(zhì)上講，防策略投票不可能性定理意味著在一定條件下，任何投票選擇程序要么是可被操縱的，要么是獨(dú)裁的。這一定理從理論上證明了社會決策過程中策略投票行為的普遍存在性。

21世紀(jì)初，泰勒(Alan D.Taylor)2005年在其著作《社會選擇和操縱的數(shù)學(xué)》中用公理化的方法，首次嚴(yán)謹(jǐn)系統(tǒng)地給出了Gibbard-Satterthwaite防策略不可能定理、Duggan-Schwartz定理、Barberá-Kelly定理這三個(gè)定理的統(tǒng)一證明［1］。其中，Gibbard-Satterthwaite防策略不可能定理在社會選擇中是非常重要的，在過去的30年里，有許多關(guān)于這個(gè)定理的證明。泰勒借助集合論，通過大量的謂詞演算，對Gibbard-Satterthwaite防策略不可能性定理進(jìn)行了精致的邏輯刻畫，這對化解操縱問題提供了很大的幫助。基于上述工作，范艾吉克(Jan van Eijck)2011年借助Saari方法將三角型分為六個(gè)區(qū)域，分別代表六種不同的投票類型，通過從一個(gè)區(qū)域移動(dòng)到另一個(gè)區(qū)域來改變其投票類型。三角形的三個(gè)頂點(diǎn)分別代表不同的選票，越接近一個(gè)區(qū)域的頂點(diǎn)，越偏好于這個(gè)頂點(diǎn)所代表的選票。這種方法很巧妙地簡化了Gibbard-Satterthwaite防策略不可能性定理的證明，從新的角度論證了防策略不可能性定理［2］。

不難看出，社會選擇理論最初引入邏輯只是其公理化方法的嚴(yán)格使用，而不是作為一個(gè)正規(guī)的形式系統(tǒng)的應(yīng)用。對此，艾格特尼斯(Thomas gotnes)、特羅卡爾(Nicolas Troquard)、帕瑞曼(Erik Parmann)等人做了進(jìn)一步研究。

艾格特尼斯等2006年基于模態(tài)邏輯，設(shè)計(jì)了一種可以刻畫社會福利函數(shù)的邏輯，這種邏輯在語法上是簡單的，但足以表達(dá)社會福利函數(shù)的屬性，如量化偏好關(guān)系，從而刻畫阿羅定理［3］。特羅卡爾等2011年設(shè)計(jì)了一種邏輯，用于推理社會選擇函數(shù)。這個(gè)邏輯也是基于模態(tài)邏輯的，想法來源于命題控制聯(lián)盟邏輯(CL-PC)［4］。CL-PC邏輯包括可以表示策略穩(wěn)定性的算子。特羅卡爾等擴(kuò)展了這種邏輯，增加了表示個(gè)體偏好的算子，個(gè)體的策略穩(wěn)定性由CL-PC-like算子表示。由此，更精確地確立了社會選擇函數(shù)的屬性和邏輯公式之間的聯(lián)系，表明使用邏輯語言可以很好地刻畫社會選擇函數(shù)。每一個(gè)社會選擇函數(shù)都可以由一個(gè)邏輯公式來描述，并且這個(gè)邏輯是可判定的，這種處理在判斷社會選擇函數(shù)是否防操縱這一問題上起了相當(dāng)大的作用。

同年，艾格特尼斯等提出了偏好和判斷聚合的邏輯，判斷聚合是從邏輯的角度研究聚合，考慮如何將多組邏輯公式聚合為一個(gè)單個(gè)一致集。判斷聚合也可以看作是偏好聚合的子集。他們提出的判斷聚合邏輯(JAL)，可以直接解釋判斷聚合規(guī)則［5］。

帕瑞曼和艾格特尼斯2012年基于乘積邏輯S5m，提出了一種投票邏輯(voting logic)，增加了算子□U，用于量化所有真實(shí)的情境，即個(gè)體如實(shí)表達(dá)他們偏好的真實(shí)世界。進(jìn)而刻畫了獨(dú)裁、防策略等屬性，并完整地表述了Gibbard-Satterthwaite防策略不可能定理。另外，帕瑞曼和艾格特尼斯還討論了該邏輯的表達(dá)力問題，說明當(dāng)存在多個(gè)個(gè)體(投票者)時(shí)，它是不可判定的，然而，也有特例，即當(dāng)有兩個(gè)個(gè)體時(shí)，是可判定的［6］。

可以看出，上述工作都是基于模態(tài)邏輯，以設(shè)計(jì)適合的邏輯系統(tǒng)來模型社會選擇中防操縱問題。其實(shí)，邏輯和博弈(logic and games)領(lǐng)域中有很多這方面的研究，如可以用模態(tài)邏輯來刻畫博弈理論中的概念，如策略、偏好、聯(lián)盟等，這些概念也是社會選擇中的重要概念。然而，在邏輯和博弈中，關(guān)注的是個(gè)體如何在一個(gè)情境中行為，而不是關(guān)注于如何模型一個(gè)機(jī)制，以實(shí)現(xiàn)社會選擇。

另外，還有一些邏輯學(xué)家，利用已有的邏輯框架，如高階邏輯、命題邏輯、一階邏輯來研究社會選擇問題及刻畫防策略不可能性定理。

尼普科夫(T.Nipkow)2009年通過用高階邏輯對阿羅定理和防策略不可能性定理進(jìn)行了論證［7］。同年，唐平中和林方真在命題邏輯的基礎(chǔ)上，設(shè)計(jì)了一種社會選擇的邏輯語言，引入了一元謂詞情境的概念，并令4元謂詞p來模型個(gè)體偏好，3元謂詞w來模型集體偏好。此外，還引入了行動(dòng)swap(x，a，b)，表示在個(gè)體x的偏好序下，將a和b交換位置。基于上述工作，最終將社會選擇中的阿羅不可能性定理翻譯成相應(yīng)的邏輯語言，然后使用可滿足解析器(SAT solver)來對之進(jìn)行驗(yàn)證，從而完整自動(dòng)地證明不可能性定理［8］。

在此基礎(chǔ)之上，唐平中2010年用同樣的邏輯語言，通過歸納法將防策略不可能性定理的條件減化到基本條件(The base case)，基本條件是指有兩個(gè)投票者和三個(gè)候選人的情況，即當(dāng)|N|=2并且|O|=3時(shí)，社會選擇函數(shù)是一個(gè)映射，它是防策略的當(dāng)且僅當(dāng)它是獨(dú)裁的。另外，唐平中還使用了計(jì)算程序來驗(yàn)證這個(gè)部分，他把這個(gè)問題看成是一個(gè)限制可滿足問題(CSP)，并且使用所謂的深度搜索策略(depth-first search algorithm)，先找到滿足前兩個(gè)條件的社會選擇函數(shù)，然而再驗(yàn)證它們都是獨(dú)裁的。最后，在基本事例下，可以驗(yàn)證有17個(gè)防策略社會選擇函數(shù)是獨(dú)裁的［9］。在某種程度上，借助邏輯來輔助分析和設(shè)計(jì)社會選擇過程，形式地刻畫社會選擇中一些重要的不可能性定理，從而為自動(dòng)定理證明打下基礎(chǔ)，從計(jì)算機(jī)科學(xué)的觀點(diǎn)來看，這個(gè)問題是很有趣的。

格蘭迪(U.Grandi)和安迪瑞斯(U.Endriss)2009年用一階邏輯來模型化社會選擇中的理論，將社會選擇中的社會福利函數(shù)嵌入到古典一階邏輯中，用一階邏輯成功地刻畫了阿羅不可能定理［10］。繼而，格蘭迪和安迪瑞斯2012年又用一階邏輯來刻畫偏好聚合中的不可能性定理，提出了社會福利函數(shù)的一階定理，成功地形式化了社會選擇中的三個(gè)重要的結(jié)論，即對 Arrow定理(1963)、Sen定理(1972)、Kirman-Sondermann定理(1972)進(jìn)行了邏輯刻畫，并用prover 9，最終實(shí)現(xiàn)自動(dòng)推理證明［11］。

不難看出，對于驗(yàn)證社會選擇中的不可能定理，一個(gè)完整的形式化更能保證結(jié)果的正確性，并且還可以為自動(dòng)推理的實(shí)現(xiàn)建立很好的基礎(chǔ)。筆者認(rèn)為，這種方法可以作為研究社會選擇理論中的古典定理及發(fā)現(xiàn)新定理的一種不錯(cuò)的方法。

總之，對于社會選擇學(xué)家來說，可能最大的受益就是從邏輯中可以借助純形式語言來研究和推理社會選擇中的重要問題。因此，對社會選擇理論中的防策略不可能性定理，提供一個(gè)純形式化表述，以最終實(shí)現(xiàn)自動(dòng)定理證明，以及設(shè)計(jì)一個(gè)適合的邏輯系統(tǒng)來模型社會選擇中防操縱問題，這都是邏輯作為工具應(yīng)用到社會選擇中的重要價(jià)值。

三、結(jié)語

綜上所述，從國外學(xué)者對防操縱社會選擇理論研究的狀況可以看出，借助邏輯工具對防操縱問題的研究，已經(jīng)引起了邏輯學(xué)、計(jì)算機(jī)科學(xué)、經(jīng)濟(jì)學(xué)等領(lǐng)域中學(xué)者的廣泛注意。用邏輯的方法來研究防操縱社會選擇機(jī)制，可以最終完美地刻畫和解決防操縱問題，因而其在實(shí)踐上是可行的，這在今天具有重要的現(xiàn)實(shí)意義。然而，對于邏輯學(xué)家來說，用現(xiàn)代邏輯模型社會選擇中的問題，找到適合的邏輯系統(tǒng)來解決防操縱問題，仍還有許多問題亟待解決。但隨著更多的新技術(shù)被國內(nèi)學(xué)者所掌握，我們相信，邏輯學(xué)界關(guān)于防操縱社會選擇理論的研究必將逐步豐富起來，并能解決更多的實(shí)際問題，研究獲得的原創(chuàng)性理論成果也必將推動(dòng)我國邏輯學(xué)理論的發(fā)展，使我們的相關(guān)研究站在國際的前沿。

［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.