S2S (गणित): Difference between revisions

'''गणित''' में, '''S2S''' दो उत्तराधिकारियों वाला मोनैडिक द्वितीय क्रम सिद्धांत होता है। यह ज्ञात सबसे अभिव्यंजक प्राकृतिक निर्णायक सिद्धांतों में से एक होता है, जिसमें S2S में कई निर्णायक सिद्धांतों की व्याख्या की जा सकती है। इसकी निर्णायकता 1969 में माइकल ओ. राबिन द्वारा सिद्ध की गई थी।<ref>{{Cite journal |title=अनंत पेड़ों पर दूसरे क्रम के सिद्धांतों और ऑटोमेटा की निर्णायकता|last=Rabin |first=Michael |journal=Transactions of the American Mathematical Society |volume=141 |date=1969 |url=https://www.ams.org/journals/tran/1969-141-00/S0002-9947-1969-0246760-1/S0002-9947-1969-0246760-1.pdf}}</ref>

S2S की प्रथम क्रम की वस्तुएं परिमित बाइनरी स्ट्रिंग होती हैं। दूसरे क्रम की वस्तुएं परिमित बाइनरी स्ट्रिंग्स के अनैतिक समुच्चय (या एकात्मक विधेय) होता हैं। इस प्रकार S2S में स्ट्रिंग्स पर फलन s→s0 और s→s1होता हैं, और विधेय s∈S (प्रतिरूप, S(s)) का अर्थ है कि स्ट्रिंग s समुच्चय S से संबंधित होती है।

* [[क्लेन स्टार]] का उपयोग करते हुए, सभी बाइनरी स्ट्रिंग्स के समुच्चय को {0,1} द्वारा प्रदर्शित किया जाता है।

* सूत्र जटिलता के लिए, स्ट्रिंग्स पर उपसर्ग संबंध को सामान्यतः पहले क्रम के रूप में माना जाता है। इसकेअतिरिक्त, सभी सूत्र Δ¹₂ के समतुल्य नहीं होंगे।<ref>{{Cite conference |title=बाइनरी ट्री के मोनैडिक लॉजिक की संरचना पर|last1=Janin |first1=David |last2=Lenzi |first2=Giacomo |url=https://hal.archives-ouvertes.fr/hal-00676277 |conference=MFCS 1999 |doi=10.1007/3-540-48340-3_28}}</ref>

* एक निश्चित k के लिए, स्ट्रिंग से k तक एक फलन (अर्थात् k के नीचे की प्राकृतिक संख्या) को एक समुच्चय द्वारा एनकोड किया जा सकता है। इसके अतिरिक्त, s,t ⇒ s01t{{prime}} जहां T{{prime}} t के प्रत्येक वर्ण को दोगुना कर देता है, और s ⇒ {s01t{{prime}}: t∈{0,1}^*} S2S निश्चित होता है। इसके विपरीत, संचार जटिलता युक्ति के अनुसार, S1S (नीचे) में समुच्चय की एक जोड़ी को एक समुच्चय द्वारा एनकोड करने योग्य नहीं होता है।

S2S की कमियाँ: अशक्त S2S (WS2S) के लिए सभी समुच्चयों का परिमित होना आवश्यक होता है (ध्यान दें कि परिमितता कोनिग के लेम्मा का उपयोग करके S2S में व्यक्त की जा सकती है)। इस प्रकार अगर '1' स्ट्रिंग्स में प्रकट नही होती है तो S1S को आवश्यक रूप से प्राप्त किया जा सकता है, और इस प्रकार WS1S को भी परिमितता की भी आवश्यकता होती है। यहां तक ​​कि WS1S भी 2 की शक्तियों के विधेय के साथ [[प्रेस्बर्गर अंकगणित]] की व्याख्या कर सकता है, क्योंकि समुच्चय का उपयोग निश्चित जोड़ के साथ असीमित बाइनरी संख्याओं का प्रतिनिधित्व करने के लिए किया जा सकता है।

S2S निर्णय लेने योग्य होते है, और S2S, S1S, WS2S, WS1S में से प्रत्येक में घातांक के रैखिक रूप से बढ़ते संग्रह के अनुरूप एक [[गैर-प्राथमिक समस्या|गैर-प्राथमिक]] निर्णय जटिलता होती है। इस प्रकार निचली सीमा के लिए, Σ¹₁ WS1S सूत्रों पर विचार करना पर्याप्त होता है। अंकगणित (या अन्य) गणना का प्रस्ताव करने के लिए एक दूसरे क्रम के परिमाणक का उपयोग किया जा सकता है, जिसे पहले क्रम परिमाणक का उपयोग करके सत्यापित किया जा सकता है यदि हम परीक्षण कर सकते हैं कि कौन सी संख्याएं बराबर हैं। इसके लिए, यदि हम संख्याओं 1..m को उचित रूप से एनकोड करते हैं, तो हम बाइनरी प्रतिनिधित्व i1i2...im के साथ एक संख्या को i1 1 i2 2 ... im m के रूप में एनकोड कर सकते हैं, जिसके पहले एक संरक्षक होता है। संरक्षक के परीक्षण को विलय करने और चर नामों का पुन: उपयोग करने से, बिट्स की संख्या घातांक की संख्या में रैखिक होती है। इस प्रकार ऊपरी सीमा के लिए, निर्णय प्रक्रिया (नीचे) का उपयोग करके, के-फोल्ड परिमाणक विकल्प वाले सूत्रों को सूत्र की लंबाई (समान स्थिरांक के साथ) के के + ओ (1)-गुना घातांक के अनुरूप समय में निर्धारित किया जा सकता है।

(4) सूत्र φ पर विनिर्देशन की स्वयंसिद्ध स्कीमा है, जो सदैव दूसरे क्रम के युक्ति के लिए होती है। सदैव की तरह, यदि φ में मुक्त चर नहीं दिखाए देते हैं, तो हम अभिगृहीत का सार्वभौमिक समापन लेते हैं। यदि समानता विधेय के लिए प्राथमिक होती है, तो कोई विस्तारात्मकता S=T ⇔ ∀s (S(s) ⇔ T(s)) का सिद्धांत भी जोड़ता है। चूँकि हमारे पास समझ है, इस लिए इंडक्शन स्कीमा के अतिरिक्त एकल कथन हो सकता है।

S1S का अनुरूप स्वयंसिद्धीकरण पूरा हो जाता है।<ref>{{Cite conference |url=https://link.springer.com/content/pdf/10.1007%2F978-3-642-33475-7_22.pdf |last=Riba |first=Colin |title=अनंत शब्दों पर राक्षसी दूसरे क्रम के तर्क के स्वयंसिद्धीकरण की पूर्णता का एक मॉडल सैद्धांतिक प्रमाण|conference=TCS 2012 |date=2012 |doi=10.1007/978-3-642-33475-7_22}}</ref> यघपि, S2S के लिए, पूर्णता खुली रहती है (2021 तक)। जबकि S1S में एकरूपता होती है, कोई S2S परिभाषित (यहां तक ​​कि पैरामीटर की अनुमति देने वाला) विकल्प फलन नहीं होता है जो एक गैर-रिक्त समुच्चय दिखाता है, S, S का एक तत्व लौटाता है,<ref>{{Citation |chapter-url=https://hal-upec-upem.archives-ouvertes.fr/hal-00620169/file/csl07.pdf |chapter=MSO on the Infinite Binary Tree: Choice and Order |last1=Carayol |first1=Arnaud |last2= Löding|first2=Christof |title=Computer Science Logic |series=Lecture Notes in Computer Science |date=2007 |volume=4646 |pages=161–176 |doi=10.1007/978-3-540-74915-8_15|isbn=978-3-540-74914-1 |s2cid=14580598 }}</ref> और समझ स्कीमों को सामान्यतः विकल्प के सिद्धांत के विभिन्न रूपों के साथ संवर्धित किया जाता है। यघपि, (1)-(4) कुछ [[समता खेल|समानता का खेलों]] के लिए निर्धारण स्कीमा के साथ विस्तारित होने पर पूर्ण हो जाता है।<ref>{{Cite journal |title=अनंत पेड़ों का एक कार्यात्मक (मोनैडिक) दूसरे क्रम का सिद्धांत|last1=Das |first=Anupam |last2=Riba |first2=Colin |journal=Logical Methods in Computer Science |volume=16|issue=4 |date=2020 |doi=10.23638/LMCS-16(4:6)2020 |arxiv=1903.05878}} (A preliminary 2015 version erroneously claimed proof of completeness without the determinacy schema.)</ref>

S2S को Π¹₃ सूत्रों द्वारा भी स्वयंसिद्ध किया जा सकता है (स्ट्रिंग्स पर उपसर्ग संबंध को प्राथमिक के रूप में उपयोग करके)। यघपि, यह अंतिम रूप से स्वयंसिद्ध नहीं होता है, न ही इसे Σ¹₃ सूत्रों द्वारा स्वयंसिद्ध किया जा सकता है, तथापि हम प्रेरण स्कीमा और अन्य सूत्रों का एक सीमित समुच्चय जोड़ दें (यह Π¹₂-CA₀ से सम्बन्धित होता है)।

प्रत्येक परिमित k के लिए, ट्री-चौड़ाई ≤k (और संबंधित ट्री अपघटन) के साथ गणनीय ग्राफ़ का मोनैडिक द्वितीय क्रम (MSओ) सिद्धांत S2S में व्याख्या योग्य होता है (कोर्सेल का प्रमेय देखें)। उदाहरण के लिए, ट्री कीMSO सिद्धांत (ग्राफ़ के रूप में) या [[श्रृंखला-समानांतर ग्राफ]] का निर्णय लेने योग्य होता है। यहां (अर्थात् सीमित हुए ट्री की चौड़ाई के लिए), हम शीर्षों (या किनारों) के एक समुच्चय के लिए परिमितता परिमाणक की व्याख्या भी कर सकते हैं, और एक निश्चित पूर्णांक के समुच्चय मॉड्यूलो में शीर्षों (या किनारों) की गिनती भी कर सकते हैं। इस प्रकार असंख्य ग्राफ़ की अनुमति देने से सिद्धांत नहीं बदलता है। इसके अतिरिक्त, तुलना के लिए, S1S सीमित हुए [[पथ-चौड़ाई]] के जुड़े ग्राफ़ की व्याख्या कर सकता है।

इसके विपरीत, असंबद्ध ट्री -चौड़ाई के ग्राफ़ के प्रत्येक समुच्चय के लिए, इसका अस्तित्व (अर्थात् Σ¹₁) यदि हम शीर्षों और किनारों दोनों पर विधेय की अनुमति देते हैं तो MSO सिद्धांत अनिर्णीत होता है। इस प्रकार, एक अर्थ में, S2S की निर्णायकता सर्वोत्तम संभव होती है। इस प्रकार असीमित ट्री-चौड़ाई वाले ग्राफ़ में बड़े ग्रिड माइनर होते हैं, जिनका उपयोग [[ट्यूरिंग मशीन]] का अनुकरण करने के लिए किया जा सकता है।

S2S में कमी करके, गणनीय आदेशों का MSO सिद्धांत निर्णायक होता है, जैसा कि उनके क्लेन-ब्रौवर आदेशों के साथ गणनीय ट्री का MSO सिद्धांत होता है। यघपि, MSO सिद्धांत (<math>\mathbb{R}</math>, <) अनिर्णीत होता है।<ref>{{Cite journal |first1=Yuri |last1=Gurevich |first2=Saharon |last2=Shelah | authorlink2=Saharon Shelah |title=अद्वैतवादी सिद्धांत और "अगली दुनिया"|journal=[[Israel Journal of Mathematics]] |date=1984 |volume=49 |issue=1–3 |pages=55–68 |doi=10.1007/BF02760646 | doi-access=free |s2cid=15807840 }}</ref><ref>{{Cite web |url=https://mathoverflow.net/questions/385530/what-is-the-turing-degree-of-the-monadic-theory-of-the-real-line |title=What is the Turing degree of the monadic theory of the real line? |publisher=MathOverflow |access-date=November 14, 2022}}</ref> इस प्रकार क्रमवाचक संख्या का MSO सिद्धांत <ω₂ निर्णय योग्य होता है; इस प्रकार ω₂ के लिए निर्णायकता ZFC से स्वतंत्र होता है (Con(ZFC + [[कमजोर रूप से कॉम्पैक्ट कार्डिनल]] मानते हुए)) ।<ref>{{Cite journal |first1=Yuri |last1=Gurevich |first2=Menachem |last2=Magidor |first3=Saharon |last3=Shelah |date=1993 |title=The monadic theory of ω₂ |journal=The Journal of Symbolic Logic |volume=48 |issue=2 |pages=387–398 |doi=10.2307/2273556 |jstor=2273556 |s2cid=120260712 |url=https://shelah.logic.at/files/95215/141.pdf }}</ref> इसके अतिरिक्त, एक क्रमवाचक संख्या को क्रमवाचक संख्या पर मोनैडिक सेकेंड क्रम युक्ति का उपयोग करके परिभाषित किया जा सकता है यदि इसे क्रमवाचक संख्या जोड़ और गुणा द्वारा निश्चित नियमित क्रमवाचक संख्या से प्राप्त किया जा सकता है।<ref>{{Citation |chapter=Monadic definability of ordinals |first=Itay |last=Neeman|title=Computational Prospects of Infinity |series=Lecture Notes Series, Institute for Mathematical Sciences, National University of Singapore |chapter-url=https://www.math.ucla.edu/~ineeman/monadic-def.pdf |date=2008 |volume=15 |pages=193–205 |doi=10.1142/9789812796554_0010|isbn=978-981-279-654-7 }}</ref>

S1S के लिए, प्रत्येक सूत्र Δ¹₁ सूत्र, और Π⁰₂ अंकगणितीय सूत्रों के बूलियन संयोजन के बराबर होता है। इसके अतिरिक्त, प्रत्येक S1S सूत्र सूत्र के मापदंडों के संगत ω-ऑटोमेटन द्वारा स्वीकृति के बराबर होते है। इस प्रकार ऑटोमेटन एक नियतात्मक समता ऑटोमेटन हो सकता है: एक समता ऑटोमेटन में प्रत्येक स्थिति के लिए एक पूर्णांक प्राथमिकता होती है, और यदि अनंत रूप से देखी जाने वाली सर्वोच्च प्राथमिकता अधिकांशतः विषम (वैकल्पिक रूप से, सम) होती है, तो इसे स्वीकार करता है।

S2S के लिए, ट्री ऑटोमेटा (नीचे) का उपयोग करते हुए, प्रत्येक सूत्र Δ¹₂ सूत्र के बराबर होता है। इसके अतिरिक्त, प्रत्येक S2S सूत्र मात्र चार परिमाणक, ∃S∀T∃s∀t ... वाले सूत्र के बराबर होता है (यह मानते हुए कि हमारी औपचारिकता में उपसर्ग संबंध और उत्तराधिकारी कार्य दोनों होते हैं)। इस प्रकार S1S के लिए, तीन परिमाणक (∃S∀s∃t) पर्याप्त होते हैं, और WS2S और WS1S के लिए, दो परिमाणक (∃S∀t) पर्याप्त होते हैं; WS2S और WS1S के लिए यहां उपसर्ग संबंध की आवश्यकता नहीं होती है।

यघपि , मुक्त दूसरे क्रम के चर के साथ, प्रत्येक S2S सूत्र को मात्र Π¹₁ के माध्यम से दूसरे क्रम के अंकगणित में व्यक्त नहीं किया जा सकता है (रिवर्स गणित देखें)। RCA₀ + (स्कीमा) {τ: τ एक सत्य S2S सूत्र } (स्कीमा) के बराबर होता है {τ: τ एक Π¹₃ सूत्र है जिसे Π¹₂-CA₀ } में सिद्ध किया जा सकता है।<ref name="S2S--Pi-1-2-CA_0">{{Cite conference |conference=LICS '16: 31st Annual ACM/IEEE Symposium on Logic in Computer Science |date=2016  |title=राबिन की निर्णायकता प्रमेय कितनी अप्रमाणित है?|first1=Leszek |last1=Kołodziejczyk |first2=Henryk |last2=Michalewski |arxiv=1508.06780 }}</ref><ref>{{Cite web |last=Kołodziejczyk |first=Leszek |url = https://cs.nyu.edu/pipermail/fom/2015-October/019257.html |title=Question on Decidability of S2S |publisher=FOM |date=October 19, 2015}}</ref> आधार सिद्धांत पर, स्कीमा (k पर स्कीमा) ∀S⊆ω ∃α₁<....<α_''k'' ''L''_α1(''S'') ≺_Σ1 ... ≺_Σ1 ''L''_α''k''(S) के समतुल्य होती है। जहां L रचनात्मक ब्रह्मांड होता है ([[बड़े गणनीय क्रमसूचक]] भी देखें)। सीमित प्रेरण के कारण, Π¹₂-CA₀ यह सिद्ध नहीं करता कि सब सत्य है (मानक निर्णय प्रक्रिया के अंतर्गत) Π¹₃ S2S कथन वास्तव में सत्य होते हैं, तथापि ऐसा प्रत्येक सूत्र Π¹₂-CA₀ सिद्ध करने योग्य होता है।

S2S के न्यूनतम प्रतिरूप में बाइनरी स्ट्रिंग्स पर सभी नियमित भाषाएँ सम्मलित होती हैं। इस प्रकार यह मानक प्रतिरूप का एक प्रारंभिक उप प्रतिरूप होता है, इसलिए यदि ट्री एक S2S पैरामीटर-मुक्त निश्चित समुच्चय गैर-रिक्त होता है, तो इसमें एक नियमित ट्री सम्मलित होता है। इस प्रकार एक नियमित भाषा को एक नियमित {0,1}-लेबल पूर्ण अनंत बाइनरी ट्री (स्ट्रिंग्स पर विधेय के साथ पहचाना गया) के रूप में भी माना जा सकता है। एक लेबल वाला ट्री नियमित होता है यदि इसे प्रारंभिक शीर्ष के साथ शीर्ष-लेबल वाले परिमित निर्देशित ग्राफ को अनियंत्रित करके प्राप्त किया जा सकता है; प्रारंभिक शीर्ष से पहुंच योग्य ग्राफ़ में एक (निर्देशित) चक्र एक अनंत ट्री देता है। नियमित ट्री की इस व्याख्या और एन्कोडिंग के साथ, प्रत्येक सत्य S2S सूत्र प्राथमिक फलन अंकगणित में पहले से ही सिद्ध हो सकता है। इस प्रकार यह गैर-नियमित ट्री होता हैं जिन्हें निर्धारण के लिए गैर-विधेयात्मक समझ की आवश्यकता हो सकती है। गणना योग्य संबंध के साथ S1S (और संभवतः S2S) (मानक प्रथम क्रम भाग के साथ और बिना दोनों) के गैर-नियमित (अर्थात् गैर-नियमित भाषाओं वाले) प्रतिरूप होते हैं। यघपि , स्ट्रिंग के पुनरावर्ती समुच्चय का समुच्चय के ज्ञान और निर्धारण की विफलता के कारण S2S का प्रतिरूप नहीं बनाता है।

निर्णायकता का प्रमाण यह प्रदर्शित करता है कि प्रत्येक सूत्र एक गैर-नियतात्मक ट्री ऑटोमेटन द्वारा स्वीकृति के बराबर होता है ([[ वृक्ष स्वचालन | ट्री स्वचालन]] और अनंत-ट्री ऑटोमेटन देखें)। एक अनंत ट्री ऑटोमेटन जड़ से प्रारम्भ होता है और ट्री की ओर बढ़ता है, और यदि प्रत्येक ट्री उपखंड स्वीकार करती है। एक गैर-नियतात्मक ट्री ऑटोमेटन स्वीकार करता है कि क्या खिलाड़ी 1 के पास जीतने की रणनीति होती है, जहां खिलाड़ी 1 नए स्थितियों (p₀,p₁) की एक (वर्तमान स्थिति और इनपुट के लिए) जोड़ी का चयन करता  है, जबकि खिलाड़ी 2उपखंड का चयन करता  है, यदि 0 चयन किया जाता है तो p₀ में संक्रमण होता है और p1 अन्यथा में होता है। इस प्रकार सह-नॉन-नियतिवादी ऑटोमेटन के लिए, सभी विकल्प खिलाड़ी 2 द्वारा तय किए जाते हैं, जबकि नियतात्मक के लिए, (p0,p1) स्थिति और इनपुट द्वारा तय किया जाता है; और एक गेम ऑटोमेटन के लिए, दो खिलाड़ी उपखंड और स्थिति को सेट करने के लिए एक सीमित खेल खेलते हैं। किसी उपखंड पर स्वीकृति उपखंड पर अनंत बार देखी जाने वाली स्थितियों पर आधारित होती है; इस प्रकार समता ऑटोमेटा यहाँ पर्याप्त रूप से सामान्य होता हैं।

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

निश्चयात्मकता: [[ZFC]] में, बोरेल खेल निर्धारित किए जाते हैं और Π⁰₂ के सूत्र (अनैतिक वास्तविक मापदंडों के साथ) के बूलियन संयोजनों के लिए निर्धारण प्रमाण भी यहां एक रणनीति भी देते हैं जो मात्र वर्तमान स्थिति और ट्री की स्थिति पर निर्भर करती है। इसका प्रमाण प्राथमिकताओं की संख्या पर प्रेरण द्वारा होता है। मान लें कि k प्राथमिकताएँ हैं, सर्वोच्च प्राथमिकता k है, और k में खिलाड़ी 2 के लिए सही समता है। प्रत्येक स्थिति (ट्री स्थिति + स्थिति) के लिए कम से कम क्रमसूचक α (यदि कोई हो) निर्दिष्ट करें जिससें खिलाड़ी 1 की जीत हो सभी प्रविष्टि की गई (एक या अधिक चरणों के बाद) प्राथमिकता k स्थितियों (यदि कोई हो) के साथ रणनीति जिसमें लेबल <α होता है। यदि प्रारंभिक स्थिति को लेबल किया गया है तो खिलाड़ी 1 जीत सकता है: हर बार प्राथमिकता k स्थिति तक पहुंचने पर, क्रमसूचक कम हो जाता है, और इसके अतिरिक्त घटने के मध्य, खिलाड़ी 1 k-1 प्राथमिकताओं के लिए एक रणनीति का उपयोग कर सकता है। यदि स्थिति लेबल रहित है तो खिलाड़ी 2 जीत सकता है: k-1 प्राथमिकताओं के निर्धारण के अनुसार, खिलाड़ी 2 के पास एक रणनीति होती है जो जीतती है या एक गैर-लेबल प्राथमिकता k स्थिति में प्रवेश करती है, ज�