तकनीकी सारांश: निर्देशित प्रथम-क्रम तर्क (Directed First-Order Logic) का सैद्धांतिक अर्थशास्त्र (Doctrinal Semantics)

1. समस्या विवरण

यह शोधपत्र एक तार्किक ढांचे के भीतर निर्देशित समानता (directed equality) को औपचारिक रूप देने की चुनौती को संबोधित करता है। जबकि लॉवरे (Lawvere) के श्रेणीगत परिप्रेक्ष्य ने शास्त्रीय समानता को संकुचन (contraction) के बाएं एडजॉइंट (left adjoint) के रूप में सफलतापूर्वक अभिलक्षणित किया, यह दृष्टिकोण समरूपता (symmetry) पर निर्भर करता है। निर्देशित प्रकार सिद्धांत (directed type theory) में, जहाँ प्रकारों की व्याख्या ग्रूपॉइड्स (groupoids) के बजाय श्रेणियों (categories) या प्रीऑर्डर (preorders) के रूप में की जाती है, समानता एक असममित संबंध बन जाती है (जैसे कि एक मोर्फिज्म $a \to b$ या एक क्रम $a \le b$)।

मुख्य कठिनाई विचर्य (variance/polarity) को संभालने में निहित है। एक निर्देशित सेटिंग में, एक चर (variable) एक "नकारात्मक" स्थिति (contravariant, जैसे कि मोर्फिज्म का स्रोत/source) में या एक "सकारात्मक" स्थिति (covariant, जैसे कि लक्ष्य/target) में दिखाई दे सकता है। समानता के मानक तार्किक नियम (reflexivity और J-rule/elimination) इस संदर्भ में विफल हो जाते हैं क्योंकि वे अंतर्निहित रूप से समरूपता की धारणा रखते हैं या चरों को एक साथ दोनों ध्रुवीयताओं (polarities) में इस तरह से उपस्थित होने की अनुमति देते हैं जो समरूपता ($a \le b \vdash b \le a$) को व्युत्पन्न कर देगा, जो कि निर्देशित तर्क में अमान्य है। पिछले निर्देशित प्रकार सिद्धांत के प्रयास अक्सर इन ध्रुवीयता बाधाओं के साथ संघर्ष करते हैं, विशेष रूप से प्रमाण-अप्रासंगत तर्क (proof-irrelevant logic) के संदर्भ में (जहाँ समानता एक प्रपोजीशन है, न कि कई निवासियों वाला एक प्रकार)।

2. कार्यप्रणाली

लेखक लॉवरे के हाइपरडॉक्ट्राइन्स (hyperdoctrines) के ढांचे का सामान्यीकरण करके एक निर्देशित प्रथम-क्रम तर्क (dFOL) और इसके सैद्धांतिक अर्थशास्त्र (doctrinal semantics) को विकसित करते हैं।

वाक्य रचना (Syntax): ध्रुवीकृत संदर्भ (Polarized Contexts)

वाक्य रचना एक ध्रुवीकृत संदर्भ $[\Theta \mid \Delta \mid \Gamma]$ पेश करती है, जो चरों को उनके विचर्य के आधार पर तीन सेटों में विभाजित करती है:

• $\Theta$ (नकारात्मक): वे चर जो केवल कंट्रावेरिएंट (contravariant) स्थितियों में दिखाई देते हैं।
• $\Gamma$ (सकारात्मक): वे चर जो केवल कोवेरिएंट (covariant) स्थितियों में दिखाई देते हैं।
• $\Delta$ (डिनेटुरल/Dinatural): वे चर जो दोनों स्थितियों में दिखाई देते हैं (या जिन्हें इस रूप में माना जा सकता है)।

प्रमुख वाक्यात्मक विशेषताएं शामिल हैं:

• निर्देशित समानता ($\le_A$): एक मौलिक संबंध $s \le_A t$ जहाँ $s$ नकारात्मक संदर्भ में टाइप्ड है और $t$ सकारात्मक संदर्भ में।
• ध्रुवीकृत निहितार्थ (Polarized Implication): निहितार्थ $\psi \Rightarrow \phi$ संदर्भ की ध्रुवीयता को $\psi$ के लिए बदल देता है (इसे टर्नस्टाइल के दाईं ओर से बाईं ओर ले जाता है), जो $\psi$ के कंट्रावेरिएंट तर्क के व्यवहार को दर्शाता है।
• ध्रुवीकृत क्वांटिफायर (Polarized Quantifiers): क्वांटिफायर ($\forall^p, \exists^p$) ध्रुवीयता $p \in \{-, \Delta, +\}$ द्वारा अनुक्रमित (indexed) होते हैं ताकि बाउंड वेरिएबल के विचर्य को ट्रैक किया जा सके।
• प्रतिस्थापन नियम (Substitution Rules): एक विशिष्ट प्रतिस्थापन तंत्र (परिभाषा 2.7) ध्रुवीकृत संदर्भों में टर्म्स के री-इंडेक्सिंग को संभालता है, यह सुनिश्चित करता है कि डिनेटुरल चरों को सुसंगत रूप से प्रतिस्थापित किया जाए।

अर्थशास्त्र (Semantics): निर्देशित डॉक्ट्राइन्स (Directed Doctrines)

अर्थशास्त्र को निर्देशित डॉक्ट्राइन्स के माध्यम से कैप्चर किया गया है, जो लॉवरे के डॉक्ट्राइन्स का एक सामान्यीकरण है।

• आधार श्रेणी (Base Category): मानक श्रेणी के बजाय, आधार एक ध्रुवीकरण श्रेणी $ndp(\mathcal{C})$ है, जिसके ऑब्जेक्ट्स ट्रिपल $(\Theta, \Delta, \Gamma)$ हैं और मोर्फिज्म विचर्य संरचना का सम्मान करते हैं।
• फाइबर्ड संरचना (Fibered Structure): एक फंकटर $P: ndp(\mathcal{C})^{op} \to \mathbf{Pos}$ ध्रुवीकृत संदर्भों को फॉर्मुलों के पोसेट्स (posets) में मैप करता है।
• प्रमुख शर्तें:
  • नो-डिनेटुरल-वैरिएंस (ndv): एक शर्त जो यह सुनिश्चित करती है कि प्रेडिकेट्स में डिनेटुरल चर केवल सकारात्मक और नकारात्मक चरों के विलय से उत्पन्न होते हैं, जिससे "तीसरे" प्रकार के विचर्य को रोका जा सके।
  • सापेक्ष एडजॉन्शन्स (Relative Adjunctions): निर्देशित समानता को एक मानक बाएं एडजॉइंट के रूप में नहीं, बल्कि एक बाएं सापेक्ष एडजॉइंट (left relative adjoint) के रूप में अभिलक्षणित किया गया है, जो एक संकुचन-समान ऑपरेशन को कोलैप्स करता है जो दो विपरीत ध्रुवीयता वाले चरों को एक एकल डिनेटुरल चर में मिला देता है। यह उस वाक्यात्मक प्रतिबंध को पकड़ता है जो समरूपता को व्युत्पन्न करने से रोकता है।
  • ध्रुवीकृत निहितार्थ: एक सापेक्ष को-एडजॉइंट (relative coadjoint) के रूप में अभिलक्षणित।

3. प्रमुख योगदान

1. dFOL की वाक्य रचना: निर्देशित समानता के साथ प्रथम-क्रम तर्क का एक सटीक नेचुरल डिडक्शन सिस्टम, जिसमें डिनेटुरलिटी से प्रेरित एक कठोर ध्रुवीयता प्रणाली है। यह प्रणाली स्पष्ट रूप से निर्देशित समानता के लिए समरूपता के व्युत्पत्ति को वर्जित करती है जबकि मानक तार्किक संयोजकों को बनाए रखती है।
2. निर्देशित समानता का अभिलक्षण: यह लेख लॉवरे के "समानता एक बाएं एडजॉइंट के रूप में" को "निर्देशित समानता एक बाएं सापेक्ष एडजॉइंट के रूप में" के रूप में सामान्यीकृत करता है। यह निर्देशित समानता के लिए एक सटीक श्रेणीगत सार्वभौमिक गुण प्रदान करता है जो संबंध की विषमता को ध्यान में रखता है।
3. निर्देशित डॉक्ट्राइन्स: निर्देशित डॉक्ट्राइन्स के रूप में एक अर्थशास्त्रीय ढांचे की भूमिका। लेखक सिद्ध करते हैं कि dFOL की वाक्य रचना इस अर्थशास्त्र के संबंध में सुसंगत (sound) और पूर्ण (complete) है।
4. प्रीऑर्डर पूर्णता (Preorder Completeness): प्रीऑर्डर ($\mathbf{Preord}$) के मानक मॉडल के संबंध में dFOL के शास्त्रीय खंड (classical fragment) के लिए एक विशिष्ट पूर्णता परिणाम सिद्ध किया गया है। यह स्थापित करता है कि सभी प्रीऑर्डर मॉडलों में मान्य कोई भी निहितार्थ (entailment) वाक्य रचना में व्युत्पन्न योग्य है।
5. ध्रुवीयता का प्रबंधन: यह पेपर दिखाता है कि प्रमाण-असंगत सेटिंग में विचर्य को कैसे प्रबंधित किया जाए, जो इसे $\mathbf{Cat}$ के प्रमाण-प्रासंगिक (proof-relevant) निर्देशित प्रकार सिद्धांतों से अलग करता है, इसके लिए पोसेटल फाइब्रेशन्स (posetal fibrations) और पोसेट-वैल्यूड फाइबर्स का उपयोग करता है।

4. परिणाम

• सुसंगतता और पूर्णता (Soundness and Completeness): लेखक सिद्धांतों की श्रेणी ($\mathbf{Theory}$) और निर्देशित डॉक्ट्राइन्स की 2-श्रेणी ($\mathbf{DDoctrine}$) के बीच एक द्विपक्षीय एडजंक्शन (bi-adjunction) स्थापित करते हैं। इसका तात्पर्य है कि dFOL निर्देशित डॉक्ट्राइन्स की आंतरिक भाषा है।
• प्रीऑर्डर के लिए पूर्णता: ध्रुवीकृत संदर्भों के लिए अनुकूलित हेनकिन-शैली (Henkin-style) के निर्माण का उपयोग करते हुए, पेपर सिद्ध करता है कि dFOL का शास्त्रीय खंड प्रीऑर्डर के मॉडल के संबंध में पूर्ण है। यह निर्माण मॉडल के डोमेन को निर्देशित समानता ($\le_A$) की व्युत्पत्ति योग्यता द्वारा क्रमबद्ध क्लोज्ड टर्म्स के सेट के रूप में परिभाषित करता है।
• व्युत्पन्न नियम: सिस्टम निर्देशित समानता के ट्रांजिटिविटी (transitivity), रिफ्लेक्सिविटी (reflexivity) और कॉंग्रुएंस (congruence) के साथ-साथ ध्रुवीकृत क्वांटिफायर और निहितार्थ के बीच इंटरैक्शन नियमों का समर्थन करता है।
• प्रति-उदाहरण (Counterexamples): पेपर दर्शाता है कि समरूपता ($a \le b \vdash b \le a$) व्युत्पन्न योग्य नहीं है, और प्रीऑर्डर मॉडल ऐसे व्युत्पत्तियों के लिए काउंटरमॉडल के रूप में कार्य करता है।

5. महत्व और दावे

यह शोधपत्र लॉवरे के कार्य को आगे बढ़ाता है जो विचर्य और होम-फंक्टर्स की तर्क में भूमिका पर केंद्रित है। विशेष रूप से:

• यह प्रमाण-असंगत सेटिंग में निर्देशित समानता के लिए एक सटीक वाक्यात्मक और अर्थशास्त्रीय अभिलक्षण प्रदान करता है, जो शास्त्रीय तर्क और निर्देशित प्रकार सिद्धांत के बीच के अंतर को भरता है।
• यह सापेक्ष एडजॉन्शन्स के माध्यम से समानता को निर्देशित मामले में एक बाएं एडजॉइंट के रूप में सामान्यीकृत करता है, जो निर्देशित संरचनाओं को समझने के लिए एक नया श्रेणीगत उपकरण प्रदान करता है।
• यह प्रदर्शित करता है कि जटिल ज्यामितीय या उच्च-श्रेणीगत यांत्रिकी की आवश्यकता के बिना, ध्रुवीकृत संदर्भों के माध्यम से ध्रुवीयता को सावधानीपूर्वक प्रबंधित करके, निर्देशित तर्क को मानक तार्किक तकनीकों (जैसे हेनकिन पूर्णता) के साथ प्रबंधित किया जा सकता है।
• यह कार्य रीराइटिंग सिस्टम (rewriting systems) और निर्देशित घटनाओं (प्रक्रियाएं, संक्रमण) के बारे में तर्क करने के लिए एक आधारभूत कदम के रूप में स्थित है, जो होमोटॉपी टाइप थ्योरी के प्रमाण-प्रासंगिक दृष्टिकोणों से भिन्न है।

लेखक स्पष्ट रूप से कहते हैं कि उनका ध्यान प्रमाण-असंगत (proof-irrelevant) मामले पर है, जो रीराइटिंग लॉजिक की प्रकृति (जहाँ या तो रीराइट होता है या नहीं होता है) और पोसेटल फाइब्रेशन्स के उपयोग द्वारा न्यायसंगत है। वे पूर्ण डिपेंडेंट निर्देशित प्रकार सिद्धांत की जटिलता को हल करने का दावा नहीं करते हैं, बल्कि प्रथम-क्रम, प्रीऑर्डर-आधारित मामले के लिए एक मजबूत आधार प्रदान करते हैं।