Lindström Maximality for Fitting's Finite Heyting-Valued Modal Logic with Exact Truth Tests

तकनीकी सारांश: फिटिंग के फाईनाइट हेयटिंग-वैल्यूड मोडल लॉजिक के लिए लिंडस्ट्रॉम मैक्सिमैलिटी (Lindström Maximality)

समस्या विवरण
यह शोध पत्र कई-मूल्यों वाले मोडल लॉजिक (many-valued modal logics) की अभिव्यंजक शक्ति के लक्षण वर्णन को संबोधित करता है, विशेष रूप से एक निश्चित परिमित हेयटिंग बीजगणित ($L$) पर आधारित फिटिंग के मोडल लॉजिक को। जबकि शास्त्रीय मोडल लॉजिक और परिमित MTL-चेन्स (रैखिक क्रमबद्ध बीजगणित) पर आधारित कई-मूल्यों वाले लॉजिक के लिए लिंडस्ट्रॉम-शैली के मैक्सिमैलिटी प्रमेय मौजूद हैं, एक अनुरूप परिणाम गैर-रैखिक मामले के लिए उपलब्ध नहीं था। बडिया और ओलखोविक के पिछले कार्य ने एक विशिष्ट 'कोएटोम' (coatom) का उपयोग करके MTL-चेन्स पर मैक्सिमैलिटी स्थापित की थी, जो नामित (designated) मूल्यों को गैर-नामित मूल्यों से अलग करता है। यह दृष्टिकोण मनमाने परिमित हेयटिंग बीजगणितों के लिए विफल हो जाता है, क्योंकि उनमें रैखिकता (linearity) की कमी हो सकती है और 1 के नीचे एक एकल कोएटम नहीं होता है। केंद्रीय समस्या यह निर्धारित करना है कि क्या मारुयामा का फिटिंग लॉजिक का प्रस्तुतीकरण—जो सभी मूल्यों के लिए मूल सत्य स्थिरांकों (truth constants) के बजाय यूनरी एक्सैक्ट ट्रुथ टेस्ट ($T_\ell$) का उपयोग करता है—बिना रैखिकता की धारणा के अपने अमूर्त विस्तारों (abstract extensions) के बीच मैक्सिमैलिटी बनाए रखता है।

कार्यप्रणाली
लेखक शास्त्रीय और कई-मूल्यों वाले लिंडस्ट्रॉम प्रमेयों से अनुकूलित एक मॉडल-थ्योरेटिक दृष्टिकोण अपनाता है। कार्यप्रणाली इस प्रकार है:

1. आधार लॉजिक को परिभाषित करना: क्रिस्प क्रिप्के फ्रेम्स (crisp Kripke frames) पर मारुयामा के फिटिंग लॉजिक ($FML_L$) का उपयोग करना, जहाँ सूत्र एक परिमित हेयटिंग बीजगणित $L$ में मान लेते हैं। भाषा में एक्सैक्ट ट्रुथ टेस्ट $T_\ell$ शामिल हैं, जहाँ $T_\ell \phi$ का मान 1 होगा यदि और केवल यदि $\phi$ का मान $\ell$ है।
2. व्युत्पन्न बुलियन ऑपरेटरों को पेश करना: श्रृंखला-निर्भर पृथक्करण तंत्र को बदलने के लिए, लेखक बुलियन-मूल्य वाले टेस्ट को परिभाषित करता है:
   • $D\phi := T_1\phi$ (सत्य यदि $\phi$ नामित/1 के बराबर है)।
   • $N\phi := T_0(T_1\phi)$ (सत्य यदि $\phi$ गैर-नामित/1 के बराबर नहीं है)।
   • एक व्युत्पन्न अस्तित्वगत मोडैलिटी (existential modality) $\Diamond_1 \phi := T_0(\Box N\phi)$, जो एक सुलभ अवस्था (accessible state) की अभिव्यक्ति करता है जहाँ $\phi$ का मान 1 है।
3. अमूर्त विस्तार (Abstract Extensions): शोध पत्र एक ऐसे अमूर्त विस्तार $\mathcal{L}$ पर विचार करता है जो तीन मॉडल-थ्योरेटिक गुणों को संतुष्ट करता है: कॉम्पैक्टनेस (Compactness), टार्स्की यूनियन प्रॉपर्टी (Tarski Union Property), और बिसिम्यूलेशन (bisimulation) के तहत स्ट्रॉन्ग इनवेरिएंस (strong invariance)।
4. सैचुरेशन और अनरैवलिंग (Saturation and Unravelling): प्रमाण अनरैवलिंग तकनीकों का उपयोग करके सैचुरेटेड एलिमेंट्री एक्सटेंशन का निर्माण करता है। यह "सक्सेसर टाइप्स" (successor types) को परिभाषित करने के लिए व्युत्पन्न मोडैलिटी $\Diamond_1$ का लाभ उठाता है और इन प्रकारों को साकार करने वाले मॉडल बनाने के लिए कॉम्पैक्टनेस और टार्स्की यूनियन गुणों का उपयोग करता है।
5. निर्णय लेम्मा (The Decision Lemma): एक महत्वपूर्ण चरण "डिसीजन लेम्मा" है जो किसी भी काल्पनिक नए सूत्र को आधार लॉजिक से अलग करने के लिए जोड़ी $(D\psi, N\psi)$ का उपयोग करता है। यह "1 के तत्काल पूर्ववर्ती" वाले तर्क को प्रतिस्थापित करता है जिसका उपयोग चेन-आधारित प्रमाणों में किया जाता था।

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

• लिंडस्ट्रॉम मैक्सिमैलिटी थ्योरम: प्राथमिक परिणाम (प्रमेय 1) यह है कि किसी भी निश्चित परिमित हेयिंग बीजगणित $L$ के लिए, मारुयामा का फिटिंग लॉजिक, उन सभी अमूर्त विस्तारों के बीच 1-अभिव्यक्ति शक्ति के संबंध में मैक्सिमल है जो कॉम्पैक्ट, टार्स्की यूनियन प्रॉपर्टी रखते हैं, और बिसिम्यूलेशन के तहत स्ट्रॉन्गली इनवेरिएंट हैं।
• रैखिकता धारणा को हटाना: शोध पत्र सफलतापूर्वक रैखिक क्रमबद्ध बीजगणितों (MTL-chains) के प्रतिबंधात्मक सेटिंग से मनमाने परिमित हेयिंग बीजगणितों तक मैक्सिमैलिटी परिणाम का सामान्यीकरण करता है। प्रमाण यह दर्शाता है कि एक्सैक्ट ट्रुथ टेस्ट पर्याप्त पृथक्करण शक्ति प्रदान करते हैं, जिसके लिए रैखिक क्रम या विशिष्ट कोएटम की आवश्यकता नहीं होती है।
• एक्सैक्ट-वैल्यू डिफिनेबिलिटी (Exact-Value Definability): मैक्सिमैलिटी प्रमेय के एक परिणाम के रूप में (अनुवर्ती 1), शोध पत्र यह सिद्ध करता है कि किसी विस्तार $\mathcal{L}$ में किसी सूत्र $\phi$ और किसी मान $\ell \in L$ के लिए, वे पॉइंटेड मॉडल्स जहाँ $\phi$ का सटीक मान $\ell$ है, आधार लॉजिक में एक सूत्र द्वारा परिभाषित हैं। विशेष रूप से, "एक्सैक्ट-वैल्यू फाइबर" (exact-value fibre) परिभाषित है, हालांकि शोध पत्र यह नोट करता है कि इसका अर्थ यह नहीं है कि $FML_L$ में एक एकल सूत्र मौजूद है जो $\phi$ के पूर्ण $L$-वैल्यूड सिमेंटिक्स को पुनरुत्पादित कर सके।
• सैचुरेटेड मॉडल्स के लिए हेनेसी-मिलनर प्रॉपर्टी: शोध पत्र स्थापित करता है कि $FML_L$-सैचुरेटेड मॉडल्स के लिए, मोडल इक्विवेलेंस (modal equivalence) बिसिम्यूलेशन को निहित करता है, जो इस कई-मूल्यों वाले परिवेश में मानक हेनेसी-मिलनर घटनाओं का विस्तार करता है।

महत्व और दावे
शोध पत्र गैर-रैखिक बीजगणितों पर कई-मूल्यों वाले मोडल लॉजिक के अभिव्यंजक सीमाओं के संबंध में साहित्य के अंतराल को हल करने का दावा करता है। यह प्रदर्शित करके कि एक्सैक्ट ट्रुथ टेस्ट ($T_\ell$) द्वारा व्युत्पन्न बुलियन निर्णय जोड़े ($D\phi, N\phi$) नामित से गैर-नामित मूल्यों को अलग करने में सक्षम हैं, लेखक दिखाता है कि संरचनात्मक बाधाएं (विशेष रूप से रैखिकता) लिंडस्ट्रॉम मैक्सिमैलिटी के लिए आवश्यक नहीं हैं।

इसका महत्व निम्नलिखित में निहित है:

1. सामान्यीकरण: लिंडस्ट्रॉम प्रमेयों को परिमित चेन्स के प्रतिबंधात्मक सेटिंग से व्यापक श्रेणी के परिमित हेयिंग बीजगणितों तक विस्तारित करना।
2. तंत्र की पहचान: गैर-रैखिक सेटिंग्स में मान पृथक्करण और सैचुरेशन तर्कों के लिए एक्सैक्ट ट्रुथ टेस्ट से प्राप्त बुलियन-वैल्यूड टेस्ट को महत्वपूर्ण तंत्र के रूप में पहचानना।
3. परिभाषा क्षमता (Definability): यह स्थापित करना कि आधार लॉजिक किसी भी "उचित" विस्तार में किसी सूत्र के सटीक-मान फाइबर को परिभाषित करने के लिए पर्याप्त अभिव्यंजक है, जो मारुयामा के प्रस्तुतीकरण की मजबूती को पुष्ट करता है।

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