Hyperformalism for Relevant Modal Logics

तकनीकी सारांश: प्रासंगिक मोडल लॉजिक्स के लिए हाइपरफॉर्मलिज्म (Hyperformalism)

समस्या और संदर्भ
यह शोध पत्र हाइपरफॉर्मलिज्म (hyperformalism) के दृष्टिकोण से प्रासंगिक तर्क (relevant logics) के विश्लेषण को संबोधित करता है, जो एक ऐसा गुण है जिसमें एक तर्क गैर-समान प्रतिस्थापन (non-uniform substitutions) के तहत बंद रहता है। मानक औपचारिक तर्क (formal logics) में, परमाणु सूत्रों (atomic formulas) को समान प्रतिस्थापन (uniform substitution) के माध्यम से स्वतंत्र माना जाता है। हाइपरफॉर्मलिज्म इस स्वतंत्रता का विस्तार करता है, जिससे एक ही परमाणु के विभिन्न occurrences को स्वतंत्र माना जा सकता है यदि वे पर्याप्त भिन्न सिंथैक्टिक संदर्भों (जैसे कि अलग-अलग "गहराई" या अलग-अलग मोडल ऑपरेटर्स के अंतर्गत) में दिखाई देते हैं। जबकि हाइपरफॉर्मलिज्म को गैर-मोडल प्रासंगिक तर्कों (जैसे कि $B$ और $DR$) के लिए सफलतापूर्वक लागू किया गया है, जो मजबूत वेरिएबल शेयरिंग गुणों को प्रकट करते हैं और नए प्रासंगिक तर्क पहचानते हैं, मोडल सेटिंग्स में इसका अनुप्रयोग अभी भी कम खोजा गया है। लेखक इन तकनीकों को मोडल सेटिंग्स में विस्तारित करने का प्रयास करते हैं, विशेष रूप से यह जांचते हुए कि मोडल ऑपरेटर$\square$ की उपस्थिति गैर-समान प्रतिस्थापन और वेरिएबल शेयरिंग के साथ कैसे परस्पर क्रिया करती है।

कार्यप्रणाली (Methodology)
लेखक प्रासंगिक मोडल लॉजिक्स का विश्लेषण करने के लिए प्रमाण-सिद्धांतिक (proof-theoretic) और अर्थपूर्ण (semantic) तकनीकों के संयोजन का उपयोग करते हैं:

1. सिंथैक्टिक ढांचा (MPos): लेखक पदों (positions) का एक सेट परिभाषित करते हैं, $MPos = \{l, r, n, b\}^*c$, जहाँ $l$ और $r$ कंडिशनल्स के बाएं और दाएं शाखाओं को दर्शाते हैं, $n$ निषेध (negation) को दर्शाता है, और $b$ मोडल ऑपरेटर $\square$ के दायरे (scope) को दर्शाता है।
2. प्रतिस्थापन (Substitutions): वे $MPos$-प्रतिस्थापनों को$\sigma: MPos \times At \to L$ के रूप में परिभाषित करते हैं जो सूत्रों की संरचना का सम्मान करते हैं। महत्वपूर्ण रूप से, ये प्रतिस्थापन परमाणुओं को अलग-अलग स्थितियों पर स्वतंत्र मानते हैं, जो विशिष्ट "निष्ठा" (faithfulness) बाधाओं के अधीन होते हैं (उदाहरण के लिए, $\sigma_{xnn}(p) = \sigma_x(p)$ ताकि डबल नेगेशन गुणों को संरक्षित किया जा सके)।
3. प्रमाण-सिद्धांतिक विश्लेषण: शोध पत्र आधारभूत प्रासंगिक मोडल तर्क $B^\square$ (जो प्रासंगिक तर्क $B$ में अभिगृम $C$ और नियम $RM$ जोड़कर बनाया गया है) का विश्लेषण करता है। यह इंडक्शन (induction) के माध्यम से $MPos$-प्रतिस्थापनों के तहत क्लोजर (closure) को सिद्ध करता है।
4. विस्तार (Extensions): लेखक मोडल अभिगृमों $T, 4, K,$ और $RN$के अनुरूप$MPos$ पर तुल्यता संबंधों (equivalence relations) को परिभाषित करते हैं। वे इन परिणामों से उत्पन्न होने वाले तर्कों $B^\square_S$ और उनके संगत $MPos_S$-प्रतिस्थापनों के तहत क्लोजर की जांच करते हैं।
5. अर्थपूर्ण लक्षण वर्णन (Semantic Characterization): शास्त्रीय मोडल तर्क $K$ के सबसे बड़े $MPos$-हाइपरफॉर्मल उप-तर्क (sublogic) (जिसे $KMPos$ कहा जाता है) को चित्रित करने के लिए, लेखक निम्नलिखित को पेश करते हैं:
   • MPosK-असाइनमेंट्स: क्रिपके फ्रेम्स (Kripke frames) पर $\alpha: MPos \times W \times At \to \{0, 1\}$ फलन, जहाँ सत्य मान (truth values) स्थिति सूचकांक के आधार पर बदलते हैं।
   • एनालिटिक टैबलो (Analytic Tableaux): एक टैबलो सिस्टम जो स्थितियों ($x$), दुनियाओं ($\omega$), सूत्रों ($A$), और सत्य मानों ($i$) को ट्रैक करने वाले नोड्स $\langle x, \omega, A, i \rangle$ का उपयोग करता है।
6. कैनोनिकल मॉडल (Canonical Models): पूर्णता (completeness) को अधिकतम, विटनेस्ड (witnessed), टैबलो-संगत ब्रांचसेट्स और उनके संबंधित कैनोनिकल मॉडल्स के निर्माण के माध्यम से स्थापित किया जाता है।

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

1. $B^\square$ की MPos-हाइपरफॉर्मलिज्म:

   • प्रमेय 2.1: $B^\square$ को $MPos$-हाइपरफॉर्मल सिद्ध किया गया है। प्रमाण यह दर्शाता है कि सिस्टम के अभिगृम ($C$) और नियम ($RM$)$MPos$-प्रतिस्थापनों के तहत थ्योरडम (theoremhood) को संरक्षित करते हैं।
   • वेरिएबल शेयरिंग: इसके परिणामस्वरूप, $B^\square$ MPos-वेरिएबल शेयरिंग प्रॉपर्टी का पालन करता है। यदि $A \to B$ एक प्रमेय है, तो एक साझा चर $p$ मौजूद है जिससे $A$ और $B$ में $p$ की स्थिति $\sim_{nn}$ के तहत समान है (केवल निषेध के जोड़ों द्वारा भिन्न)।
   • परिणाम 2.6: एक विशिष्ट परिणाम यह है कि $B^\square$ में कोई भी प्रमेय $A \to B$ एक साझा चर को साझा करता है जो पूर्ववर्ती (antecedent) और परिणाम (consequent) दोनों में $\square$ ऑपरेटर्स की समान संख्या के भीतर स्थित है।

2. $B^\square$ के विस्तार:

   • प्रमेय 2.7: किसी भी उपसमुच्चय $S \subseteq \{T, 4, K, RN\}$ के लिए, तर्क $B^\square_S$ एक $MPos_S$-हाइपरफॉर्मल है, जहाँ $MPos_S$ विशिष्ट मोडल अभिगृमों (जैसे कि अभिगृम 4 के लिए $xby \sim_4 xbby$) को प्रतिबिंबित करने वाले तुल्यता संबंधों को शामिल करता है।
   • परिष्कृत वेरिएबल शेयरिंग: ये विस्तार परिष्कृत वेरिएबल शेयरिंग गुण प्रदान करते हैं। उदाहरण के लिए, $B^\square_{\{4\}}$ में, साझा चरों को एक ही "मोड" (एक्सटेंशनल बनाम इंटेंशनल) का होना चाहिए, जो प्रभावी रूप से $\square$ ऑपरेटर्स की गिनती को शेयरिंग कंडीशन से हटा देता है।

3. $KMPos$ का लक्षण वर्णन:

   • लेखक $KMPos$को शास्त्रीय मोडल तर्क$K$के सबसे बड़े$MPos$-हाइपरफॉर्मल उप-तर्क के रूप में परिभाषित करते हैं।
   • अर्थपूर्ण लक्षण वर्णन: $KMPos$को$MPosK$-असाइनमेंट्स से सुसज्जित क्रिपके फ्रेम्स में वैधता द्वारा वर्णित किया गया है।
   • टैबलो लक्षण वर्णन: $KMPos$ के लिए एक सुदृढ़ (sound) और पूर्ण टैबलो सिस्टम प्रदान किया गया है।
   • प्रमेय 3.6: $KMPos$उन सूत्रों$A$ के सेट के बराबर है जिनके लिए कुछ परमाणु, निष्पक्षता-तक-इनजेक्टिव (injective-up-to-faithfulness) प्रतिस्थापन $\iota$ के लिए, $\iota(A)$ का $K$ में एक प्रमेय है। यह पुष्टि करता है कि $KMPos$, $K$ का वह अधिकतम उपसमुच्चय है जो $MPos$-प्रतिस्थापनों के तहत बंद है।
   • वेरिएबल शेयरिंग: प्रमेय 3.9 स्थापित करता है कि $KMPos$ में वेरिएबल शेयरिंग प्रॉपर्टी है।

4. संक्रामकता (Transitivity) और $KMPos$ की प्रकृति:

   • प्रमेय 4.1: $KMPos$ संक्रामक (transitive) है। लेखक तर्क देते हैं कि प्रासंगिकता के "सिंटैक्टिक सीव" (syntactic sieve) दृष्टिकोणों के विपरीत (जो अक्सर संक्रामकता में विफल रहते हैं), $KMPos$ इन विकृतियों से बचता है क्योंकि यह एक क्लोजर प्रॉपर्टी (हाइपरफॉर्मलिज्म) द्वारा परिभाषित है, न कि शास्त्रीय प्रमेयों पर एक स्थिर फिल्टर द्वारा।

महत्व और दावे
यह शोध पत्र दावा करता है कि हाइपरफॉर्मलिज्म प्रासंगिक मोडल लॉजिक्स का विश्लेषण करने के लिए एक शक्तिशाली उपकरण है, जो $B^\square$ जैसे कमजोर सिस्टम में भी मजबूत वेरिएबल शेयरिंग गुणों को प्रकट करने में सक्षम है। हालांकि, लेखक तर्क देते हैं कि $B^\square$ इन विशेषताओं वाला सबसे मजबूत तर्क नहीं है।

प्राथमिक महत्व **$KMPos$** की शुरूआत और लक्षण वर्णन में निहित है। लेखक प्रस्ताव करते हैं कि$KMPos$प्रासंगिक मोडल लॉजिक के रूप में "सबसे बड़ा" है, इस अर्थ में कि यह$MPos$-प्रतिस्थापनों के तहत बंद शास्त्रीय$K$ का maximal उप-तर्क है। उनका दावा है कि $KMPos$, $B^\square$ और अन्य पारंपरिक प्रासंगिक मोडल लॉजिक्स की तुलना में अर्थपूर्ण और प्रमाण-सिद्धांतिक लाभ प्रदान करता है। विशेष रूप से, वे तर्क देते हैं कि $KMPos$ केवल एक "सिंटैक्टिक सीव" (शास्त्रीय प्रमेयों को केवल फिल्टर करने से परिभाषित लॉजिक्स के लिए एक नकारात्मक शब्द) नहीं है क्योंकि यह संक्रामक है और एक मजबूत क्लोजर प्रॉपर्टी द्वारा परिभाषित है।

शोध पत्र पारंपरिक प्रासंगिक मोडल लॉजिक्स (जैसे $B^\square$) के ऊपर $KMPos$को प्राथमिकता देने की चुनौती के साथ समाप्त होता है। लेखक सुझाव देते हैं कि जब तक पूर्ववर्ती को चुनने के विशिष्ट कारण न हों, शोधकर्ताओं को$KMPos$ पर विचार करना चाहिए, क्योंकि यह शास्त्रीय मोडल तर्क के maximal उप-तर्क होने के साथ-साथ वांछनीय वेरिएबल शेयरिंग विशेषताओं को बनाए रखता है। शोध पत्र स्वीकार करता है कि $KMPos$ का अभिगृम-आधारित लक्षण वर्णन एक खुला प्रश्न बना हुआ है, यह नोट करते हुए कि ऐसे लॉजिक्स ने ऐतिहासिक रूप से रिकर्सिव एक्सिओमैटाइजेशन (recursive axiomatization) का विरोध किया है।