Glivenko's theorems from an ecumenical perspective

तकनीकी सारांश: एक उदारवादी (Ecumenical) परिप्रेक्ष्य से ग्लिवेंको के प्रमेय

समस्या विवरण
यह शोध पत्र शास्त्रीय तर्क (Classical Logic - CL) और सहजतावादी तर्क (Intuitionistic Logic - IL) के बीच के मौलिक संबंध को संबोधित करता है, विशेष रूप से ग्लिवेंको के प्रमेयों (Glivenko's theorems) की पुनरावृत्ति करता है। ये प्रमेय स्थापित करते हैं कि यदि कोई सूत्र शास्त्रीय रूप से सिद्ध करने योग्य है, तो उसका दोहरा निषेध (double negation) सहजतावादी रूप से सिद्ध करने योग्य होता है, और यदि एक निषेध किया गया सूत्र शास्त्रीय रूप से सिद्ध करने योग्य है, तो वह सहजतावादी रूप से भी सिद्ध करने योग्य होता है। जबकि ये परिणाम अलग-अलग तार्किक प्रणालियों के संदर्भ में अच्छी तरह से समझे गए हैं, यह शोध पत्र जांच करता है कि ये संबंध उदारवादी प्रणालियों (Ecumenical systems) के भीतर कैसे प्रकट होते हैं। उदारवादी प्रणालियाँ वे एकीकृत ढांचे हैं जहाँ शास्त्रीय और सहजतावादी तर्क एक-दूसरे में विलीन हुए बिना शांतिपूर्वक सह-अस्तित्व में रहते हैं, अक्सर ऑपरेटरों (जैसे, शास्त्रीय बनाम सहजतावादी वियोजन) को अलग करके या सूत्रों को उनकी तार्किक प्रकृति को इंगित करने के लिए लेबल लगाकर। केंद्रीय समस्या यह निर्धारित करना है कि जब शास्त्रीय और सहजतावादी तर्क को एक ही निगमन प्रणाली में एकीकृत किया जाता है, तो ग्लिवेंको-प्रकार के परिणाम कैसे अनुवादित होते हैं, और उदारवाद के दो प्राथमिक दृष्टिकोणों के बीच के अंतर का विश्लेषण करना है: "अनुमानवादी" (inferentialist) दृष्टिकोण (ऑपरेटरों को अलग करना) और "सामान्यवादी" (generalist) दृष्टिकोण (लेबल के माध्यम से सूत्रों को अलग करना)।

कार्यप्रणाली
लेखक नेचुरल डीडक्शन (Natural Deduction) प्रणालियों का उपयोग करते हुए एक प्रमाण-सैद्धांतिक विश्लेषण (proof-theoretic analysis) नियोजित करते हैं। वे तीन विशिष्ट उदारवादी ढांचों का परीक्षण करते हैं:

1. NE (प्रावित्ज़ की प्रणाली): एक अनुमानवादी दृष्टिकोण जहाँ शास्त्रीय और सहजतावादी तर्क तटस्थ ऑपरेटरों (संयोजन, सार्वभौमिक परिमाणक, निषेध, निरर्थकता) को साझा करते हैं, लेकिन गैर-तटस्थ ऑपरेटरों (निगमन, वियोजन, अस्तित्व संबंधी परिमाणक) के भिन्न संस्करण रखते हैं।
2. ECI (बरोसो-नासिमेंटो की प्रणाली): एक सामान्यवादी दृष्टिकोण जहाँ ऑपरेटरों का एक एकल सेट उपयोग किया जाता है, लेकिन सूत्रों को लेबल $c$ (जैसे, $A^c$) के साथ लेबल किया जाता है ताकि शास्त्रीय व्यवहार को दर्शाया जा सके। यह प्रणाली सहजतावादी नेचुरल डीडक्शन पर आधारित है जिसे लेबल के लिए परिचय ($I_C$) और विलोपन ($E_C$) नियमों के साथ संवर्धित किया गया है।
3. NEK (क्रास-प्रेरित प्रणाली): प्रावित्ज़ की प्रणाली का एक रूपांतर जिसमें क्रास के अप्रकाशित कार्य पर आधारित एक शास्त्रीय संयोजन ($\land_c$) और एक शास्त्रीय सार्वभौमिक परिमाणक ($\forall_c$) शामिल है।

कार्यप्रणाली में शामिल हैं:

• इन प्रणालियों के भीतर आंतरिक ग्लिवेंको-प्रकार के प्रमेयों को परिभाषित करना (शास्त्रीय ऑपरेटरों/सूत्रों को उनके सहजतावादी समकक्षों से संबंधित करना)।
• इन आंतरिक संबंधों को सिद्ध करने के लिए व्युत्पत्ति (derivations) का निर्माण करना।
• सूत्रों को प्रणालियों के बीच मैप करने के लिए अनुवाद फलन (translation functions) ($t_{ECI}$ और $t_{NEK}$) को परिभाषित करना।
• इन प्रणालियों की निगमन समानता (deductive equivalence) की जांच करना, विशेष रूप से प्रस्तावात्मक खंड (propositional fragment) बनाम सार्वभौमिक परिमाणन वाले प्रथम-क्रम खंड (first-order fragment) में।

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

1. NE में आंतरिक ग्लिवेंको प्रमेय:
   लेखक प्रदर्शित करते हैं कि प्रावित्ज़ की प्रणाली (NE) में, जहाँ भिन्न ऑपरेटर मौजूद हैं, एक "ग्लिवेंको-प्रकार" का संबंध आंतरिक रूप से बना रहता है। किसी भी सूत्र $C$ के लिए जहाँ मुख्य ऑपरेटर शास्त्रीय है, $C \vdash_{NE} \neg\neg C^*$ होता है, जहाँ $C^*$ वह सूत्र है जिसमें शास्त्रीय ऑपरेटर को उसके सहजतावादी समकक्ष द्वारा प्रतिस्थापित किया गया है। यह शास्त्रीय वियोजन ($\lor_c$), निहितार्थ ($\to_c$), और अस्तित्व संबंधी परिमाणक ($\exists_c$) पर लागू होता है। निषेध किए गए सूत्रों के लिए एक संगत परिणाम प्राप्त होता है: $\neg C \vdash_{NE} \neg C^*$।

2. ECI में ग्लिवेंको परिणामों की तुच्छता (Triviality):
   ECI प्रणाली में, एक शास्त्रीय सूत्र $A^c$ और उसके सहजतावादी समकक्ष के बीच का संबंध संरचनात्मक रूप से तुच्छ है। प्रणाली के नियम तुरंत $A^c \vdash_{ECI} \neg\neg A$ प्रदान करते हैं। फलस्वरूप, अनुवाद $t_{ECI}$, जो $A^c$ को $\neg\neg A$ में मैप करता है, ECI में सामान्यीकरण (normalization) की समस्या को सहजतावादी तर्क की समस्या में बदल देता है। लेखक दिखाते हैं कि जबकि यह अनुवाद प्रस्तावात्मक तर्क के लिए काम करता है, यह व्युत्पत्ति में शास्त्रीय तर्क के विशिष्ट स्थान को तब तक अस्पष्ट कर देता है जब तक कि व्युत्पत्ति को व्युत्पन्न सूत्रों के "शास्त्रीय स्वभाव" को ट्रैक करने के लिए सावधानीपूर्वक पुनर्गठित न किया जाए।

3. शास्त्रीय संयोजन और NEK का मामला:
   यह शोध पत्र NEK पेश करता है, जो प्रावित्ज़ की प्रणाली में शास्त्रीय संयोजन ($\land_c$) जोड़ता है। लेखक सिद्ध करते हैं कि $\land_c$ आंतरिक ग्लिवेंको प्रमेयों को संतुष्ट करता है ($B \land_c C \vdash_{NEK} \neg\neg(B \land_i C)$)। वे यह भी दिखाते हैं कि प्रस्तावात्मक खंड में (या सार्वभौमिक परिमाणक के बिना प्रथम-क्रम तर्क में), NEK और ECI निगमन रूप से समान हैं। यह समानता एक अनुवाद $t_{NEK}$ के माध्यम से स्थापित की जाती है जो NEK में शास्त्रीय ऑपरेटरों को ECI में लेबल किए गए सूत्रों में मैप करती है।

4. सार्वभौमिक परिमाणन के साथ विचलन:
   सार्वभौमिक परिमाणन को पेश करने पर NEK और ECI के बीच निगमन समानता की विफलता एक महत्वपूर्ण परिणाम है।

• NEK में, शास्त्रीय सार्वभौमिक परिमाणक $\forall_c$ को नियमों के माध्यम से परिभाषित किया गया है जो सहजतावादी तर्क के साथ सामंजस्यपूर्ण हैं। हालाँकि, आंतरिक ग्लिवेंको प्रमेय $\forall_c$ के लिए विफल हो जाता है: $\vdash_{NEK} \forall_c x A(x)$ का अर्थ यह नहीं है कि $\vdash_{NEK} \neg\neg \forall_i x A(x)$।
• ECI में, लेबल किया गया सूत्र $(\forall x A(x))^c$ अलग व्यवहार करता है। प्रणाली के नियमों के कारण, $(\forall x A(x))^c \vdash_{ECI} \neg\neg \forall x A(x)$ सत्य है।
• लेखक इस विसंगति की व्याख्या करते हैं: NEK में, $\forall_c x A(x)$ को $\neg \exists x \neg A(x)$ के रूप में व्याख्यायित किया जाता है, जबकि ECI में, $(\forall x A(x))^c$ प्रभावी रूप से $\neg\neg \forall x A(x)$ के रूप में व्याख्यायित किया जाता है। ये सहजतावादी रूप से समकक्ष नहीं हैं। शोध पत्र तर्क देता है कि सार्वभौमिक सूत्रों के लिए ECI में ग्लिवेंको परिणामों की "तुच्छता" इस कारण उत्पन्न होती है क्योंकि लेबल $c$ एक दोहरा-निषेध (double-negation) व्याख्या को थोपता है जो अनुमानवादी दृष्टिकोण में सार्वभौमिक ऑपरेटर के अर्थपूर्ण व्यवहार के साथ संरेखित नहीं होता है।

महत्व और दावे
शोध पत्र का दावा है कि उदारवादी परिप्रेक्ष्य शास्त्रीय और सहजतावादी तर्क के बीच परस्पर क्रिया की गहरी समझ प्रदान करता है। "अनुमानवादी" (NE/NEK) और "सामान्यवादी" (ECI) दृष्टिकोणों की तुलना करके, लेखक एक सूक्ष्म लेकिन महत्वपूर्ण वैचारिक अंतर को उजागर करते हैं:

• अनुमानवादी प्रणालियाँ (Pravitz/Krauss) शास्त्रीय ऑपरेटरों के लिए विशिष्ट परिचय और विलोपन नियम प्रदान करके सीधे संयोजकों के अर्थ को बदल देती हैं।
• सामान्यवादी प्रणालियाँ (ECI) प्रमाण के स्तर को बदल देती हैं, सहजतावादी तर्क को शास्त्रीय प्रमाण के साधनों से लैस करती हैं (लेबल $c$ के माध्यम से) जो अप्रत्यक्ष रूप से ऑपरेटरों के अर्थ को बदलते हैं।

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