तकनीकी सारांश: सामान्यीकृत विभाजन (Generalized Splitting) के माध्यम से इंटरपोलेशन

समस्या विवरण (Problem Statement)

यह शोध पत्र लिंडन इंटरपोलेशन प्रमेय (Lyndon interpolation theorem) के प्रमाण-सिद्धांतिक (proof-theoretic) प्रमाण को संबोधित करता है। जबकि विभिन्न तर्कशास्त्रों (शास्त्रीय, सहज ज्ञान युक्त, मोडल, रैखिक) के लिए मॉडल-सैद्धांतिक, ऑटोमेटा-सैद्धांतिक या सिंटैक्टिक विधियों का उपयोग करके इंटरपोलेशन स्थापित किया जा चुका है, सबसे सामान्य प्रमाण-सिद्धांतिक दृष्टिकोण माएहारा की विधि (Maehara's method) पर निर्भर करता है। माएहारा का यह तरीका एक कट-मुक्त (cut-free) अनुक्रम प्रमाण (sequent proof) से एक इंटरपोलेन्ट (interpolant) को कुशलतापूर्वक निकालता है। हालाँकि, माएहारा का दृष्टिकोण और इसके आधुनिक रूपांतर अक्सर मॉड्यूलरिटी (modularity) का अभाव रखते हैं; प्रमाण प्रणाली में मामूली परिवर्तन (जैसे नए नियमों को जोड़ना) अक्सर पूरे इंटरपोलेशन प्रमाण को फिर से शुरू से करने की आवश्यकता पैदा करते हैं। इसके अतिरिक्त, पारंपरिक अनुक्रम कैलकुलस (sequent calculus) मुख्य तार्किक नियमों को संरचनात्मक नियमों (जैसे वीकनिंग और कॉन्ट्रैक्शन) के साथ मिला देता है, जिससे व्युत्पत्ति के तार्किक सार को उसके संसाधन प्रबंधन पहलुओं से अलग करना कठिन हो जाता है।

लेखक एक नई विधि प्रस्तावित करता है जो अनुक्रम कैलकुलस का पूरी तरह से त्याग करती है और डीप इन्फरेंस (deep inference) तकनीकों का उपयोग करती है। लक्ष्य इंटरपोलेशन को केवल एक सूत्र के अस्तित्व के रूप में नहीं, बल्कि एक व्युत्पत्ति के संरचनात्मक अपघटन (structural decomposition) के रूप में तैयार करना है, जिससे एक अधिक मॉड्यूलर और सामान्यीकरण योग्य प्रमाण तकनीक प्राप्त की जा सके।

कार्यप्रणाली (Methodology)

प्रस्तावित कार्यप्रणाली डीप इन्फरेंस पर आधारित है, जो एक ऐसा प्रमाण-सिद्धांतिक ढांचा है जहाँ अनुमान नियम (inference rules) केवल रूट (root) पर ही नहीं, बल्कि किसी भी सूत्र के भीतर किसी भी गहराई पर लागू किए जा सकते हैं। इस दृष्टिकोण के मुख्य भाग में तीन प्रमुख तकनीकी घटक शामिल हैं:

1. सामान्यीकृत विभाजन लेम्मा (Generalized Splitting Lemma):
   डीप इन्फरेंस में मानक विभाजन लेम्मा यह बताता है कि यदि एक सूत्र $(A \otimes B) \parr K$ सिद्ध है, तो संदर्भ $K$ को $K_A$ और $K_B$ में विभाजित किया जा सकता है ताकि $A \parr K_A$ और $B \parr K_B$ सिद्ध हों। लेखक इसे एक मनमाने प्रिमिस (premise) $J$ (केवल इकाई $1$के बजाय) वाले व्युत्पत्तियों के लिए सामान्यीकृत करते हैं। विशेष रूप से, यदि$J \vdash (A \otimes B) \parr K$है, तो व्युत्पत्ति को एक "अप-फ्रैगमेंट" (एक विभाजित संदर्भ को व्युत्पन्न करने वाला) और एक "डाउन-फ्रैगमेंट" (विभाजित संदर्भ से$K$को व्युत्पन्न करने वाला) में विघटित किया जा सकता है, और साथ ही$A$और$B$के उप-व्युत्पत्तियों को अलग किया जा सकता है। महत्वपूर्ण रूप से, इस सामान्यीकरण के लिए विशिष्ट नियमों (जिन्हें$p'{\downarrow}, d'{\downarrow}, d'_{0\downarrow}$ द्वारा दर्शाया गया है) की आवश्यकता होती है जो पूर्णता (completeness) के लिए अनिवार्य नहीं हैं लेकिन अपघटन के लिए आवश्यक हैं।

2. कोर/नॉन-कोर पृथक्करण (Core/Non-Core Separation):
   प्रमाण प्रणालियों को एक कोर फ्रैगमेंट (जिसमें तार्किक नियम और विशिष्ट संरचनात्मक नियम जैसे $p'_{\downarrow}$ शामिल हैं) और एक नॉन-कोर फ्रैगमेंट (जिसमें मानक संरचनात्मक नियम जैसे वीकनिंग, कॉन्ट्रैक्शन और प्रमोशन शामिल हैं) में विभाजित किया गया है। एक प्रमुख लेम्मा यह प्रदर्शित करता है कि पूर्ण प्रणाली में किसी भी व्युत्पत्ति को एक ऐसे रूप में क्रमबद्ध किया जा सकता है जहाँ कोर फ्रैगमेंट को पहले लागू किया जाता है, जिसके बाद नॉन-कोर फ्रैगमेंट आता है, जो निष्कर्ष की मल्टीप्लिकेटिव संरचना को सुरक्षित रखता है। यह पृथक्करण इंटरपोलेशन प्रमाण को मॉड्यूलर बनाता है: कोर तार्किक विभाजन को संभालता है, जबकि नॉन-कोर संसाधन प्रबंधन को संभालता है।

3. फ्लिपिंग लेम्मा (Flipping Lemma):
   सामान्यीकृत विभाजन पर आधारित, लेखक एक "फ्लिपिंग" तंत्र पेश करते हैं। यह लेम्मा एक ऐसी व्युत्पत्ति को रूपांतरित करने की अनुमति देता है जहाँ एक "अप-फ्रैगमेंट" (कट परिचय के समान) एक "डाउन-फ्रैगमेंट" (कट उन्मूलन के समान) के ऊपर स्थित होता है, उसे एक नई व्युत्पत्ति में बदल देता है जहाँ भूमिकाएँ उलट या पुनर्गठित होती हैं। विशेष रूप से, $H$ से $F \parr K$ तक की एक व्युत्पत्ति (एक अप-फ्रैगमेंट और एक डाउन-फ्रैगमेंट के माध्यम से) एक flipped अप-फ्रैगमेंट और डाउन-फ्रैगमेंट के माध्यम से $F^\perp \otimes H$ से $K$ तक की नई व्युत्पत्ति में बदली जा सकती है, जो एक मध्यवर्ती सूत्र $I$ पेश करती है।

मुख्य योगदान (Key Contributions)

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

2. प्रमेय 1 (डिकम्पोजिशन थ्योरम):
   केंद्रीय परिणाम यह है कि प्रत्येक व्युत्पत्ति $A \vdash_X B$ को निम्नानुसार विघटित किया जा सकता है:
   $$A \xrightarrow{\delta_1} I \xrightarrow{\delta_2} B$$
   जहाँ $\delta_1$ केवल अप-फ्रैगमेंट ($X^\uparrow$) के नियमों का उपयोग करता है और $\delta_2$ केवल डाउन-फ्रैगमेंट ($X^\downarrow$) के नियमों का उपयोग करता है। सूत्र $I$ लिंडन इंटरपोलेन्ट के रूप में कार्य करता है। यह प्रमेय मानक इंटरपोलेशन प्रमेय के सुदृढ़ीकरण (स्पष्ट प्रमाण $A \vdash I$ और $I \vdash B$ प्रदान करके) और कट एलिमिनेशन प्रमेय के सामान्यीकरण के रूप में प्रस्तुत किया गया है।

3. मॉडल लॉजिक्स के लिए नवीन प्रमाण प्रणालियाँ:
   लेखक मोडल लॉजिक्स K, KT, K4, और S4 के लिए नई कट-फ्री डीप इन्फरेंस प्रमाण प्रणालियाँ पेश करते हैं। मॉडल लॉजिक के मौजूदा डीप इन्फरेंस सिस्टम को प्रस्तावित पद्धति के लिए अपर्याप्त माना गया था (विशेष रूप से आवश्यक कोर/नॉन-कोर पृथक्करण या कट एलिमिनेशन गुणों की कमी के कारण)। ये नई प्रणालियाँ इंटरपोलेशन परिणामों को रैखिक और शास्त्रीय तर्क से इन मोडल लॉजिक्स तक विस्तारित करने की अनुमति देती हैं।

4. प्रमाण की मॉड्यूलरिटी (Modularity of Proof):
   कार्यप्रणाली इंटरपोलेशन प्रमाणों के लिए एक मॉड्यूलर संरचना स्थापित करती है। क्योंकि कोर फ्रैगमेंट नॉन-कोर फ्रैगमेंट के स्वतंत्र रूप से सामान्यीकृत विभाजन लेम्मा को संतुष्ट करता है, इसलिए प्रमाण प्रणाली में मामूली परिवर्तन (जैसे नए मोडालिटीज या संरचनात्मक नियम जोड़ना) पूरे इंटरपोलेशन प्रमेय के पुन: व्युत्पत्ति की आवश्यकता नहीं डालते, बशर्ते कोर/नॉन-कोर पृथक्करण बना रहे।

परिणाम (Results)

शोध पत्र इस दृष्टिकोण की लचीलापन को निम्नलिखित पर लागू करके सफलतापूर्वक प्रदर्शित करता है:

• रैखिक तर्क (Linear Logic): मल्टीप्लिकेटिव, एडिटिव और एक्सपोनेंशियल फ्रैगमेंट (MELL) सहित प्रणालियों के लिए इंटरपोलेशन सिद्ध करना।
• शास्त्रीय तर्क (Classical Logic): यह दिखाना कि रैखिक तर्क के परिणाम एक ट्रांसलेशन के माध्यम से शास्त्रीय तर्क के परिणामों को निहित करते हैं, और SKS प्रणाली के लिए एक प्रत्यक्ष प्रमाण प्रदान करना।
• मॉडल लॉजिक्स (Modal Logics): नव-डिज़ाइन की गई प्रमाण प्रणालियों का उपयोग करके K, KT, K4, और S4 के लिए इंटरपोलेशन स्थापित करना।

सभी मामलों में, विधि एक लिंडन इंटरपोलेन्ट (प्रोपोजिशनल प्रतीकों की पोलैरिटी को संरक्षित करते हुए) प्रदान करती है और इंटरपोलेन्ट के निहितार्थों के लिए स्पष्ट व्युत्पत्तियों का निर्माण करती है। शोध पत्र यह भी नोट करता है कि अप- और डाउन-फ्रैगमेंट में विभाजन दो तरीकों से कट एलिमिनेशन को दर्शाता है: सीधे तौर पर (यदि प्रिमिस यूनिट है) और एक "फ्लिपिंग" ऑपरेशन के माध्यम से जो निहितार्थ का एक कट-फ्री व्युत्पत्ति बनाता है।

महत्व और दावे (Significance and Claims)

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

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

अंततः, यह शोध पत्र खुद को उन लॉजिक्स में इंटरपोलेशन को समझने की दिशा में एक कदम के रूप में स्थापित करता है जहाँ कोई अनुक्रम कैलकुलस मौजूद नहीं है, यह सुझाव देते हुए कि कोर/नॉन-कोर पृथक्करण अन्य तार्किक प्रणालियों में इंटरपोलेशन के अस्तित्व के लिए एक सामान्य मानदंड हो सकता है। लेखक विनम्रतापूर्वक नोट करते हैं कि यद्यपि यह विधि शक्तिशाली है, वर्तमान में यह आवश्यक अपघटन प्राप्त करने के लिए अनुमान नियमों (जैसे $p'_{\downarrow}$ का समावेश) में विशिष्ट डिज़ाइन विकल्पों पर निर्भर करती है, और प्रथम-क्रम तर्क (first-order logic) और अन्य मोडल लॉजिक्स तक इन परिणामों को विस्तारित करने के लिए आगे के कार्य की आवश्यकता है।