A Proof-theoretic Semantics for Intuitionistic Linear Logic

समस्या
प्रमाण-सिद्धांतिक अर्थशास्त्र (P-tS) अर्थ को सत्य के बजाय प्रमाण की धारणा के माध्यम से तार्किक अभिव्यक्तियों को प्रदान करने का लक्ष्य रखता है। जहाँ सैंडक्विस्ट ने सहज बोधनात्मक प्रस्तावक तर्क (IPL) के लिए एक बेस-एक्सटेंशन अर्थशास्त्र (B-eS) सफलतापूर्वक स्थापित किया, और घेओर्गियस, गु, और पिम ने इसे सहज बोधनात्मक रैखिक तर्क (IMLL) के गुणात्मक खंड तक विस्तारित किया, वहीं पूर्ण सहज बोधनात्मक रैखिक तर्क (ILL) के लिए एक पूर्ण P-tS मिलना कठिन बना रहा। प्राथमिक चुनौती ILL की उप-संरचनात्मक प्रकृति में निहित है, जो सामान्य कमजोरी (weakening) और संकुचन (contraction) को वर्जित करती है, और इसमें योगात्मक संयोजक (additive connectives) तथा घातांकीय मोडालिटी (exponential modality, !) का समावेश है। मौजूदा दृष्टिकोण इस ढांचे के भीतर इन विशेषताओं के बीच परस्पर क्रिया को संभालने में संघर्ष करते हैं। विशेष रूप से, एक ऐसा समर्थन संबंध (support relation) परिभाषित करना जो ILL की संसाधन-संवेदनशील प्रकृति का सम्मान करता हो और 'बैंग' (!) मोडालिटी के अनुमानात्मक विषय-वस्तु को सही ढंग से पकड़ता हो—जो कि एक सख्त व्युत्पत्ति की आवश्यकता वाला मोडाल ऑपरेटर है—महत्वपूर्ण कठिनाइयाँ प्रस्तुत करता है। इसके अलावा, ILL के मानक प्राकृतिक अपादान (natural deduction) प्रणालियाँ अक्सर संदर्भ साझाकरण (additivity) और प्रेरकों की संख्या की परिवर्तनशील मात्रा के संबंध में 'एड-हॉक' (ad-hoc) पक्ष शर्तों पर निर्भर करती हैं, जिन्हें B-eS में आवश्यक गैर-स्कीमेटिक संरचना के भीतर औपचारिक रूप देना कठिन है।

कार्यप्रणाली
यह शोध पत्र दो मुख्य तकनीकी बाधाओं को संबोधित करके ILL के लिए एक नवीन बेस-एक्सटेंशन अर्थशास्त्र प्रस्तावित करता है: बिना स्कीमेटिक संदर्भ मेटावेरिएबल्स के प्राकृतिक अपादान नियमों का औपचारिक रूप देना, और योगात्मकता (additivity) एवं मोडालिटी को संभालने वाले समर्थन संबंध को परिभाषित करना।

1. प्राकृतिक अपादान का पुनर्गठन: लेखक "योगात्मक बॉक्स" (जिसे कर्ली ब्रेसेस {...} द्वारा दर्शाया गया है) और "मोडाल बॉक्स" (जिसे सिमेंटिक ब्रैकेट J...K द्वारा दर्शाा गया है) का उपयोग करके प्राकृतिक अपादान प्रणाली NILL के लिए एक नया सिंटैक्स पेश करते हैं।

   • योगात्मक बॉक्स (Additive Boxes): ये साझा संदर्भों को चिह्नित करते हैं, जिससे प्रणाली योगात्मक संयोजकों (जैसे & और ⊕) और परिवर्तनशील प्रेरकों वाले नियमों (जैसे ⊤I और 0E) को बिना किसी मनमाने संदर्भ मेटावेरिएबल पर निर्भर रहे, प्रदर्शित कर सकती है। यह एक व्यवस्थित उपचार की अनुमति देता है जहाँ बॉक्स के भीतर की व्युत्पत्तियाँ खुले धारणाओं के एक ही मल्टीसेट को साझा करती हैं।
   • मोडाल बॉक्स (Modal Boxes): इनका उपयोग प्रमोशन नियम (Prom) को चित्रित करने के लिए किया जाता है। नियम को इस प्रकार पुनर्गोषित किया गया है कि निष्कर्ष उस संदर्भ से अनुसरण करता है जहाँ सभी धारणाएँ उन नियमों के निष्कर्ष हैं जिनमें उनके ऊपर केवल मोडाल बॉक्स शामिल हैं। यह ! मोडालिटी के लिए सख्त व्युत्पत्ति की आवश्यकता को उसके संरचनात्मक परिभाषा में ! संयोजक का स्पष्ट संदर्भ दिए बिना पकड़ता है।
   • लेखक यह सिद्ध करते हैं कि यह नई प्रणाली मानक अनुक्रम-शैली (sequent-style) वाली NILL के समकक्ष है (प्रमेय 2.7)।

2. परमाणु व्युत्पत्ति और समर्थन संबंध:

   • परमाणु नियम (Atomic Rules): अर्थशास्त्र परमाणु नियमों को एक मल्टीसेट योगात्मक बॉक्स, एक एकल योगात्मक बॉक्स (निष्कर्ष), और एक परमाणु (atom) के त्रिक (triples) के रूप में परिभाषित करता है। यह पुनर्गठित प्राकृतिक अपादान नियमों की संरचना को दर्शाता है।
   • बेस एक्सटेंशन (Base Extension): एक बेस $B$ ऐसे परमाणु नियमों का सेट है। व्युत्पत्ति संबंध $\vdash_B$ को संदर्भों के गुणात्मक विभाजन (multiplicative splitting) और बॉक्स संरचना के माध्यम से योगात्मक साझाकरण को संभालते हुए, आगमनात्मक (inductively) रूप से परिभाषित किया गया है।
   • समर्थन संबंध ($\Vdash_B^L$): कोर सिमेंटिक परिभाषा समर्थन संबंध को ILL के लिए विस्तारित करती है। महत्वपूर्ण रूप से, घातांकीय मोडालिटी !ϕ के लिए खंड केवल एक संरचनात्मक नियम के रूप में नहीं, बल्कि बेस एक्सटेंशन के माध्यम से $\phi$ की वैधता पर एक शर्त के रूप में परिभाषित किया गया है। विशेष रूप से, $\Vdash_B^L !\phi$ तब सत्य होता है जब किसी भी विस्तार $C$ के लिए, यदि $\phi$ एक "$C$ का प्रमेय" है (अर्थात, सभी $D \supseteq C$ के लिए $\Vdash_D^\emptyset \phi$), तो उस संसाधन का उपयोग किया जा सकता है।
   • मोडालिटी को संभालना: शोध पत्र बेस में "स्थिर परमाणुओं" (persistent atoms) की अवधारणा पेश करता है, जो !ϕ के रूप में सूत्रों के अनुरूप होते हैं। ये परमाणु ! के संबंध में भूमिका निभाते हैं, जो मानक धारणाओं और उन धारणाओं के बीच अंतर करने की अनुमति देते हैं जिन्हें कमजोर या संकुचित किया जा सकता है।

मुख्य योगदान

• ILL के लिए एक पूर्ण B-eS: यह शोध पत्र पहला बेस-एक्सटेंशन अर्थशास्त्र प्रस्तुत करता है जो पूर्ण सहज बोधनात्मक रैखिक तर्क (ILL) को कवर करता है, जिसमें योगात्मक संयोजक और घातांकीय मोडालिटी शामिल हैं।
• योगात्मकता का व्यवस्थित उपचार: योगात्मक बॉक्स पेश करके, लेखक बिना एड-हॉक पक्ष शर्तों या स्पष्ट संदर्भ मेटावेरिएबल्स के, प्राकृतिक अपादान में संदर्भ-साझाकरण और परिवर्तनशील-प्रेरक नियमों को संभालने का एक तरीका प्रदान करते हैं। यह अनुमान चित्र (inference figures) के अधिक स्वच्छ और समान प्रतिनिधित्व की पेशकश करता है।
• मोडाल बॉक्स लक्षण वर्णन: मोडाल बॉक्स का उपयोग करके प्रमोशन नियम का पुनर्गठन घातांकीय मोडालिटी के लिए एक संरचनात्मक लक्षण वर्णन प्रदान करता है जो विशिष्ट संयोजक सिंटैक्स से स्वतंत्र है, जिससे बेस-एक्सटेंशन ढांचे में इसके एकीकरण की सुविधा मिलती है।
• ! का अनुमानात्मक विवरण: शोध पत्र ! संयोजक के अनुमानात्मक विषय-वस्तु पर विस्तृत चर्चा प्रदान करता है। यह तर्क देता है कि अर्थशास्त्र ! की मोडाल प्रकृति को पकड़ता है क्योंकि यह इसे बेस एक्सटेंशन के माध्यम से सूत्रों की वैधता पर एक शर्त के रूप में मानता है, जो प्रभावी रूप से मोडालिटी के "नेसेसिटेशन" (necessitation) पहलू को आंतरिक बनाता है।
• सुदृढ़ता (Soundness) और पूर्णता (Completeness): शोध पत्र सिद्ध करता है कि प्रस्तावित अर्थशास्त्र NILL के प्राकृतिक अपादान प्रणाली के सापेक्ष सुदृढ़ और पूर्ण दोनों है। पूर्णता प्रमाण एक "सिमुलेशन बेस" $N$ का निर्माण करके पूरा किया जाता है जहाँ परमाणु नियम NILL के अनुमान नियमों की नकल करते हैं, और एक 'फ्लैटनिंग मैप' ILL सूत्रों को परमाणुओं में अनुवादित करता है।

परिणाम

• प्रमेय 2.7: मानक अनुक्रम-शैली व्युत्पत्ति ($\vdash$) और नई बॉक्स-आधारित व्युत्पत्ति ($\vdash^*$) के बीच समानता स्थापित करता है।
• प्रमेय 5.1 (सुदृढ़ता): सिद्ध करता है कि यदि एक अनुक्रम NILL में सिद्ध है, तो वह प्रस्तावित अर्थशास्त्र में मान्य है ($\Gamma \vdash \phi \implies \Gamma \Vdash \phi$)।
• प्रमेय 6.1 (पूर्णता): सिद्ध करता है कि यदि एक अनुक्रम अर्थशास्त्र में मान्य है, तो वह NILL में सिद्ध है ($\Gamma \Vdash \phi \implies \Gamma \vdash \phi$)।
• प्रमेय 4.15: यह प्रदर्शित करता है कि ! वाली धारणाओं को संभालने के लिए उपयोग किया जाने वाला विशिष्ट (Inf) खंड एक अधिक सामान्य (Gen-Inf) खंड के समकक्ष है, जो मोडाल हाइपोथीसिस के विशिष्ट उपचार को मान्य करता है।
• कोरोलरी 4.11 और 4.12: समर्थन संबंध के साथ ! की परस्पर क्रिया के संबंध में संरचनात्मक गुणों को स्थापित करते हैं, यह दिखाते हुए कि यदि $\phi$ मान्य है, तो !ϕ मान्य है, और !Γ, !ϕ का समर्थन करता है यदि वह ϕ का समर्थन करता है।

महत्व
यह शोध पत्र दावा करता है कि यह IPL और IMLL से पूर्ण ILL तक बेस-एक्सटेंशन दृष्टिकोण का विस्तार करके P-tS में एक महत्वपूर्ण अंतराल को भरता है। लेखक नोट करते हैं कि जहाँ घेओर्गियस, गु, और पिम ने गुणात्मक खंड को सफलतापूर्वक संभाला, वहीं योगात्मक तत्वों और घातांकीय मोडालिटी को जोड़ने के लिए पर्याप्त नए तंत्र की आवश्यकता थी। यह कार्य मोडालिटी के प्रति इसके अंतर्निहित प्रमाण-सिद्धांतिक दृष्टिकोण के लिए महत्वपूर्ण है, जो ! संयोजक को केवल एक संरचनात्मक नियम के रूप में नहीं, बल्कि बेस-एक्सटेंशन ढांचे के भीतर सूत्रों की वैधता पर एक शर्त के रूप में समझने का एक तरीका प्रदान करता है। लेखक विनम्रतापूर्वक स्वीकार करते हैं कि प्रमोशन नियम और योगात्मकता को संभालने के लिए समाधान "कुछ हद तक जटिल" (convoluted) है, लेकिन अनुमान चित्रों के एक स्वच्छ, व्यवस्थित प्रतिनिधित्व को प्राप्त करने के लिए आवश्यक है। इसके अतिरिक्त, शोध पत्र इस बात पर प्रकाश डालता है कि सैंडक्विस्ट के IPL अर्थशास्त्र को सीधे इस ILL ढांचे में एम्बेड करना कठिन है, जो दोनों के बीच मैपिंग के सामान्यीकरण को भविष्य के अध्ययन के लिए एक खुला प्रश्न छोड़ देता है। यह कार्य सुझाव देता है कि P-tS में मोडालिटी के लिए वर्तमान दृष्टिकोण को गहरे आध्यात्मिक या संरचनात्मक अंतर्दृष्टि की आवश्यकता हो सकती है जिसे अभी संबोधित किया जाना शुरू ही किया गया है।