The proof theory and semantics of second-order (intuitionistic) tense logic

तकनीकी सारांश: द्वितीय-क्रम (अंतर्ज्ञानवादी) काल तर्क (Tense Logic) का प्रमाण सिद्धांत और अर्थशास्त्र

समस्या और प्रेरणा
यह शोध पत्र शास्त्रीय और अंतर्ज्ञानवादी (intuitionistic) दोनों आधारों पर द्वितीय-क्रम काल तर्क के मौलिक विकास को संबोधित करता है। जबकि द्वितीय-क्रम तर्क गणितीय और गणनात्मक तर्क के लिए एक मानक उपकरण है, इसके धातु-तार्किक (metalogical) आधारों, विशेष रूप से प्रमाण सिद्धांत और अर्थशास्त्र (semantics) के संबंध में, महत्वपूर्ण चुनौतियाँ पेश की हैं। अंतर्ज्ञानवादी मोडल लॉजिक में एक विशिष्ट कठिनाई डायमंड मोडैलिटी ($\Diamond$) के उपयुक्त स्वयंसिद्धीकरण (axiomatization) के संबंध में सर्वसम्मति का अभाव है, जिसे शास्त्रीय तर्क में बॉक्स ($\Box$) के संदर्भ में परिभाषित नहीं किया जा सकता है। विभिन्न प्रस्ताव मौजूद हैं (जैसे, CK, IK), लेकिन उनमें अक्सर स्वैच्छिक चयनों (arbitrary choices) का समावेश होता है।

लेखक द्वितीय-क्रम परिमाणीकरण (quantification) का उपयोग करके एक एकीकृत दृष्टिकोण प्रस्तावित करते हैं। एक प्रमुख अवलोकन यह है कि द्वितीय-क्रम अंतर्ज्ञानवादी तर्क में, सकारात्मक संयोजक (positive connectives) को नकारात्मक खंड (negative fragment) से परिभाषित किया जा सकता है। विशेष रूप से, शोध पत्र यह प्रदर्शित करता है कि डायमंड मोडैलिटी (और उससे जुड़े सिद्धांत) को केवल बॉक्स ($\Box$) और बैकवर्ड बॉक्स ($\blacksquare$) का उपयोग करके पुनः प्राप्त किया जा सकता है, बशर्ते कि फॉरवर्ड और बैकवर्ड दोनों मोडैलिटी (काल तर्क) शामिल हों। यह $\Diamond A$ को $\forall X(\Box(A \to \blacksquare X) \to X)$ के रूप में परिभाषित करने की अनुमति देता है, जिससे स्वैच्छिक स्वयंसिद्धीकरण से बचा जा सके।

कार्यप्रणाली (Methodology)
लेखक द्वितीय-क्रम काल तर्क के लिए तीन समानांतर परिभाषाएँ विकसित करते हैं:

1. स्वयंसिद्ध (Axiomatic): प्रणालियाँ $Kt2$(शास्त्रीय) और$IKt2$ (अंतर्ज्ञानवादी) को परिभाषित किया गया है। ये सामान्य मोडैलिटी और काल युग्मों (tense pairs) के लिए एडजंक्शन स्वयंसिद्धों के साथ द्वितीय-क्रम प्रस्तावात्मक तर्क का विस्तार करते हैं। महत्वपूर्ण रूप से, इनमें एक पूर्ण बोध स्वयंसिद्ध (comprehension axiom) शामिल है, जो इम्प्रेडिकेटिव (impredicative) परिभाषाओं की अनुमति देता है।
2. अर्थशास्त्रीय (Semantic): शोध पत्र अंतर्ज्ञानवादी मामले के लिए (द्वि)संबंधी अर्थशास्त्र (birelational semantics) और शास्त्रीय मामले के लिए संबंधपरक अर्थशास्त्र प्रस्तुत करता है। इन संरचनाओं में एक आंशिक क्रम (अंतर्ज्ञानवाद के लिए) और एक सुलभता संबंध (accessibility relation) शामिल है। एक केंद्रीय विशेषता "बोधपूर्णता" (comprehensiveness) की आवश्यकता है, जहाँ समुच्चयों का डोमेन सभी सूत्रों के विस्तार (extensions) को सम्मिलित करता है, जो प्रभावी रूप से बोध स्वयंसिद्ध को मॉडल करता है। लेखक "प्रेडिकेट संरचनाएं" (जहाँ विश्व शास्त्रीय मोडल मॉडल होते हैं) भी परिभाषित करते हैं और उन्हें द्विर संबंधपरक संरचनाओं के समकक्ष दिखाते हैं।
3. प्रमाण-सैद्धांतिक (Proof-Theoretic): लेबल वाले सिक्वेंट कैलकुली ($\ell Kt2$ और $\ell IKt2$) प्रस्तावित किए गए हैं। ये सिस्टम अर्थशास्त्र को आंतरिक बनाने के लिए विश्व लेबल और संबंधपरक परमाणुओं का उपयोग करते हैं। अंतर्ज्ञानवादी मामले के लिए, एक मध्यवर्ती मल्टी-सक्सेडेंट कैलकुलस ($m\ell IKt2$) पेश किया गया है ताकि प्रमाण खोज (proof search) तर्कों को सुगम बनाया जा सके, जिसे एकल-सक्सेडेंट संस्करण पर संरक्षित (conservative) दिखाया गया है।

मुख्य तकनीकी रणनीति यह सिद्ध करना है कि ये तीन परिभाषाएँ मेल खाती हैं। इसे स्वयंसिद्ध प्रमाण योग्यता, अर्थशास्त्रीय वैधता और प्रमाण-सैद्धांतिक व्युत्पत्ति को जोड़ने वाले "ग्रैंड टूर्स" के रूप में देखा जा सकता है। पूर्णता प्रमाणों (completeness proofs) के लिए श्यूट (Schütte) के सेमी-वैल्यूएशन और प्रावित्ज़ (Prawitz) की 'संभावित मान' (possible values) की अवधारणा से अनुकूलित एक प्रमाण-खोज तर्क पर निर्भर किया जाता है, जो इम्प्रेडिकेटिविटी की बाधाओं को दूर करता है।

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

• द्वितीय-क्रम परिमाणीकरण के माध्यम से डायमंड्स की परिभाषा: शोध पत्र स्थापित करता है कि काल मोडैलिटी की उपस्थिति में, डायमंड मोडैलिटी को द्वितीय-क्रम अंतर्ज्ञानवादी तर्क में $\Diamond A \iff \forall X(\Box(A \to \blacksquare X) \to X)$ के रूप में परिभाषित किया जा सकता है। यह फिशर सर्वी और सिम्पसन के $IK$तथा इवाल्ड के$IKt$ के सिद्धांत को बिना किसी स्वैच्छिक स्वयंसिद्ध चयन के पुनः प्राप्त करता है।
• सुसंगतता और पूर्णता (Soundness and Completeness):
  • अंतर्ज्ञानवादी: प्रणाली $IKt2$ को व्यापक द्विर संबंधपरक अर्थशास्त्र के संबंध में सुसंगत और पूर्ण सिद्ध किया गया है (मुख्य प्रमेय 3.3)।
  • शास्त्रीय: प्रणाली $Kt2$ को व्यापक संबंधपरक अर्थशास्त्र के संबंध में सुसंगत और पूर्ण सिद्ध किया गया है (मुख्य प्रमेय 3.14)।
• कट-स्वीकार्यता (Cut-Admissibility): शोध पत्र लेबल वाले सिक्वेंट कैलकुली $\ell Kt2$ और $\ell IKt2$ के लिए कट-स्वीकार्यता स्थापित करता है (मुख्य प्रमेय 4.2)। इसे एक प्रमाण-खोज तर्क के माध्यम से प्राप्त किया जाता है जो विफल प्रमाण खोजों से काउंटरमॉडल का निर्माण करता है।
  • शास्त्रीय मामले के लिए, तर्क श्यूट के सेमी-वैल्यूएशन और प्रावित्ज़ के संभावित मानों को एक संबंधपरक काउंटरमॉडल निकालने के लिए अनुकूलित करता है।
  • अंतर्ज्ञानवादी मामले के लिए, यह अधिक जटिल है, जिसमें क्रिप्के मॉडलों के आंशिक क्रम को संभालने के लिए एक प्रमाण-खोज वृक्ष (शाखा के बजाय) का निर्माण आवश्यक है, जो अंततः एक प्रेडिकेट मॉडल काउंटरमॉडल प्रदान करता है।
• लेबल वाले प्रमाणों की स्वयंसिद्ध सुसंगतता: शोध पत्र लेबल वाले प्रमाणों से स्वयंसिद्ध प्रमाणों में एक अनुवाद प्रदान करता है (प्रमेय 7.1), जो तुल्यता के चक्र को पूरा करता है। इसमें लेबल वाले पोलिट्री सिक्वेंट्स को काल सूत्रों (tense formulas) के रूप में व्याख्या करना और यह दिखाना शामिल है कि प्रत्येक निष्कर्ष नियम स्वयंसिद्ध प्रणाली में एक स्वीकार्य नियम के अनुरूप है।
• शास्त्रीय-अंतर्ज्ञानवादी संबंध: शोध पत्र एक नकारात्मक अनुवाद (प्रमेय 8.2) के माध्यम से शास्त्रीय द्वितीय-क्रम काल तर्क ($Kt2$) को अंतर्ज्ञानवादी प्रणाली ($IKt2$) में एम्बेड करने की क्षमता स्थापित करता है, जो गोडेल-जेंटन अनुवाद के समान है।

महत्व
शोध पत्र का दावा है कि यह द्वितीय-क्रम काल तर्क के लिए एक मजबूत, एकीकृत आधार प्रदान करता है। यह प्रदर्शित करके कि स्वयंसिद्ध, अर्थशास्त्रीय और प्रमाण-सैद्धांतिक परिभाषाएँ मेल खाती हैं, यह चुने गए न्यूनतम स्वयंसिद्धीकरण को मान्य करता है। कार्य स्वैच्छिक स्वयंसिद्धों के बिना एक अंतर्ज्ञानवादी सेटिंग में सकारात्मक मोडैलिटी को परिभाषित करने की विशिष्ट चुनौती को संबोधित करता है, जो द्वितीय-क्रम परिमाणीकरण की अभिव्यंजक शक्ति का लाभ उठाता है।

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