Biprofile Deviation Logic: Report-Replacement Frames and Audit Witnesses

तकनीकी सारांश: बाइप्रोफाइल विचलन तर्क (Biproprofile Deviation Logic): रिपोर्ट-प्रतिस्थापन फ्रेम और ऑडिट विटनेस

समस्या विवरण
यह शोध पत्र रणनीतिक सामाजिक चयन (strategic social choice) के औपचारिकीकरण को संबोधित करता है, विशेष रूप से एक "वास्तविक" वरीयता प्रोफ़ाइल ($R$) जो कल्याण तुलनाओं को निर्धारित करती है, और एक "सबमिट की गई" रिपोर्ट प्रोफ़ाइल ($P$) के बीच अंतर करता है जो सामाजिक चयन नियम के परिणाम को निर्धारित करती है। पारंपरिक मोडल लॉजिक दृष्टिकोण अक्सर विचलन (deviation) को एक जेनेरिक ग्राफ एज के रूप में देखते हैं या सामान्य पत्राचार सिद्धांत (जैसे, साल्क्विस्ट प्रमेय) पर निर्भर करते हैं, बिना विशिष्ट गठबंधन-आधारित रिपोर्ट प्रतिस्थापन के बीजगणितीय ढांचे को स्पष्ट रूप से मॉडल किए। लेखक एक ऐसे तर्क की कमी की पहचान करते हैं जो अवस्था (state) को $(R, P)$ के युग्म के रूप में मानता है, जहाँ मोडैलिटीज़ (modalities) एक विशिष्ट गठबंधन $C$ के रिपोर्ट निर्देशांकों को बदलने के लिए सटीक रूप से समर्पित हैं, जबकि वास्तविक प्रोफ़ाइल $R$ को अपरिवर्तित रखती हैं। इसके अतिरिक्त, एक "ऑडिट लेयर" की आवश्यकता है जो यह सत्यापित करे कि रणनीतिक गुण (जैसे, रणनीति-प्रमाणन/strategy-proofness) कैसे व्यवहार करते हैं जब स्वीकार्य रिपोर्टों का डोमेन बदला जाता है (जैसे, प्रतिबंधित, विस्तारित, या सार्वजनिक रूप से हटाया गया) बिना शास्त्रीय असंभवता प्रमेयों को पुन: सिद्ध किए।

कार्यप्रणाली
लेखक बाइप्रोफाइल विचलन तर्क (Biprofile Deviation Logic) विकसित करते हैं, जो एक मल्टीमॉडल लॉजिक है जहाँ अवस्थाएँ $(R, P)$ के युग्म हैं।

1. सिमेंटिक्स (Semantics): यह तर्क एजेंटों के एक सेट $N$ द्वारा परिभाषित $\text{Dev}(N)$ के फ्रेमों का उपयोग करता है। एक गठबंधन $C$ के लिए एक्सेसिबिलिटी रिलेशंस (accessibility relations) $E_C$, एजेंटों के लिए रिपोर्ट निर्देशांकों के प्रतिस्थापन का प्रतिनिधित्व करते हैं। मुख्य सिमेंटिक बाधा सटीक यूनियन-कंपोजिशन नियम (exact union-composition law) है: $E_C \circ E_D = E_{C \cup D}$। यह इस अंतर्ज्ञान को पकड़ता है कि विलगित (disjoint) गठबंधनों द्वारा स्वतंत्र रिपोर्ट परिवर्तन, उनके यूनियन द्वारा परिवर्तन के बराबर होते हैं।
2. प्रूफ थ्योरी (Proof Theory): प्रत्येक गठबंधन के लिए S5 व्यवहार (रिफ्लेक्सिविटी, ट्रांजिटिविटी, यूक्लिडियन प्रॉपर्टी) के लिए एक्सिओम्स (axioms) के साथ एक हिल्बर्ट सिस्टम $H_{bp}$ को परिभाषित किया गया है, जिसमें खाली गठबंधन के लिए एक आइडेंटिटी एक्सिओम, गठबंधन उपसमुच्चयों के लिए समावेशन (inclusion) एक्सिओम, और गठबंधनों के यूनियन के लिए एक रिडक्शन एक्सिओम शामिल है।
3. पूर्णता प्रमाण (Completeness Proof): शोध पत्र $H_{bp}$ के लिए एक प्रत्यक्ष कैनोनिकल पूर्णता प्रमाण प्रदान करता है। एक प्रमुख तकनीकी चरण में कैनोनिकल मॉडल में एक "मिडपॉइंट" का निर्माण करना शामिल है ताकि रिवर्स इनक्लूजन कंपोजिशन एक्सिओम ($R_{C \cup D} \subseteq R_C \circ R_D$) को सिद्ध किया जा सके, यह सुनिश्चित करते हुए कि कैनोनिकल फ्रेम बिना किसी उत्पाद संरचना (product structure) को पूर्व-मान्य किए सटीक यूनियन-कंपोजिशन नियम को संतुष्ट करता है।
4. प्रतिनिधित्व पृथक्करण (Representation Separation): लेखक अमूर्त $\text{Dev}(N)$ समीकरणों को संतुष्ट करने वाले अमूर्त फ्रेमों और ठोस रिपोर्ट-निर्देशांक उत्पादों के बीच अंतर करते हैं। वे सिद्ध करते हैं कि एक वास्तविक उत्पाद संरचना को अमूर्त बीजगणित से पुनः प्राप्त करने के लिए एक अतिरिक्त निर्देशांक पृथक्करण (coordinate separation) स्थिति आवश्यक है।
5. ऑडिट फ्रेमवर्क (Audit Framework): शोध पत्र शास्त्रीय सामाजिक चयन अवधारणाओं (रणनीति-प्रमाणन, गिबर्ड-सैटरथवेट, सिंगल-पीक्डनेस) को मोडल फॉर्मूला में अनुवादित करता है। इसके बाद, यह एक "ऑडिट लेयर" पेश करता है जो निदान करता है कि डोमेन के प्रतिनिधित्व में परिवर्तन (जैसे, ऑफ-डोमेन विस्तार या सार्वजनिक विलोपन) होने पर रणनीतिक गुण कैसे बदलते हैं।

प्रमुख योगदान

• मोडल कोर (Theorem 1): शोध पत्र $\text{Dev}(N)$ के अमूर्त फ्रेम वर्ग के लिए $H_{bp}$ की साउंडनेस और पूर्णता को सिद्ध करता है। यह विशेष रूप से उस "मिडपॉइंट" चरण को अलग करता और सिद्ध करता है जो रिवर्स कंपोजिशन एक्सिओम के लिए आवश्यक है, जो इस विशिष्ट सेमिलैटेस टेबल (semilattice table) के लिए गैर-रूटीन हिस्सा है।
• प्रतिनिधित्व सीमा (Proposition 1): लेखक प्रदर्शित करते हैं कि अमूर्त $\text{Dev}(N)$ समीकरणों को संतुष्ट करना एक ठोस निर्देशांक-उत्पाद संरचना को पुनः प्राप्त करने की गारंटी देने के लिए पर्याप्त नहीं है। वे पहचानते हैं कि एक अमूर्त विचलन फ्रेम से वास्तविक रिपोर्ट-निर्देशांक उत्पाद को पुनः प्राप्त करने के लिए निर्देशांक पृथक्करण आवश्यक और पर्याप्त शर्त है।
• ऑडिट थ्योरम्स (Audit Theorems):
  • थ्योरम 4 (बाउंड्री-रो क्राइटेरियन): यह स्थापित करता है कि किसी नियम को बड़े रिपोर्ट डोमेन तक विस्तारित करने से नए हेरफेर विटनेस (manipulation witnesses) केवल "सीमा" (अर्थात, जो पहले अस्वीकरणीय थे) पर बनते हैं। यह पूरे डोमेन की पुन: जाँच किए बिना रणनीति-प्रमाणन के वृद्धिशील सत्यापन की अनुमति देता है।
  • प्रपोजिशन 6 (फैक्टर-क्लोजर क्राइटेरियन): एक सार्वजनिक विलोपन (सबमॉडल) के लिए $\text{Dev}(N)$ बीजगणितीय संरचना को बनाए रखने के लिए एक आवश्यक और पर्याप्त शर्त प्रदान करता है। शर्त यह है कि जीवित बचे हुए अवस्थाओं को "फैक्टर क्लोज्ड" होना चाहिए, जिसका अर्थ है कि कोई भी जीवित बचा हुआ एज $E_{C \cup D}$ एक जीवित बचे मध्यवर्ती अवस्था के माध्यम से फैक्टर करने योग्य होना चाहिए।
• परिमित ऑडिट तंत्र (Finite Audit Mechanisms): शोध पत्र एक टाइप्ड सर्टिफिकेट फॉर्मेट और निष्पादन योग्य चेकर (Python, Lean, और Alloy में) पेश करता है जो तर्क के परिमित उदाहरणों को सत्यापित करता है। इसमें एक "विटनेस रीप्ले" तंत्र शामिल है जो विटनेस रिकॉर्ड के किस क्षेत्र में परिवर्तन हुआ है, इसके आधार पर विफलताओं को 'एज-डिलीटेड', 'बाउंड्री-विटनेस', या 'अनसेफ-अपडेट' के रूपक रूप में वर्गीकृत करता है।

परिणाम

• पूर्णता (Completeness): $H_{bp}$ प्रणाली $\text{Dev}(N)$ के लिए पूर्ण सिद्ध है। प्रमाण एक कैनोनिकल मॉडल निर्माण पर निर्भर करता है जो स्पष्ट रूप से यूनियन-कंपोजिशन नियम को साकार करता है।
• शास्त्रीय प्रमेयों का अनुवाद: गिबर्ड-सैटरथवेट प्रमेय और मूलिन के मीडियन वोटर प्रमेय को सफलतापूर्वक बाइप्रोफाइल भाषा में अनुवादित किया गया है। शोध पत्र इन प्रमेयों को पुनः सिद्ध नहीं करता है, बल्कि डोमेन परिवर्तनों के तहत उनके व्यवहार का विश्लेषण करने के लिए इस नई भाषा का उपयोग करता है।
• केस स्टडी: पाँच-एजेंट सिंगल-पीक्ड मीडियन उदाहरण का उपयोग ऑडिट लेयर को प्रदर्शित करने के लिए किया गया है। अध्ययन दिखाता है कि कैसे एक एकल हेरफेर विटनेस टुपल $(R, P, C, Q, x, y)$ को तीन परिदृश्यों के तहत अलग तरह से व्याख्यायित किया जाता है:
  1. प्रतिबंधित डोमेन (Restricted Domain): विटनेस "एज-डिलीटेड" है क्योंकि विचलित रिपोर्ट $Q$ प्रतिबंधित डोमेन जनरेटर द्वारा उत्पन्न नहीं होती है।
  2. ऑफ-डोमेन विस्तार (Off-Domain Extension): विटनेस एक "बाउंड्री-रो" विफलता है, जो केवल नए स्वीकार्य रिपोर्ट $Q$ द्वारा निर्मित है।
  3. सार्वजनिक विलोपन (Public Deletion): विटनेस जीवित रह सकता है (एंडपॉइंट्स बने रहते हैं), लेकिन अपडेट "अनसेफ" है क्योंकि एक मिश्रित मिडपॉइंट का विलोपन $\text{Dev}(N)$ बीजगणित के लिए आवश्यक फैक्टर-क्लोजर को तोड़ देता है।
• सत्यापन जटिलता (Verification Complexity): प्रपोजिशन 7 स्थापित करता है कि एजेंटों के एक निश्चित सेट $N$ के लिए एक सबमिट किए गए परिमित टाइप्ड सर्टिफिकेट का सत्यापन सर्टिफिकेट के आकार के सापेक्ष बहुपद (polynomial) में होता है।

महत्व और दावे
शोध पत्र मुख्य रूप से एक नए असंभवता प्रमेय के बजाय एक औपचारिक ऑडिट फ्रेमवर्क के रूप में अपनी महत्ता का दावा करता है।

• चिंताओं का पृथक्करण (Separation of Concerns): यह प्रमाण-सैद्धांतिक स्पाइन (अमूर्त बीजगणित की पूर्णता) को प्रतिनिधित्व सीमा (निर्देशांकों को पुनः प्राप्त करना) और अनुप्रयोग परत (डोमेन परिवर्तनों का ऑडिट करना) से अलग करता है।
• परिचालन मूल्य (Operational Value): लेखक तर्क देते हैं कि उनकी "ऑडिट लेयर" सामाजिक चयन तंत्र के लिए एक नैदानिक इंटरफेस प्रदान करती है। डोमेन संशोधित होने पर जटिल असंभवता प्रमाणों को फिर से चलाने के बजाय, सत्यापनकर्ता केवल नई पंक्तियों की जाँच करने के लिए बाउंड्री-रो थ्योरम और यह जाँचने के लिए कि क्या कोई विलोपन आवश्यक बीजगणितीय संरचना को बनाए रखता है, फैक्टर-क्लोजर क्राइटेरियन का उपयोग कर सकते हैं।
• विनम्रता (Modesty): लेखक स्पष्ट रूप से कहते हैं कि वे \text{Dev}(N} के लिए सामान्य संतृप्ति एल्गोरिदम (satisfiability algorithm) या संक्षिप्त रूप से प्रस्तुत नियमों के लिए नया जटिलता बाउंड प्रदान नहीं करते हैं। पूर्णता का परिणाम अमूर्त फ्रेम वर्ग के लिए है, और परिमित जाँच स्पष्ट रूप से दिए गए सर्टिफिकेट के लिए है। यह कार्य एक "छोटा लेकिन पूर्ण ऑडिट परिदृश्य" के रूप में प्रस्तुत किया गया है जो यह स्पष्ट करता है कि प्रतिनिधित्व परिवर्तन रणनीतिक गुणों को कहाँ और क्यों प्रभावित करता है, न कि सामाजिक चयन की मौलिक समस्याओं के लिए एक नया समाधान प्रदान करता है।