S2S (गणित): Difference between revisions

From Vigyanwiki
No edit summary
No edit summary
 
(8 intermediate revisions by 3 users not shown)
Line 1: Line 1:
गणित में, 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 में कई निर्णायक सिद्धांतों की व्याख्या की जा सकती है। इसकी निर्णायकता 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 से संबंधित है।
S2S की प्रथम क्रम की वस्तुएं परिमित बाइनरी स्ट्रिंग होती हैं। दूसरे क्रम की वस्तुएं परिमित बाइनरी स्ट्रिंग्स के अनैतिक समुच्चय (या एकात्मक विधेय) होता हैं। इस प्रकार S2S में स्ट्रिंग्स पर फलन s→s0 और s→s1होता हैं, और विधेय s∈S (प्रतिरूप, S(s)) का अर्थ है कि स्ट्रिंग s समुच्चय S से संबंधित होती है।


कुछ गुण और परंपराएँ:
कुछ गुण और परंपराएँ:
* डिफ़ॉल्ट रूप से, लोअरकेस अक्षर पहले क्रम की वस्तुओं को संदर्भित करते हैं, और अपरकेस दूसरे क्रम की वस्तुओं को संदर्भित करते हैं।
* डिफ़ॉल्ट रूप से, लोअरकेस अक्षर पहले क्रम की वस्तुओं को संदर्भित करते हैं, औरअपरकेस दूसरे क्रम की वस्तुओं को संदर्भित करते हैं।
* समुच्चयों का समावेश S2S को दूसरे क्रम का बनाता है, जिसमें k>1 के लिए k-ary विधेय चर की अनुपस्थिति का संकेत मिलता है।
* समुच्चयों का समावेश S2S को दूसरे क्रम का बनाता है, जिसमें k>1 के लिए k-ary विधेय चर की अनुपस्थिति का संकेत मिलता है।
* स्ट्रिंग्स s और t का संयोजन st द्वारा दर्शाया जाता है, और यह आम तौर पर S2S में उपलब्ध नहीं है, यहां तक ​​कि s→0s में भी नहीं। स्ट्रिंग्स के बीच [[स्ट्रिंग ऑपरेशन]] निश्चित है।
* स्ट्रिंग्स s और t का संयोजन st द्वारा दर्शाया जाता है, और यह सामान्यतः S2S में उपलब्ध नहीं होता है, यहां तक ​​कि s→0s में भी उपलब्ध नहीं होता है। स्ट्रिंग्स के मध्य [[स्ट्रिंग ऑपरेशन]] निश्चित होता है।
* समानता आदिम है, या इसे s = t ⇔ ∀S (S(s) ⇔ S(t)) और S = T ⇔ ∀s (S(s) ⇔ T(s)) के रूप में परिभाषित किया जा सकता है।
* समानता प्राथमिक होती है, और इसे s = t ⇔ ∀S (S(s) ⇔ S(t)) और S = T ⇔ ∀s (S(s) ⇔ T(s)) के रूप में परिभाषित किया जा सकता है।
* स्ट्रिंग्स के स्थान पर, कोई (उदाहरण के लिए) n→2n+1 और n→2n+2 के साथ प्राकृतिक संख्याओं का उपयोग कर सकता है, लेकिन कोई अन्य ऑपरेशन नहीं।
* स्ट्रिंग्स के स्थान पर, कोई (उदाहरण के लिए) n→2n+1 और n→2n+2 के साथ प्राकृतिक संख्याओं का उपयोग कर सकता है, लेकिन कोई अन्य ऑपरेशन नहीं प्रयोग कर सकता है।
* सभी बाइनरी स्ट्रिंग्स का समुच्चय {0,1} द्वारा दर्शाया गया है<sup>*</sup>, [[क्लेन स्टार]] का उपयोग करते हुए।
* [[क्लेन स्टार]] का उपयोग करते हुए, सभी बाइनरी स्ट्रिंग्स के समुच्चय को {0,1} द्वारा प्रदर्शित किया जाता है।
* {0,1} का मनमाना उपसमुच्चय<sup>*</sup> को कभी-कभी पेड़ों से पहचाना जाता है, विशेष रूप से {0,1}-लेबल वाले पेड़ {0,1} के रूप में<sup>*</sup>; {0,1}<sup>*</sup> एक पूर्ण अनंत बाइनरी ट्री बनाता है।
* {0,1} का अनैतिक उपसमुच्चय<sup>*</sup> को कभी-कभी ट्री से पहचाना जाता है, विशेष रूप से {0,1}-लेबल वाले ट्री {0,1} के रूप में<sup>*</sup>; {0,1} एक पूर्ण अनंत बाइनरी ट्री बनाता है।
* सूत्र जटिलता के लिए, स्ट्रिंग्स पर उपसर्ग संबंध को आम तौर पर पहले क्रम के रूप में माना जाता है। इसके बिना, सभी सूत्र Δ के समतुल्य नहीं होंगे<sup>1</sup><sub>2</sub> सूत्र.<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>
* सूत्र जटिलता के लिए, स्ट्रिंग्स पर उपसर्ग संबंध को सामान्यतः पहले क्रम के रूप में माना जाता है। इसकेअतिरिक्त, सभी सूत्र Δ<sup>1</sup><sub>2</sub> के समतुल्य नहीं होंगे।<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>
* S2S में अभिव्यक्त गुणों के लिए (सभी बाइनरी स्ट्रिंग्स के समुच्चय को एक पेड़ के रूप में देखते हुए), प्रत्येक नोड के लिए, केवल O(1) बिट्स को बाएं सबट्री और दाएं सबट्री और बाकी के बीच संचारित किया जा सकता है ([[संचार जटिलता]] देखें)।
* S2S में अभिव्यक्त गुणों के लिए (सभी बाइनरी स्ट्रिंग्स के समुच्चय को एक ट्री के रूप में देखते हुए), प्रत्येक नोड के लिए, मात्र O(1) बिट्स को बाएं सबट्री और दाएं सबट्री और बाकी के मध्य संचारित किया जा सकता है ([[संचार जटिलता]] देखें)।
* एक निश्चित k के लिए, स्ट्रिंग से k तक एक फ़ंक्शन (यानी k के नीचे की प्राकृतिक संख्या) को एक समुच्चय द्वारा एन्कोड किया जा सकता है। इसके अलावा, s,t ⇒ s01t{{prime}} जहां टी{{prime}} t के प्रत्येक वर्ण को दोगुना कर देता है, और s ⇒ {s01t{{prime}}: t∈{0,1}<sup>*</sup>} S2S निश्चित है। इसके विपरीत, संचार जटिलता तर्क के अनुसार, S1S (नीचे) में समुच्चय की एक जोड़ी एक समुच्चय द्वारा एन्कोड करने योग्य नहीं है।
* एक निश्चित k के लिए, स्ट्रिंग से k तक एक फलन (अर्थात् k के नीचे की प्राकृतिक संख्या) को एक समुच्चय द्वारा एनकोड किया जा सकता है। इसके अतिरिक्त, s,t ⇒ s01t{{prime}} जहां T{{prime}} t के प्रत्येक वर्ण को दोगुना कर देता है, और s ⇒ {s01t{{prime}}: t∈{0,1}<sup>*</sup>} S2S निश्चित होता है। इसके विपरीत, संचार जटिलता युक्ति के अनुसार, S1S (नीचे) में समुच्चय की एक जोड़ी को एक समुच्चय द्वारा एनकोड करने योग्य नहीं होता है।


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


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


S2S निर्णय लेने योग्य है, और S2S, S1S, WS2S, WS1S में से प्रत्येक में घातांक के रैखिक रूप से बढ़ते ढेर के अनुरूप एक [[गैर-प्राथमिक समस्या]] निर्णय जटिलता है। निचली सीमा के लिए, Σ पर विचार करना पर्याप्त है<sup>1</sup><sub>1</sub> WS1S वाक्य. अंकगणित (या अन्य) गणना का प्रस्ताव करने के लिए एक दूसरे क्रम के क्वांटिफायर का उपयोग किया जा सकता है, जिसे पहले ऑर्डर क्वांटिफायर का उपयोग करके सत्यापित किया जा सकता है यदि हम परीक्षण कर सकते हैं कि कौन सी संख्याएं बराबर हैं। इसके लिए, यदि हम संख्याओं 1..m को उचित रूप से एन्कोड करते हैं, तो हम बाइनरी प्रतिनिधित्व i के साथ एक संख्या को एनकोड कर सकते हैं<sub>1</sub>i<sub>2</sub>...मैं<sub>''m''</sub> जैसे मैं<sub>1</sub> 1 मैं<sub>2</sub> 2... मैं<sub>''m''</sub> मी, एक गार्ड से पहले। गार्ड के परीक्षण को मर्ज करने और चर नामों का पुन: उपयोग करने से, बिट्स की संख्या घातांक की संख्या में रैखिक होती है। ऊपरी सीमा के लिए, निर्णय प्रक्रिया (नीचे) का उपयोग करके, के-गुना क्वांटिफायर विकल्प वाले वाक्यों को वाक्य की लंबाई (समान स्थिरांक के साथ) के के + ओ (1)-गुना घातांक के अनुरूप समय में तय किया जा सकता है।
==== अक्षीयकरण ====
WS2S को कुछ बुनियादी गुणों और प्रेरण स्कीमा के माध्यम से स्वयंसिद्ध किया जा सकता है।<ref>{{Citation |url=https://docs.lib.purdue.edu/cgi/viewcontent.cgi?article=1477&context=cstech |title=An axiom system for the weak monadic second order theory of two successors |last=Siefkes |first=Dirk |date=1971 }}</ref>


'स्वयंसिद्धीकरण'
S2S को आंशिक रूप से स्वयंसिद्ध किया जा सकता है:<br />(1) ∃!s ∀t ( t0≠s ∧ t1≠s) (रिक्त स्ट्रिंग, जिसे ε द्वारा दर्शाया गया है; ∃!s का अर्थ है कि "अद्वितीय s" होता है)<br />(2) ∀s,t ∀i∈{0,1} ∀j∈{0,1} (si=tj ⇒ s=t ∧ i=j) (i और j का उपयोग एक संक्षिप्त रूप होता है; i= j के लिए, 0, 1 के बराबर नहीं होता है)<br />(3) ∀S (S(ε) ∧ ∀s (S(s) ⇒ S(s0) ∧ S(s1))⇒ ∀s S(s)) ([[गणितीय प्रेरण]])<br />(4) ∃S ∀s (S(s) ⇔ φ(s)) (S φ में मुक्त नहीं होता है)


WS2S को कुछ बुनियादी गुणों और प्रेरण स्कीमा के माध्यम से स्वयंसिद्ध किया जा सकता है।<ref>{{Citation |url=https://docs.lib.purdue.edu/cgi/viewcontent.cgi?article=1477&context=cstech |title=An axiom system for the weak monadic second order theory of two successors |last=Siefkes |first=Dirk |date=1971 }}</ref>
(4) सूत्र φ पर विनिर्देशन की स्वयंसिद्ध स्कीमा है, जो सदैव दूसरे क्रम के युक्ति के लिए होती है। सदैव की तरह, यदि φ में मुक्त चर नहीं दिखाए देते हैं, तो हम अभिगृहीत का सार्वभौमिक समापन लेते हैं। यदि समानता विधेय के लिए प्राथमिक होती है, तो कोई विस्तारात्मकता S=T ⇔ ∀s (S(s) ⇔ T(s)) का सिद्धांत भी जोड़ता है। चूँकि हमारे पास समझ है, इस लिए इंडक्शन स्कीमा के अतिरिक्त एकल कथन हो सकता है।
S2S को आंशिक रूप से स्वयंसिद्ध किया जा सकता है:<br />
(1) ∃!s ∀t ( t0≠s ∧ t1≠s) (खाली स्ट्रिंग, जिसे ε द्वारा दर्शाया गया है; ∃!s का अर्थ है कि अद्वितीय s है)<br />
(2) ∀s,t ∀i∈{0,1} ∀j∈{0,1} (si=tj ⇒ s=t ∧ i=j) (i और j का उपयोग एक संक्षिप्त नाम है; i= के लिए j, 0 1 के बराबर नहीं है)<br />
(3) ∀S (S(ε) ∧ ∀s (S(s) ⇒ S(s0) ∧ S(s1))⇒ ∀s S(s)) ([[गणितीय प्रेरण]])<br />
(4) ∃S ∀s (S(s) ⇔ φ(s)) (S φ में मुक्त नहीं है)


(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>


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 को Π<sup>1</sup><sub>3</sub> सूत्रों द्वारा भी स्वयंसिद्ध किया जा सकता है (स्ट्रिंग्स पर उपसर्ग संबंध को प्राथमिक के रूप में उपयोग करके)। यघपि, यह अंतिम रूप से स्वयंसिद्ध नहीं होता है, न ही इसे Σ<sup>1</sup><sub>3</sub> सूत्रों द्वारा स्वयंसिद्ध किया जा सकता है, तथापि हम प्रेरण स्कीमा और अन्य सूत्रों का एक सीमित समुच्चय जोड़ दें (यह Π<sup>1</sup><sub>2</sub>-CA<sub>0</sub> से सम्बन्धित होता है)
S2S को Π द्वारा भी स्वयंसिद्ध किया जा सकता है<sup>1</sup><sub>3</sub> वाक्य (स्ट्रिंग्स पर उपसर्ग संबंध को आदिम के रूप में उपयोग करना)। हालाँकि, यह अंतिम रूप से स्वयंसिद्ध नहीं है, न ही इसे Σ द्वारा स्वयंसिद्ध किया जा सकता है<sup>1</sup><sub>3</sub> वाक्य भले ही हम प्रेरण स्कीमा और अन्य वाक्यों का एक सीमित समुच्चय जोड़ते हैं (यह Π से इसके संबंध से पता चलता है)<sup>1</sup><sub>2</sub>-वह<sub>0</sub>).


== S2S से संबंधित सिद्धांत ==
== S2S से संबंधित सिद्धांत ==


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


इसके विपरीत, असंबद्ध वृक्ष-चौड़ाई के ग्राफ़ के प्रत्येक समुच्चय के लिए, इसका अस्तित्व (यानी Σ)<sup>1</sup><sub>1</sub>) यदि हम शीर्षों और किनारों दोनों पर विधेय की अनुमति देते हैं तो एमएसओ सिद्धांत अनिर्णीत है। इस प्रकार, एक अर्थ में, 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 सिद्धांत <ω<sub>2</sub> निर्णय योग्य होता है; इस प्रकार ω<sub>2</sub> के लिए निर्णायकता 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 ω<sub>2</sub> |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>


S2S में कमी करके, गणनीय आदेशों का 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> ऑर्डिनल्स का एमएसओ सिद्धांत <ω<sub>2</sub> निर्णययोग्य है; ω के लिए निर्णायकता<sub>2</sub> 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 ω<sub>2</sub> |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>
S2S कुछ मोडल युक्ति की निर्णायकता के लिए उपयोगी होता है, [[क्रिपके शब्दार्थ]] स्वाभाविक रूप से ट्री की ओर ले जाता है।
S2S कुछ मोडल लॉजिक्स की निर्णायकता के लिए उपयोगी है, [[क्रिपके शब्दार्थ]] स्वाभाविक रूप से पेड़ों की ओर ले जाता है।


S2S+U (या सिर्फ S1S+U) अनिर्णीत है यदि U अनबाउंडिंग क्वांटिफायर है - UX Φ(X) यदि Φ(X) कुछ मनमाने ढंग से बड़े परिमित X के लिए है।<ref>{{Citation |title=The MSO+U theory of (N, &lt;) is undecidable |first1=Mikołaj |last1=Bojańczyk |first2=Paweł |last2=Parys |first3=Szymon |last3=Toruńczyk |arxiv=1502.04578 |date=2015}}</ref> हालाँकि, WS2S+U, अनंत पथों पर परिमाणीकरण के साथ भी, निर्णय लेने योग्य है, यहां तक ​​कि S2S उपसूत्रों के साथ भी, जिनमें U शामिल नहीं है।<ref>{{Citation |title=Weak MSO+U with path quantifiers over infinite trees |first1=Mikołaj |last1=Bojańczyk |arxiv=1404.7278 |date=2014}}</ref>
S2S+U (या सिर्फ S1S+U) अनिर्णीत होता है यदि U असीम परिमाणक होता है - UX Φ(X) यदि Φ(X) कुछ अनैतिक ढंग से बड़े परिमित X के लिए होता है।<ref>{{Citation |title=The MSO+U theory of (N, &lt;) is undecidable |first1=Mikołaj |last1=Bojańczyk |first2=Paweł |last2=Parys |first3=Szymon |last3=Toruńczyk |arxiv=1502.04578 |date=2015}}</ref> यघपि , WS2S+U, अनंत पथों पर परिमाणीकरण के साथ भी, निर्णय लेने योग्य होता है, यहां तक ​​कि S2S उपसूत्रों के साथ भी, जिनमें U सम्मलित नहीं होता है।<ref>{{Citation |title=Weak MSO+U with path quantifiers over infinite trees |first1=Mikołaj |last1=Bojańczyk |arxiv=1404.7278 |date=2014}}</ref>


== सूत्र जटिलता ==
== सूत्र जटिलता ==
बाइनरी स्ट्रिंग्स का एक समुच्चय S2S में निश्चित है यदि यह नियमित है (यानी एक [[नियमित भाषा]] बनाता है)S1S में, समुच्चय पर एक (एकात्मक) विधेय (पैरामीटर-मुक्त) निश्चित है यदि यह एक ओमेगा-नियमित भाषा है|ω-नियमित भाषा है। S2S के लिए, उन सूत्रों के लिए जो अपने मुक्त चर का उपयोग केवल उन स्ट्रिंग्स पर करते हैं जिनमें 1 नहीं है, अभिव्यक्ति S1S के समान ही है।
बाइनरी स्ट्रिंग्स का एक समुच्चय S2S में निश्चित होता है यदि यह नियमित (अर्थात् एक [[नियमित भाषा]] बनाता है) होता है। S1S में, समुच्चय पर एक (एकात्मक) विधेय (पैरामीटर-मुक्त) निश्चित होता है यदि यह एक ω-नियमित भाषा होती है। S2S के लिए, उन सूत्रों के लिए जो अपने मुक्त चर का उपयोग मात्र उन स्ट्रिंग्स पर करते हैं जिनमें 1 नहीं होता है, जिसकी अभिव्यक्ति S1S के समान ही होती है।


प्रत्येक S2S सूत्र के लिए φ(S<sub>1</sub>,...,एस<sub>''k''</sub>), (k मुक्त चर के साथ) और बाइनरी स्ट्रिंग्स T, φ(S) का परिमित वृक्ष<sub>1</sub>∩टी,...,एस<sub>''k''</sub>∩T) की गणना |T| में रैखिक समय में की जा सकती है (कोर्सेल का प्रमेय देखें), लेकिन जैसा कि ऊपर बताया गया है, ओवरहेड को सूत्र आकार में घातीय रूप से दोहराया जा सकता है (अधिक सटीक रूप से, समय है <math>O(|T|k)+2_{O(|\phi|)}^2</math>).
प्रत्येक S2S सूत्र के लिए φ(S<sub>1</sub>,...,S<sub>''k''</sub>), (k मुक्त चर के साथ) और बाइनरी स्ट्रिंग्स T के परिमित ट्री के लिए, φ(''S''<sub>1</sub>∩T,...,''S<sub>k</sub>''∩T) की गणना रैखिक समय में की जा सकती है (कोर्सेल का प्रमेय देखें), लेकिन जैसा कि ऊपर बताया गया है, ओवरहेड को सूत्र आकार में घातीय रूप से दोहराया जा सकता है (अधिक स्पष्ट रूप से, <math>O(|T|k)+2_{O(|\phi|)}^2</math> समय होता है)


S1S के लिए, प्रत्येक सूत्र Δ के बराबर है<sup>1</sup><sub>1</sub> सूत्र, और Π के बूलियन संयोजन के लिए<sup>0</sup><sub>2</sub> अंकगणितीय सूत्र. इसके अलावा, प्रत्येक S1S सूत्र सूत्र के मापदंडों के संगत ω-ऑटोमेटन द्वारा स्वीकृति के बराबर है। ऑटोमेटन एक नियतात्मक समता ऑटोमेटन हो सकता है: एक समता ऑटोमेटन में प्रत्येक राज्य के लिए एक पूर्णांक प्राथमिकता होती है, और यदि अनंत रूप से देखी जाने वाली सर्वोच्च प्राथमिकता अक्सर विषम (वैकल्पिक रूप से, सम) होती है, तो इसे स्वीकार करता है।
S1S के लिए, प्रत्येक सूत्र Δ<sup>1</sup><sub>1</sub> सूत्र, और Π<sup>0</sup><sub>2</sub> अंकगणितीय सूत्रों के बूलियन संयोजन के बराबर होता है। इसके अतिरिक्त, प्रत्येक S1S सूत्र सूत्र के मापदंडों के संगत ω-ऑटोमेटन द्वारा स्वीकृति के बराबर होते है। इस प्रकार ऑटोमेटन एक नियतात्मक समता ऑटोमेटन हो सकता है: एक समता ऑटोमेटन में प्रत्येक स्थिति के लिए एक पूर्णांक प्राथमिकता होती है, और यदि अनंत रूप से देखी जाने वाली सर्वोच्च प्राथमिकता अधिकांशतः विषम (वैकल्पिक रूप से, सम) होती है, तो इसे स्वीकार करता है।


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


हालाँकि, मुक्त दूसरे क्रम के चर के साथ, प्रत्येक S2S सूत्र को केवल Π के माध्यम से दूसरे क्रम के अंकगणित में व्यक्त नहीं किया जा सकता है<sup>1</sup><sub>1</sub> ट्रांसफ़िनिट रिकर्सन (रिवर्स गणित देखें)। आरसीए<sub>0</sub> + (स्कीमा) {τ: τ एक सच्चा S2S वाक्य है} (स्कीमा) के बराबर है {τ: τ एक Π है<sup>1</sup><sub>3</sub> Π में सिद्ध वाक्य<sup>1</sup><sub>2</sub>-वह<sub>0</sub> }.<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⊆ω ∃α के बराबर हैं<sub>1</sub><...<<sub>''k''</sub> L<sub>α<sub>1</sub></उप>(एस) ≺<sub>Σ<sub>1</sub></sub>... ≺ उप>एस<sub>1</sub></उप>एल उप>ए<sub>''k''</sub></sub>(एस) जहां एल रचनात्मक ब्रह्मांड है ([[बड़े गणनीय क्रमसूचक]] भी देखें)। सीमित प्रेरण के कारण, Π<sup>1</sup><sub>2</sub>-वह<sub>0</sub> यह सिद्ध नहीं करता कि सब सत्य है (मानक निर्णय प्रक्रिया के अंतर्गत) Π<sup>1</sup><sub>3</sub> S2S कथन वास्तव में सत्य हैं, भले ही ऐसा प्रत्येक वाक्य सिद्ध करने योग्य हो<sup>1</sup><sub>2</sub>-वह<sub>0</sub>.
यघपि , मुक्त दूसरे क्रम के चर के साथ, प्रत्येक S2S सूत्र को मात्र Π<sup>1</sup><sub>1</sub> के माध्यम से दूसरे क्रम के अंकगणित में व्यक्त नहीं किया जा सकता है (रिवर्स गणित देखें)। RCA<sub>0</sub> + (स्कीमा) {τ: τ एक सत्य S2S सूत्र } (स्कीमा) के बराबर होता है {τ: τ एक Π<sup>1</sup><sub>3</sub> सूत्र है जिसे Π<sup>1</sup><sub>2</sub>-CA<sub>0</sub> } में सिद्ध किया जा सकता है।<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⊆ω ∃α<sub>1</sub><....<α<sub>''k''</sub> ''L''<sub>α1</sub>(''S'') ≺<sub>Σ1</sub> ... ≺<sub>Σ1</sub> ''L''<sub>α''k''</sub>(S) के समतुल्य होती है। जहां L रचनात्मक ब्रह्मांड होता है ([[बड़े गणनीय क्रमसूचक]] भी देखें)। सीमित प्रेरण के कारण, Π<sup>1</sup><sub>2</sub>-CA<sub>0</sub> यह सिद्ध नहीं करता कि सब सत्य है (मानक निर्णय प्रक्रिया के अंतर्गत) Π<sup>1</sup><sub>3</sub> S2S कथन वास्तव में सत्य होते हैं, तथापि ऐसा प्रत्येक सूत्र Π<sup>1</sup><sub>2</sub>-CA<sub>0</sub> सिद्ध करने योग्य होता है।


इसके अलावा, बाइनरी स्ट्रिंग एस और टी के दिए गए समुच्चय, निम्नलिखित समतुल्य हैं:<br />
इसके अतिरिक्त, बाइनरी स्ट्रिंग S और T के दिए गए समुच्चय, निम्नलिखित समतुल्य होते हैं:<br />(1) T एक S2S होता है जिसे S से गणना योग्य बाइनरी स्ट्रिंग्स बहुपद समय के कुछ समुच्चय से परिभाषित किया जा सकता है।<br />(2) T की गणना कुछ गेम के लिए जीतने की स्थिति के समुच्चय से की जा सकती है जिसका भुगतान Π<sup>0</sup><sub>2</sub>(S) समुच्चय का एक सीमित बूलियन संयोजन होता है।<br />(3) T को अंकगणित μ-कैलकुलस में S से परिभाषित किया जा सकता है (अंकगणित सूत्र + निश्चित-बिंदु युक्ति )<br />(4) T सबसे कम β-प्रतिरूप में होता है (अर्थात् एक ω-प्रतिरूप जिसका समुच्चय-सैद्धांतिक प्रतिरूप [[ सकर्मक मॉडल |सकर्मक प्रतिरूप]] होता है) जिसमें S सम्मलित है और सभी Π<sup>1</sup><sub>3</sub> Π के Π<sup>1</sup><sub>2</sub>-CA<sub>0</sub> परिणामो को संतुष्ट करता है।
(1) टी एस2एस है जिसे एस से गणना योग्य बाइनरी स्ट्रिंग्स बहुपद समय के कुछ समुच्चय से परिभाषित किया जा सकता है।<br />
(2)