A Naive Encoding of Russell's Paradox in Type Theory

गणित के विशाल परिदृश्य में, विचारों को व्यवस्थित करने के हमारे तरीके और उन्हें बनाने के नियमों के बीच एक मौलिक तनाव मौजूद है। एक सदी से अधिक समय से, गणितज्ञों ने टाइप थ्योरी (प्रकार सिद्धांत) नामक एक ढांचे पर भरोसा किया है ताकि यह सुनिश्चित किया जा सके कि उनके तार्किक ढांचे सुदृढ़ और विरोधाभासों से मुक्त हों। इस प्रणाली को एक कठोर फाइलिंग कैबिनेट के रूप में समझें जहाँ प्रत्येक वस्तु को एक विशिष्ट फोल्डर में होना चाहिए, और फोल्डर स्वयं को या अन्य फोल्डरों को इस तरह नहीं रख सकते जो एक लूप (चक्र) बना दे। यह अलगाव रसेल के विरोधाभास (रसेल के पैराडॉक्स) नामक एक प्रसिद्ध तार्किक जाल को रोकता है, जो 1900 के दशक की एक पहेली थी जिसने दिखाया था कि यदि नियम बहुत ढीले हों तो एक सरल प्रश्न—"क्या उन सभी सेटों का सेट जो स्वयं में स्वयं को शामिल नहीं करते, स्वयं को शामिल करता है?"—कैसे एक प्रणाली को तोड़ सकता है। जबकि आधुनिक गणित ने इन श्रेणियों को सख्ती से अलग करके इस जाल से सफलतापूर्वक बचाव किया है, शोधकर्ता यह समझने के लिए कि ये प्रणालियाँ वास्तव में कहाँ और क्यों टिकी रहती हैं, इनके सीमाओं का अन्वेषण करना जारी रखते हैं।

नागोया विश्वविद्यालय के क्व ज़ुओयुआन द्वारा लिखा गया एक हालिया नोट इस सीमा पर सीधा प्रहार करता है, जो यह दर्शाता है कि कैसे कोई अनजाने में उस प्राचीन विरोधाभास को एक आधुनिक टाइप थ्योरी प्रणाली के भीतर पुन: उत्पन्न कर सकता है। लेखक यह दावा नहीं करता है कि उन्होंने मानक गणित में कोई दोष पाया है, बल्कि वह यह दिखाता है कि क्या होता है यदि कोई जानबूझकर एक विशिष्ट सुरक्षा तंत्र को हटा देता है। इस प्रयोग में, शोधकर्ता एक ऐसी स्थिति का निर्माण करता है जहाँ प्रकारों के एक "यूनिवर्स" (ब्रह्मांड) को स्वयं को समाहित करने की अनुमति दी जाती है, जिसे "टाइप-इन-टाइप" (प्रकार-में-प्रकार) नामक स्थिति कहा जाता है। समानता (equality) को संभालने के एक विशिष्ट तरीके के साथ संयोजन करते हुए—जहाँ दो चीजों के समान होने के किसी भी प्रमाण को एक ही माना जाता है—लेखक सफलतापूर्वक एक ऐसा तार्किक ढांचा बनाने में सफल रहा है जो मूल विरोधाभास की नकल करता है। परिणाम एक स्पष्ट, सीधा प्रमाण है कि यदि आप एक ब्रह्मांड को स्वयं को समाहित करने की अनुमति देते हैं और आप यह मानते हैं कि समानता सिद्ध करने के सभी तरीके एक ही हैं, तो प्रणाली विरोधाभास में ढह जाती है।

यह निर्माण एक विशेष संग्रह को परिभाषित करके कार्य करता है जो प्रत्येक संभावित प्रकार को एक साथ लाता है, ठीक वैसे ही जैसे सभी श्रेणियों का एक मास्टर कैटलॉग। इस संग्रह के भीतर, शोधकर्ता एक विशिष्ट समूह को परिभाषित करता है: उन सभी चीजों का समूह जो स्वयं में स्वयं को शामिल नहीं करते हैं। एक सामान्य, सुरक्षित प्रणाली में, यह समूह अस्तित्व में नहीं हो सकता क्योंकि नियम एक श्रेणी को स्वयं का सदस्य बनने से रोकते हैं। हालाँकि, इस विशिष्ट सेटअप में, लेखक एक तरीका बनाता है जिससे यह पूछा जा सके कि क्या यह समूह स्वयं में स्वयं को शामिल करता है। तर्क एक कड़े, अपरिहार्य पथ का अनुसरण करता है: यदि समूह स्वयं में स्वयं को शामिल करता है, तो अपनी परिभाषा के अनुसार उसे ऐसा नहीं होना चाहिए; लेकिन यदि वह स्वयं में स्वयं को शामिल नहीं करता है, तो वह परिभाषा में फिट बैठता है और स्वयं को शामिल करना चाहिए। यह एक लूप बनाता है जहाँ कथन एक ही समय में सत्य और असत्य दोनों है, जो यह सिद्ध करता है कि प्रणाली असंगत है।

इस खोज को जो बात विशेष रूप से महत्वपूर्ण बनाती है, वह है उपयोग किया गया विशिष्ट उपकरण। लेखक 'यूनिकनेस ऑफ आइडेंटिटी प्रूफ' (पहचान प्रमाण की विशिष्टता) नामक एक सिद्धांत पर निर्भर करता है, जो अनिवार्य रूप से कहता है कि यदि आप दो चीजों के समान होने का प्रमाण दे सकते हैं, तो इसे करने का केवल एक ही तरीका है। यह सिद्धांत अक्सर कई मानक गणितीय प्रणालियों में तर्क को सरल बनाने के लिए माना जाता है। शोध पत्र दिखाता है कि यह धारणा, जब स्वयं को समाहित करने वाले ब्रह्मांड के साथ जुड़ती है, तो विरोधाभास को सक्रिय करने के लिए पर्याप्त है। महत्वपूर्ण रूप से, लेखक इंगित करता है कि यह निर्माण एक अलग, अधिक आधुनिक ढांचे में विफल हो जाएगा जिसे होमोटॉपी टाइप थ्योरी (होमोटॉपी टाइप थ्योरी) कहा जाता है, जहाँ पहचान प्रमाण की विशिष्टता को नहीं माना जाता है। उस वैकल्पिक प्रणाली में, दो चीजों के समान होने का प्रमाण देने के कई अलग-अलग तरीके होते हैं, और यह विविधता विरोधाभास को बनने से रोकती है।

यह पत्र इस विरोधाभास को पुन: उत्पन्न करने के पिछले प्रयासों से अपने दृष्टिकोण को अलग करता है। अन्य शोधकर्ताओं के पिछले कार्यों ने एक समान परिणाम प्राप्त करने के लिए जटिल, वृक्ष-नुमा संरचनाओं का उपयोग किया था, जिसमें अधिक जटिल मशीनरी की आवश्यकता थी। यह नया दृष्टिकोण अधिक सरल और सीधा है, जो जटिल पेड़ों की आवश्यकता के बिना केवल प्रकारों और तार्किक संबंधों के बुनियादी घटकों का उपयोग करता है। यह समस्या को उसके मूल घटकों तक सीमित कर देता है, यह दिखाते हुए कि विरोधाभास जटिल मशीनरी का परिणाम नहीं है, बल्कि स्वयं को समाहित करने वाले ब्रह्मांड को अनुमति देने और समानता के सभी प्रमाणों को एक समान मानने का एक सीधा परिणाम है। पूरी तार्किक श्रृंखला को कंप्यूटर प्रूफ़ असिस्टेंट द्वारा सत्यापित किया गया है, जो पुष्टि करता है कि चरण वैध हैं और विरोधाभास परिभाषित नियमों के भीतर वास्तविक है।

अंततः, यह कार्य एक तार्किक खतरे के क्षेत्र के सटीक मानचित्र के रूप में कार्य करता है। यह यह सुझाव नहीं देता कि गणित टूटा हुआ है, बल्कि यह स्पष्ट करता है कि इसे सुरक्षित रखने के लिए कौन से नियम आवश्यक हैं। यह दिखाकर कि विरोधाभास को विशिष्ट धारणाओं के सेट के साथ बनाया जा सकता है, लेखक इस बात को पुख्ता करता है कि तार्किक पतन को रोकने के लिए वे धारणाएं कितनी महत्वपूर्ण हैं। यह एक अनुस्मारक है कि गणित की वास्तुकला में, समानता या ब्रह्मांडों को व्यवस्थित करने के तरीके के संबंध में एक एकल शिथिल नियम भी ऐसी संरचना की ओर ले जा सकता है जो अपने स्वयं के विनाश का समर्थन करती है। यह अध्ययन एक स्पष्ट प्रदर्शन है कि निरंतरता (consistency) कोई दी गई चीज़ नहीं है, बल्कि एक सावधानीपूर्वक बनाए रखा गया राज्य है जो उन विशिष्ट बाधाओं पर निर्भर करता है जिन्हें हम लागू करने का विकल्प चुनते हैं।