S2S (गणित): Difference between revisions

Revision as of 02:23, 6 July 2023

गणित में, S2S दो उत्तराधिकारियों वाला मोनैडिक द्वितीय क्रम सिद्धांत होता है। यह ज्ञात सबसे अभिव्यंजक प्राकृतिक निर्णायक सिद्धांतों में से एक होता है, जिसमें S2S में कई निर्णायक सिद्धांतों की व्याख्या की जा सकती है। इसकी निर्णायकता 1969 में माइकल ओ. राबिन द्वारा सिद्ध की गई थी।^[1]

मूल गुण

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

कुछ गुण और परंपराएँ:

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

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

निर्णय जटिलता

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

अक्षीयकरण

WS2S को कुछ बुनियादी गुणों और प्रेरण स्कीमा के माध्यम से स्वयंसिद्ध किया जा सकता है।^[3]

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

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

S1S का अनुरूप स्वयंसिद्धीकरण पूरा हो जाता है।^[4] यघपि, S2S के लिए, पूर्णता खुली रहती है (2021 तक)। जबकि S1S में एकरूपता है, कोई S2S परिभाषित (यहां तक कि पैरामीटर की अनुमति देने वाला) विकल्प फलन नहीं होता है जो एक गैर-खाली समुच्चय दिखाता है, S, S का एक तत्व लौटाता है,^[5] और समझ स्कीमों को सामान्यतः विकल्प के सिद्धांत के विभिन्न रूपों के साथ संवर्धित किया जाता है। यघपि, (1)-(4) कुछ समानता का खेलों के लिए निर्धारण स्कीमा के साथ विस्तारित होने पर पूर्ण हो जाता है।^[6]

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

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

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

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

S2S में कमी करके, गणनीय आदेशों का एमSओ सिद्धांत निर्णायक होता है, जैसा कि उनके क्लेन-ब्रौवर आदेशों के साथ गणनीय ट्री का एमSओ सिद्धांत होता है। यघपि, एमSओ सिद्धांत ( $\mathbb {R}$ , <) अनिर्णीत होता है।^[7]^[8] क्रमवाचक संख्या का एमSओ सिद्धांत <ω₂ निर्णय योग्य होता है; ω₂ के लिए निर्णायकता ZFC से स्वतंत्र होता है (Con(ZFC + कमजोर रूप से कॉम्पैक्ट कार्डिनल मानते हुए))।^[9] इसके अतिरिक्त, एक क्रमवाचक संख्या को क्रमवाचक संख्या पर मोनैडिक सेकेंड क्रम युक्ति का उपयोग करके परिभाषित किया जा सकता है यदि इसे क्रमवाचक संख्या जोड़ और गुणा द्वारा निश्चित नियमित क्रमवाचक संख्या से प्राप्त किया जा सकता है।^[10]

S2S कुछ मोडल युक्ति की निर्णायकता के लिए उपयोगी होता है, क्रिपके शब्दार्थ स्वाभाविक रूप से ट्री की ओर ले जाता है।

S2S+U (या सिर्फ S1S+U) अनिर्णीत होता है यदि U असीम परिमाणक होता है - UX Φ(X) यदि Φ(X) कुछ अनैतिक ढंग से बड़े परिमित X के लिए होता है।^[11] यघपि , WS2S+U, अनंत पथों पर परिमाणीकरण के साथ भी, निर्णय लेने योग्य होता है, यहां तक कि S2S उपसूत्रों के साथ भी, जिनमें U सम्मलित नहीं होता है।^[12]

सूत्र जटिलता

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

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

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

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

यघपि , मुक्त दूसरे क्रम के चर के साथ, प्रत्येक S2S सूत्र को मात्र Π¹₁ के माध्यम से दूसरे क्रम के अंकगणित में व्यक्त नहीं किया जा सकता है (रिवर्स गणित देखें)। RCA₀ + (स्कीमा) {τ: τ एक सत्य S2S सूत्र } (स्कीमा) के बराबर होता है {τ: τ एक Π¹₃ सूत्र है जिसे Π¹₂-CA₀ } में सिद्ध किया जा सकता है।^[13]^[14] आधार सिद्धांत पर, स्कीमा (k पर स्कीमा) ∀S⊆ω ∃α₁<....<α_k L_α1(S) ≺_Σ1 ... ≺_Σ1 L_αk(S) के समतुल्य होती है। जहां L रचनात्मक ब्रह्मांड होता है (बड़े गणनीय क्रमसूचक भी देखें)। सीमित प्रेरण के कारण, Π¹₂-CA₀ यह सिद्ध नहीं करता कि सब सत्य है (मानक निर्णय प्रक्रिया के अंतर्गत) Π¹₃ S2S कथन वास्तव में सत्य होते हैं, तथापि ऐसा प्रत्येक सूत्र Π¹₂-CA₀ सिद्ध करने योग्य होते हो।

इसके अतिरिक्त, बाइनरी स्ट्रिंग S और T के दिए गए समुच्चय, निम्नलिखित समतुल्य होते हैं:
(1) T एक S2S होता है जिसे S से गणना योग्य बाइनरी स्ट्रिंग्स बहुपद समय के कुछ समुच्चय से परिभाषित किया जा सकता है।
(2) T की गणना कुछ गेम के लिए जीतने की स्थिति के समुच्चय से की जा सकती है जिसका भुगतान Π⁰₂(S) समुच्चय का एक सीमित बूलियन संयोजन होता है।
(3) T को अंकगणित μ-कैलकुलस में S से परिभाषित किया जा सकता है (अंकगणित सूत्र + निश्चित-बिंदु युक्ति )।
(4) T सबसे कम β-प्रतिरूप में होता है (अर्थात् एक ω-प्रतिरूप जिसका समुच्चय-सैद्धांतिक समकक्ष सकर्मक प्रतिरूप होता है) जिसमें S सम्मलित है और सभी Π¹₃ Π के Π¹₂-CA₀ परिणामो को संतुष्ट करता है।

S1S और S2S के प्रतिरूप

मानक प्रतिरूप (जो S1S और S2S के लिए अद्वितीय एमएसओ प्रतिरूप होता है) के अतिरिक्त, S1S और S2S के लिए अन्य प्रतिरूप भी होते हैं, जो कार्यक्षेत्र के सभी सबसमुच्चय के अतिरिक्त कुछ का उपयोग करते हैं (हेनकिन अर्थ विज्ञान देखें)।

प्रत्येक S⊆ω के लिए, S में पुनरावर्ती समुच्चय मानक S1S प्रतिरूप का एक प्राथमिक उपप्रतिरूप बनाते हैं, और ट्यूरिंग जॉइन और ट्यूरिंग रिड्यूसिबिलिटी के अनुसार बंद किए गए ω के प्रत्येक गैर-रिक्त संग्रह के लिए समान होते हैं।^[15]

यह S1S निश्चित समुच्चयों की सापेक्ष पुनरावर्तीता और एकरूपता से निम्नानुसार होता है:
- φ(s) (s के एक फलन के रूप में) की गणना φ के मापदंडों और s′ के एक सीमित समुच्चय के लिए φ(s′) के मानों से की जा सकती, (इसका आकार φ के लिए एक नियतात्मक ऑटोमेटन में राज्यों की संख्या से घिरा हुआ होता है)।
- ∃S φ(S) के लिए एक k और S के S′ एक सीमित टुकड़ा चुनकर और S′ को बार-बार विस्तारित करके प्राप्त किया जा सकता है, जिससें प्रत्येक विस्तार के समय सर्वोच्च प्राथमिकता k होती है और विस्तार को k से ऊपर की प्राथमिकताओं को प्रभावित किए बिना S को संतुष्ट करते हुए S में पूरा किया जा सकता है (इन्हें मात्र प्रारंभिक S′ के लिए अनुमति दी गई है)। इसके अतिरिक्त, शाब्दिक रूप से कम से कम सबसे छोटे विकल्पों का उपयोग करके, एक S1S सूत्र φ' है, जो कि φ'⇒φ और ∃S φ(S) ⇔∃!S φ'(S) (अर्थात् एकरूपता; φ में मुक्त चर नहीं दिखाए जा सकते हैं; φ' मात्र सूत्र φ) पर निर्भर करता है।

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

S2S की निर्णायकता

निर्णायकता का प्रमाण यह प्रदर्शित करता है कि प्रत्येक सूत्र एक गैर-नियतात्मक ट्री ऑटोमेटन द्वारा स्वीकृति के बराबर होता है ( ट्री स्वचालन और अनंत-ट्री ऑटोमेटन देखें)। एक अनंत ट्री ऑटोमेटन जड़ से प्रारम्भ होता है और ट्री की ओर बढ़ता है, और यदि प्रत्येक ट्री शाखा स्वीकार करती है तो इसे स्वीकार करती है। एक गैर-नियतात्मक ट्री ऑटोमेटन स्वीकार करता है कि क्या खिलाड़ी 1 के पास जीतने की रणनीति है, जहां खिलाड़ी 1 नए राज्यों (पी 0, पी 1) की एक अनुमत (वर्तमान स्थिति और इनपुट के लिए) जोड़ी चुनता है, जबकि खिलाड़ी 2 शाखा चुनता है, यदि पी 0 में संक्रमण होता है 0 चुना गया है और 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 स्थिति में प्रवेश करती है, जिस स्थिति में खिलाड़ी 2 फिर से उस रणनीति का उपयोग कर सकता है। रणनीति को स्थितिगत बनाने के लिए (k पर प्रेरण द्वारा), सहायक खेल खेलते समय, यदि दो चुनी गई स्थितीय रणनीतियाँ एक ही स्थिति में ले जाती हैं, तो निम्न α के साथ रणनीति जारी रखें, या उसी α के लिए (या खिलाड़ी 2 के लिए) कम प्रारंभिक स्थिति (ताकि हम एक रणनीति को कई बार सीमित रूप से बदल सकें)।

ऑटोमेटा निर्धारण: सह-नॉनडेटर्मिनिस्टिक ट्री ऑटोमेटा के निर्धारण के लिए, ω-ऑटोमेटा पर विचार करना, शाखा की विकल्प को इनपुट के रूप में मानना, ऑटोमेटन का निर्धारण करना और नियतात्मक ट्री ऑटोमेटन के लिए इसका उपयोग करना पर्याप्त है। ध्यान दें कि यह गैर-नियतात्मक ट्री ऑटोमेटा के लिए काम नहीं करता है क्योंकि बाईं ओर जाने का निर्धारण (अर्थात् s→s0) दाहिनी शाखा की सामग्री पर निर्भर हो सकता है; गैर-नियतिवाद के विपरीत, नियतिवादी ट्री ऑटोमेटा स्पष्ट रूप से गैर-रिक्त समुच्चयों को भी स्वीकार नहीं कर सकता है। एक गैर-नियतात्मक ω-ऑटोमेटन एम को निर्धारित करने के लिए (सह-नॉनडेटर्मिनिस्टिक के लिए, पूरक लें, यह ध्यान में रखते हुए कि नियतात्मक समता ऑटोमेटा पूरक के अनुसार बंद हैं), हम प्रत्येक नोड के साथ एम के संभावित राज्यों का एक समुच्चय संग्रहीत करने और नोड निर्माण के लिए एक सफरा ट्री का उपयोग कर सकते हैं। और उच्च प्राथमिकता वाले राज्यों तक पहुंचने के आधार पर विलोपन। विवरण के लिए देखें ^[16] या।^[17] स्वीकृति की निर्णायकता: खाली ट्री के एक गैर-नियतात्मक समता ऑटोमेटन द्वारा स्वीकृति एक परिमित ग्राफ जी पर एक समता खेल से मेल खाती है। उपरोक्त स्थितीय (जिसे स्मृतिहीन भी कहा जाता है) निर्धारण का उपयोग करते हुए, इसे एक परिमित खेल द्वारा अनुकरण किया जा सकता है जो तब समाप्त होता है जब हम एक तक पहुंचते हैं लूप, लूप में सर्वोच्च प्राथमिकता वाले राज्य के आधार पर जीतने की स्थिति के साथ। एक चतुर अनुकूलन एक अर्धबहुपद समय एल्गोरिथ्म देता है,^[18] जो बहुपद समय है जब प्राथमिकताओं की संख्या काफी कम होती है (जो आमतौर पर व्यवहार में होती है)।

ट्री ों का सिद्धांत: ट्री ों पर एमSओ युक्ति की निर्णायकता के लिए (अर्थात् ग्राफ़ जो ट्री हैं), यहां तक कि पहले क्रम की वस्तुओं के लिए परिमितता और मॉड्यूलर गिनती परिमाणक के साथ, हम गणनीय ट्री ों को पूर्ण बाइनरी ट्री में एम्बेड कर सकते हैं और S 2 S की निर्णायकता का उपयोग कर सकते हैं। उदाहरण के लिए, एक नोड s के लिए, हम उसके बच्चों को s1, s01, s001 इत्यादि द्वारा दर्शा सकते हैं। अनगिनत ट्री ों के लिए, हम शेलह-स्टुप प्रमेय (नीचे) का उपयोग कर सकते हैं। हम कार्डिनलिT ω वाले समुच्चय प्रथम क्रम ऑब्जेक्ट के लिए एक विधेय भी जोड़ सकते हैं₁, और कार्डिनैलिT के लिए विधेय ω₂, और इसी तरह अनंत नियमित कार्डिनल्स के लिए। बंधे हुए ट्री की चौड़ाई के ग्राफ़ को ट्री ों का उपयोग करके व्याख्या की जा सकती है, और किनारों पर विधेय के बिना यह बंधे हुए क्लिक चौड़ाई के ग्राफ़ पर भी लागू होता है।

S2S को अन्य निर्णायक सिद्धांतों के साथ जोड़ना

अद्वैत सिद्धांतों के ट्री विस्तार: शेलह-स्टूप प्रमेय द्वारा,^[19]^[20] यदि एक मोनैडिक रिलेशनल प्रतिरूप एम निर्णायक है, तो उसका ट्री समकक्ष भी ऐसा ही है। उदाहरण के लिए, (औपचारिकरण का मॉड्यूलो विकल्प) S2S, {0,1} का ट्री समकक्ष है। ट्री समकक्ष में, पहले क्रम की वस्तुएं विस्तार द्वारा क्रमित एम के तत्वों के परिमित अनुक्रम हैं, और एक एम-संबंध पी_i पी पर मैप किया गया है_i(सीईओ₁,...,सीईओ_k) ⇔ पी_i(डी₁,...,डी_k) पी के साथ_i' अन्यथा गलत (डी_j∈M, और v, M के तत्वों का एक (संभवतः खाली) अनुक्रम है)। प्रमाण S2S निर्णायकता प्रमाण के समान है। प्रत्येक चरण में, एक (नॉनडेटर्मिनिस्टिक) ऑटोमेटन को इनपुट के रूप में एम ऑब्जेक्ट्स (संभवतः दूसरे क्रम) का एक टुपल मिलता है, और एक एम फॉर्मूला निर्धारित करता है कि किस राज्य संक्रमण की अनुमति है। खिलाड़ी 1 (जैसा कि ऊपर है) एक मैपिंग चाइल्ड⇒स्टेट चुनता है जिसे सूत्र (वर्तमान स्थिति को देखते हुए) द्वारा अनुमति दी जाती है, और खिलाड़ी 2 जारी रखने के लिए चाइल्ड (नोड का) चुनता है। एक गैर-नियतात्मक ऑटोमेटन द्वारा अस्वीकृति देखने के लिए, प्रत्येक (नोड, राज्य) के लिए (बच्चे, राज्य) जोड़े का एक समुच्चय चुनें, जैसे कि हर विकल्प के लिए, कम से कम एक जोड़े को हिट किया जाए, और इस तरह कि सभी परिणामी पथ आगे बढ़ें अस्वीकृति के लिए.

एक मोनैडिक सिद्धांत को प्रथम क्रम सिद्धांत के साथ जोड़ना: फ़ेफ़रमैन-वॉथ प्रमेय निम्नानुसार विस्तारित/लागू होता है। यदि एम एक एमSओ प्रतिरूप है और एन एक प्रथम क्रम प्रतिरूप है, तो एम एक (थ्योरी (एम), थ्योरी (एन)) ओरेकल मशीन के सापेक्ष निर्णायक रहता है, तथापि एम को सभी कार्यों एम → एन के साथ संवर्धित किया गया हो जहां एम की पहचान की जाती है इसकी पहली वस्तुएं, और प्रत्येक s∈M के लिए हम N की एक असंयुक्त प्रतिलिपि का उपयोग करते हैं, भाषा को तदनुसार संशोधित किया जाता है। उदाहरण के लिए, यदि N है ( $\mathbb {R}$ ,0,+,⋅), हम बता सकते हैं ∀(function f) ∀s ∃r∈N_s एफ(S)+_{N_s}आर = 0 उप>एन_s</उप>. यदि M S2S है (या अधिक सामान्यतः, कुछ मोनैडिक प्रतिरूप का ट्री समकक्ष), तो ऑटोमेटा अब N-सूत्रों का उपयोग कर सकता है, और इस प्रकार f:M→N को परिवर्तित कर सकता है^kM समुच्चय के टुपल में। असम्बद्धता आवश्यक है क्योंकि अन्यथा समानता वाले प्रत्येक अनंत N के लिए, विस्तारित S2S या मात्र WS1S अनिर्णीत है। इसके अतिरिक्त, (संभवतः अपूर्ण) सिद्धांत T के लिए, सिद्धांत T^{T के एम-उत्पादों का एम (थ्योरी (एम), T) ओरेकल के सापेक्ष निर्णय योग्य है, जहां T का एक प्रतिरूप ^M एक मनमाना असंयुक्त प्रतिरूप N का उपयोग करता है_s प्रत्येक s∈M के लिए T का (जैसा कि ऊपर बताया गया है, M एक एमSओ प्रतिरूप है; थ्योरी(N_s) S पर निर्भर हो सकता है)। इसका प्रमाण सूत्र जटिलता पर प्रेरण द्वारा है। चलो वी_s निःशुल्क एन की सूची बनें_s यदि फलन f मुफ़्त है, तो f(s) सहित चर। प्रेरण द्वारा, कोई यह दर्शाता है कि v_s इसका उपयोग मात्र |v के साथ एन-सूत्रों के एक सीमित समुच्चय के माध्यम से किया जाता है_s| मुक्त चर. इस प्रकार, हम जो संभव है उसका उत्तर देने के लिए एन (या T) का उपयोग करके सभी संभावित परिणामों की मात्रा निर्धारित कर सकते हैं, और एक सूची संभावनाओं (या बाधाओं) को देखते हुए, एम में एक संबंधित सूत्र तैयार कर सकते हैं।}

S2S के एक्सटेंशन में कोडिंग: स्ट्रिंग्स पर प्रत्येक निर्णायक विधेय को एन्कोडेड विधेय के साथ S2S (यहां तक कि उपरोक्त एक्सटेंशन के साथ) की निर्णायकता के लिए एन्कोड किया जा सकता है (रैखिक समय एन्कोडिंग और डिकोडिंग के साथ)। प्रमाण: एक गैर-नियतात्मक अनंत ट्री ऑटोमेटन को देखते हुए, हम परिमित बाइनरी लेबल वाले ट्री ों के समुच्चय को विभाजित कर सकते हैं (जिन पर ऑटोमेटन संचालित हो सकता है) को कई वर्गों में विभाजित किया जा सकता है, जैसे कि यदि एक पूर्ण अनंत बाइनरी ट्री समान श्रेणी के ट्री ों से बना हो सकता है, स्वीकृति मात्र वर्ग और प्रारंभिक स्थिति पर निर्भर करती है (अर्थात ऑटोमेटन ट्री में प्रवेश करता है)। ( पम्पिंग लेम्मा के साथ एक मोटे समानता पर ध्यान दें।) उदाहरण के लिए (एक समता ऑटोमेटन के लिए), ट्री ों को एक ही वर्ग में असाइन करें यदि उनके पास एक ही विधेय है जो दिए गए प्रारंभिक_स्टेट और (स्टेट, उच्चतम_प्राथमिकता_पहुंचे हुए) जोड़े का क्यू देता है तो खिलाड़ी 1 ( अर्थात् गैर-नियतिवाद) एक साथ सभी शाखाओं को Q के तत्वों के अनुरूप होने के लिए मजबूर कर सकता है। अब, प्रत्येक k के लिए, ट्री ों का एक सीमित समुच्चय चुनें (कोडिंग के लिए उपयुक्त) जो कि ऑटोमेटा 1-k के लिए एक ही वर्ग से संबंधित है, वर्ग की विकल्प के अनुरूप के पार किसी विधेय को एनकोड करने के लिए, कुछ बिट्स को k=1 का उपयोग करके एनकोड करें, फिर अधिक बिट्स को k=2 का उपयोग करके एनकोड करें, इत्यादि।

संदर्भ

↑ Rabin, Michael (1969). "अनंत पेड़ों पर दूसरे क्रम के सिद्धांतों और ऑटोमेटा की निर्णायकता" (PDF). Transactions of the American Mathematical Society. 141.
↑ Janin, David; Lenzi, Giacomo. बाइनरी ट्री के मोनैडिक लॉजिक की संरचना पर. MFCS 1999. doi:10.1007/3-540-48340-3_28.
↑ Siefkes, Dirk (1971), An axiom system for the weak monadic second order theory of two successors
↑ Riba, Colin (2012). अनंत शब्दों पर राक्षसी दूसरे क्रम के तर्क के स्वयंसिद्धीकरण की पूर्णता का एक मॉडल सैद्धांतिक प्रमाण (PDF). TCS 2012. doi:10.1007/978-3-642-33475-7_22.
↑ Carayol, Arnaud; Löding, Christof (2007), "MSO on the Infinite Binary Tree: Choice and Order" (PDF), Computer Science Logic, Lecture Notes in Computer Science, vol. 4646, pp. 161–176, doi:10.1007/978-3-540-74915-8_15, ISBN 978-3-540-74914-1, S2CID 14580598
↑ Das, Anupam; Riba, Colin (2020). "अनंत पेड़ों का एक कार्यात्मक (मोनैडिक) दूसरे क्रम का सिद्धांत". Logical Methods in Computer Science. 16 (4). arXiv:1903.05878. doi:10.23638/LMCS-16(4:6)2020. (A preliminary 2015 version erroneously claimed proof of completeness without the determinacy schema.)
↑ Gurevich, Yuri; Shelah, Saharon (1984). "अद्वैतवादी सिद्धांत और "अगली दुनिया"". Israel Journal of Mathematics. 49 (1–3): 55–68. doi:10.1007/BF02760646. S2CID 15807840.
↑ "What is the Turing degree of the monadic theory of the real line?". MathOverflow. Retrieved November 14, 2022.
↑ Gurevich, Yuri; Magidor, Menachem; Shelah, Saharon (1993). "The monadic theory of ω₂" (PDF). The Journal of Symbolic Logic. 48 (2): 387–398. doi:10.2307/2273556. JSTOR 2273556. S2CID 120260712.
↑ Neeman, Itay (2008), "Monadic definability of ordinals" (PDF), Computational Prospects of Infinity, Lecture Notes Series, Institute for Mathematical Sciences, National University of Singapore, vol. 15, pp. 193–205, doi:10.1142/9789812796554_0010, ISBN 978-981-279-654-7
↑ Bojańczyk, Mikołaj; Parys, Paweł; Toruńczyk, Szymon (2015), The MSO+U theory of (N, <) is undecidable, arXiv:1502.04578
↑ Bojańczyk, Mikołaj (2014), Weak MSO+U with path quantifiers over infinite trees, arXiv:1404.7278
↑ Kołodziejczyk, Leszek; Michalewski, Henryk (2016). राबिन की निर्णायकता प्रमेय कितनी अप्रमाणित है?. LICS '16: 31st Annual ACM/IEEE Symposium on Logic in Computer Science. arXiv:1508.06780.
↑ Kołodziejczyk, Leszek (October 19, 2015). "Question on Decidability of S2S". FOM.
↑ Kołodziejczyk, Leszek; Michalewski, Henryk; Pradic, Pierre; Skrzypczak, Michał (2019). "The logical strength of Büchi's decidability theorem". Logical Methods in Computer Science. 15 (2): 16:1–16:31.
↑ Piterman, Nir (2006). नॉनडेटर्मिनिस्टिक बुची और स्ट्रीट ऑटोमेटा से लेकर नियतात्मक पैरिटी ऑटोमेटा तक. 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06). pp. 255–264. arXiv:0705.2205. doi:10.1109/LICS.2006.28.
↑ Löding, Christof; Pirogov, Anton. Determinization of Büchi Automata: Unifying the Approaches of Safra and Muller-Schupp. ICALP 2019. arXiv:1902.02139.
↑ Calude, Cristian; Jain, Sanjay; Khoussainov, Bakhadyr; Li, Wei; Stephan, Frank. अर्धबहुपद समय में समता खेल तय करना (PDF). STOC 2017.
↑ Shelah, Saharon (Nov 1975). "व्यवस्था का मोनैडिक सिद्धांत" (PDF). Annals of Mathematics. 102 (3): 379–419. doi:10.2307/1971037. JSTOR 1971037.
↑ "The generalization of Shelah–Stup theorem" (PDF). Retrieved November 14, 2022.

Additional reference:
Weyer, Mark (2002). "Decidability of S1S and S2S". Automata, Logics, and Infinite Games. Lecture Notes in Computer Science. Vol. 2500. Springer. pp. 207–230. doi:10.1007/3-540-36387-4_12. ISBN 978-3-540-00388-5.

[1] Rabin, Michael (1969). "अनंत पेड़ों पर दूसरे क्रम के सिद्धांतों और ऑटोमेटा की निर्णायकता" (PDF). Transactions of the American Mathematical Society. 141.

[2] Janin, David; Lenzi, Giacomo. बाइनरी ट्री के मोनैडिक लॉजिक की संरचना पर. MFCS 1999. doi:10.1007/3-540-48340-3_28.

[3] Siefkes, Dirk (1971), An axiom system for the weak monadic second order theory of two successors

[4] Riba, Colin (2012). अनंत शब्दों पर राक्षसी दूसरे क्रम के तर्क के स्वयंसिद्धीकरण की पूर्णता का एक मॉडल सैद्धांतिक प्रमाण (PDF). TCS 2012. doi:10.1007/978-3-642-33475-7_22.

[5] Carayol, Arnaud; Löding, Christof (2007), "MSO on the Infinite Binary Tree: Choice and Order" (PDF), Computer Science Logic, Lecture Notes in Computer Science, vol. 4646, pp. 161–176, doi:10.1007/978-3-540-74915-8_15, ISBN 978-3-540-74914-1, S2CID 14580598

[6] Das, Anupam; Riba, Colin (2020). "अनंत पेड़ों का एक कार्यात्मक (मोनैडिक) दूसरे क्रम का सिद्धांत". Logical Methods in Computer Science. 16 (4). arXiv:1903.05878. doi:10.23638/LMCS-16(4:6)2020. (A preliminary 2015 version erroneously claimed proof of completeness without the determinacy schema.)

[7] Gurevich, Yuri; Shelah, Saharon (1984). "अद्वैतवादी सिद्धांत और "अगली दुनिया"". Israel Journal of Mathematics. 49 (1–3): 55–68. doi:10.1007/BF02760646. S2CID 15807840.

[8] "What is the Turing degree of the monadic theory of the real line?". MathOverflow. Retrieved November 14, 2022.

[9] Gurevich, Yuri; Magidor, Menachem; Shelah, Saharon (1993). "The monadic theory of ω₂" (PDF). The Journal of Symbolic Logic. 48 (2): 387–398. doi:10.2307/2273556. JSTOR 2273556. S2CID 120260712.

[10] Neeman, Itay (2008), "Monadic definability of ordinals" (PDF), Computational Prospects of Infinity, Lecture Notes Series, Institute for Mathematical Sciences, National University of Singapore, vol. 15, pp. 193–205, doi:10.1142/9789812796554_0010, ISBN 978-981-279-654-7

[11] Bojańczyk, Mikołaj; Parys, Paweł; Toruńczyk, Szymon (2015), The MSO+U theory of (N, <) is undecidable, arXiv:1502.04578

[12] Bojańczyk, Mikołaj (2014), Weak MSO+U with path quantifiers over infinite trees, arXiv:1404.7278

[S2S--Pi-1-2-CA_0-13] Kołodziejczyk, Leszek; Michalewski, Henryk (2016). राबिन की निर्णायकता प्रमेय कितनी अप्रमाणित है?. LICS '16: 31st Annual ACM/IEEE Symposium on Logic in Computer Science. arXiv:1508.06780.

[14] Kołodziejczyk, Leszek (October 19, 2015). "Question on Decidability of S2S". FOM.

[15] Kołodziejczyk, Leszek; Michalewski, Henryk; Pradic, Pierre; Skrzypczak, Michał (2019). "The logical strength of Büchi's decidability theorem". Logical Methods in Computer Science. 15 (2): 16:1–16:31.

[16] Piterman, Nir (2006). नॉनडेटर्मिनिस्टिक बुची और स्ट्रीट ऑटोमेटा से लेकर नियतात्मक पैरिटी ऑटोमेटा तक. 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06). pp. 255–264. arXiv:0705.2205. doi:10.1109/LICS.2006.28.

[17] Löding, Christof; Pirogov, Anton. Determinization of Büchi Automata: Unifying the Approaches of Safra and Muller-Schupp. ICALP 2019. arXiv:1902.02139.

[18] Calude, Cristian; Jain, Sanjay; Khoussainov, Bakhadyr; Li, Wei; Stephan, Frank. अर्धबहुपद समय में समता खेल तय करना (PDF). STOC 2017.

[19] Shelah, Saharon (Nov 1975). "व्यवस्था का मोनैडिक सिद्धांत" (PDF). Annals of Mathematics. 102 (3): 379–419. doi:10.2307/1971037. JSTOR 1971037.

[20] "The generalization of Shelah–Stup theorem" (PDF). Retrieved November 14, 2022.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

@@ 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 विधेय चर की अनुपस्थिति का संकेत मिलता है।
-* स्ट्रिंग्स 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 में व्यक्त की जा सकती है)। S1S को यह आवश्यक करके प्राप्त किया जा सकता है कि '1' स्ट्रिंग्स में प्रकट न हो, और 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 से संबंधित सिद्धांत ==
-प्रत्येक परिमित k के लिए, वृक्ष-चौड़ाई ≤k (और संबंधित वृक्ष अपघटन) के साथ गणनीय ग्राफ़ का मोनैडिक द्वितीय क्रम (MSO) सिद्धांत S2S में व्याख्या योग्य है (कोर्सेल का प्रमेय देखें)। उदाहरण के लिए, पेड़ों का एमएसओ सिद्धांत (ग्राफ़ के रूप में) या [[श्रृंखला-समानांतर ग्राफ]]़ का निर्णय लेने योग्य है। यहां (यानी बंधे हुए पेड़ की चौड़ाई के लिए), हम शीर्षों (या किनारों) के एक समुच्चय के लिए परिमितता परिमाणक की व्याख्या भी कर सकते हैं, और एक निश्चित पूर्णांक के समुच्चय मॉड्यूलो में शीर्षों (या किनारों) की गिनती भी कर सकते हैं। बेशुमार ग्राफ़ की अनुमति देने से सिद्धांत नहीं बदलता है। इसके अलावा, तुलना के लिए, S1S बंधे हुए [[पथ-चौड़ाई]] के जुड़े ग्राफ़ की व्याख्या कर सकता है।
+प्रत्येक परिमित k के लिए, ट्री-चौड़ाई ≤k (और संबंधित ट्री अपघटन) के साथ गणनीय ग्राफ़ का मोनैडिक द्वितीय क्रम (एमSओ) सिद्धांत S2S में व्याख्या योग्य होता है (कोर्सेल का प्रमेय देखें)। उदाहरण के लिए, ट्री की एमSओ सिद्धांत (ग्राफ़ के रूप में) या [[श्रृंखला-समानांतर ग्राफ]] का निर्णय लेने योग्य होता है। यहां (अर्थात् बंधे हुए ट्री  की चौड़ाई के लिए), हम शीर्षों (या किनारों) के एक समुच्चय के लिए परिमितता परिमाणक की व्याख्या भी कर सकते हैं, और एक निश्चित पूर्णांक के समुच्चय मॉड्यूलो में शीर्षों (या किनारों) की गिनती भी कर सकते हैं। असंख्य ग्राफ़ की अनुमति देने से सिद्धांत नहीं बदलता है। इसके अतिरिक्त, तुलना के लिए, S1S बंधे हुए [[पथ-चौड़ाई]] के जुड़े ग्राफ़ की व्याख्या कर सकता है।
+इसके विपरीत, असंबद्ध ट्री -चौड़ाई के ग्राफ़ के प्रत्येक समुच्चय के लिए, इसका अस्तित्व (अर्थात् Σ<sup>1</sup><sub>1</sub>) यदि हम शीर्षों और किनारों दोनों पर विधेय की अनुमति देते हैं तो एमSओ सिद्धांत अनिर्णीत होता है। इस प्रकार, एक अर्थ में, S2S की निर्णायकता सर्वोत्तम संभव होती है। असीमित ट्री-चौड़ाई वाले ग्राफ़ में बड़े ग्रिड माइनर होते हैं, जिनका उपयोग [[ट्यूरिंग मशीन]] का अनुकरण करने के लिए किया जा सकता है।
-इसके विपरीत, असंबद्ध वृक्ष-चौड़ाई के ग्राफ़ के प्रत्येक समुच्चय के लिए, इसका अस्तित्व (यानी Σ)<sup>1</sup><sub>1</sub>) यदि हम शीर्षों और किनारों दोनों पर विधेय की अनुमति देते हैं तो एमएसओ सिद्धांत अनिर्णीत है। इस प्रकार, एक अर्थ में, S2S की निर्णायकता सर्वोत्तम संभव है। अनबाउंड ट्रीविड्थ वाले ग्राफ़ में बड़े ग्रिड माइनर होते हैं, जिनका उपयोग [[ट्यूरिंग मशीन]] का अनुकरण करने के लिए किया जा सकता है।
+S2S में कमी करके, गणनीय आदेशों का एमSओ सिद्धांत निर्णायक होता है, जैसा कि उनके क्लेन-ब्रौवर आदेशों के साथ गणनीय ट्री का एमSओ सिद्धांत होता है। यघपि, एमSओ सिद्धांत (<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> क्रमवाचक संख्या का एमSओ सिद्धांत <ω<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>,...,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> समय होता है)।
-प्रत्येक 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>).
+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> के माध्यम से दूसरे क्रम के अंकगणित में व्यक्त नहीं किया जा सकता है (रिवर्स गणित देखें)। 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> सिद्ध करने योग्य होते हो।
-हालाँकि, मुक्त दूसरे क्रम के चर के साथ, प्रत्येक 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>.
+इसके अतिरिक्त, बाइनरी स्ट्रिंग 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> परिणामो को संतुष्ट करता है।
-इसके अलावा, बाइनरी स्ट्रिंग एस और टी के दिए गए समुच्चय, निम्नलिखित समतुल्य हैं:<br />
+== S1S और S2S के प्रतिरूप ==
-(1) टी एस2एस है जिसे एस से गणना योग्य बाइनरी स्ट्रिंग्स बहुपद समय के कुछ समुच्चय से परिभाषित किया जा सकता है।<br />
-(2) टी की गणना कुछ गेम के लिए जीतने की स्थिति के समुच्चय से की जा सकती है जिसका भुगतान Π का एक सीमित बूलियन संयोजन है<sup>0</sup><sub>2</sub>(एस) समुच्चय.<br />
-(3) टी को अंकगणित μ-कैलकुलस में एस से परिभाषित किया जा सकता है (अंकगणित सूत्र + निश्चित-बिंदु तर्क | कम से कम निश्चित-बिंदु तर्क)<br />
-(4) टी सबसे कम बीटा-मॉडल में है|β-मॉडल (यानी एक ω-मॉडल जिसका समुच्चय-सैद्धांतिक समकक्ष [[ सकर्मक मॉडल |सकर्मक मॉडल]] है) जिसमें एस शामिल है और सभी Π को संतुष्ट करता है<sup>1</sup><sub>3</sub> Π के परिणाम<sup>1</sup><sub>2</sub>-वह<sub>0</sub>.
-== S1S और S2S के मॉडल ==
+मानक प्रतिरूप  (जो S1S और S2S के लिए अद्वितीय एमएसओ प्रतिरूप  होता है) के अतिरिक्त, S1S और S2S के लिए अन्य प्रतिरूप  भी होते हैं, जो कार्यक्षेत्र के सभी सबसमुच्चय के अतिरिक्त कुछ का उपयोग करते हैं ([[रिफंड नैरो सीएस|हेनकिन अर्थ विज्ञान]] देखें)।
-मानक मॉडल (जो S1S और S2S के लिए अद्वितीय MSO मॉडल है) के अलावा, S1S और S2S के लिए अन्य मॉडल भी हैं, जो डोमेन के सभी सबसमुच्चय के बजाय कुछ का उपयोग करते हैं ([[रिफंड नैरो सीएस]] देखें)।
+प्रत्येक S⊆ω के लिए, S में पुनरावर्ती समुच्चय मानक S1S प्रतिरूप  का एक प्राथमिक उपप्रतिरूप  बनाते हैं, और ट्यूरिंग जॉइन और ट्यूरिंग रिड्यूसिबिलिटी के अनुसार बंद किए गए ω के प्रत्येक गैर-रिक्त संग्रह के लिए समान होते हैं।<ref>{{Cite journal |last1=Kołodziejczyk |first1=Leszek |last2=Michalewski |first2=Henryk |last3=Pradic |first3=Pierre |last4=Skrzypczak |first4=Michał |title=The logical strength of Büchi's decidability theorem |journal=Logical Methods in Computer Science |volume=15 |issue=2 |date=2019 |pages=16:1–16:31 |url=https://lmcs.episciences.org/5503/}}</ref>
-प्रत्येक S⊆ω के लिए, S में पुनरावर्ती समुच्चय मानक S1S मॉडल का एक प्राथमिक उपमॉडल बनाते हैं, और ट्यूरिंग जॉइन और ट्यूरिंग रिड्यूसिबिलिटी के तहत बंद किए गए ω के प्रत्येक गैर-रिक्त संग्रह के लिए समान होते हैं।<ref>{{Cite journal |last1=Kołodziejczyk |first1=Leszek |last2=Michalewski |first2=Henryk |last3=Pradic |first3=Pierre |last4=Skrzypczak |first4=Michał |title=The logical strength of Büchi's decidability theorem |journal=Logical Methods in Computer Science |volume=15 |issue=2 |date=2019 |pages=16:1–16:31 |url=https://lmcs.episciences.org/5503/}}</ref>
+यह S1S निश्चित समुच्चयों की सापेक्ष पुनरावर्तीता और एकरूपता से निम्नानुसार होता है:<br />- φ(s) (s के एक फलन  के रूप में) की गणना φ के मापदंडों और s′ के एक सीमित समुच्चय के लिए φ(s′) के मानों से की जा सकती, (इसका आकार φ के लिए एक नियतात्मक ऑटोमेटन में राज्यों की संख्या से घिरा हुआ होता है)।<br />- ∃S φ(S) के लिए एक  k और S के S′ एक सीमित टुकड़ा चुनकर और S′ को बार-बार विस्तारित करके प्राप्त किया जा सकता है, जिससें प्रत्येक विस्तार के समय सर्वोच्च प्राथमिकता k होती है और विस्तार को k से ऊपर की प्राथमिकताओं को प्रभावित किए बिना S को संतुष्ट करते हुए S में पूरा किया जा सकता है (इन्हें मात्र प्रारंभिक S′ के लिए अनुमति दी गई है)। इसके अतिरिक्त, शाब्दिक रूप से कम से कम सबसे छोटे विकल्पों का उपयोग करके, एक S1S सूत्र φ' है, जो कि φ'⇒φ और ∃S φ(S) ⇔∃!S φ'(S) (अर्थात् एकरूपता; φ में मुक्त चर नहीं दिखाए जा सकते हैं; φ' मात्र  सूत्र φ) पर निर्भर करता है।
-यह S1S निश्चित समुच्चयों की सापेक्ष पुनरावर्तीता और एकरूपता से निम्नानुसार है:<br />
-- φ(s) (s के एक फ़ंक्शन के रूप में) की गणना φ के मापदंडों और φ(s) के मानों से की जा सकती है{{prime}}) एस के एक सीमित समुच्चय के लिए{{prime}} (इसका आकार φ के लिए एक नियतात्मक ऑटोमेटन में राज्यों की संख्या से घिरा हुआ है)।<br />
-- ∃S φ(S) के लिए एक गवाह k और S का एक सीमित टुकड़ा चुनकर प्राप्त किया जा सकता है{{prime}} का, और बार-बार एस का विस्तार करना{{prime}} जैसे कि प्रत्येक विस्तार के दौरान सर्वोच्च प्राथमिकता k है और विस्तार को k से ऊपर की प्राथमिकताओं को प्रभावित किए बिना S को संतुष्ट करते हुए S में पूरा किया जा सकता है (इन्हें केवल प्रारंभिक S के लिए अनुमति दी गई है){{prime}}). इसके अलावा, लेक्सिकोग्राफ़िक रूप से कम से कम सबसे छोटे विकल्पों का उपयोग करके, एक S1S सूत्र φ' है, जैसे कि φ'⇒φ और ∃S φ(S) ⇔∃!S φ'(S) (यानी एकरूपता; φ में मुक्त चर नहीं दिखाए जा सकते हैं; φ' केवल सूत्र φ) पर निर्भर करता है।
-S2S के न्यूनतम मॉडल में बाइनरी स्ट्रिंग्स पर सभी नियमित भाषाएँ शामिल हैं। यह मानक मॉडल का एक प्रारंभिक उपमॉडल है, इसलिए यदि पेड़ों का एक S2S पैरामीटर-मुक्त निश्चित समुच्चय गैर-रिक्त है, तो इसमें एक नियमित पेड़ शामिल है। एक नियमित भाषा को एक नियमित {0,1}-लेबल पूर्ण अनंत बाइनरी ट्री (स्ट्रिंग्स पर विधेय के साथ पहचाना गया) के रूप में भी माना जा सकता है। एक लेबल वाला पेड़ नियमित होता है यदि इसे प्रारंभिक शीर्ष के साथ शीर्ष-लेबल वाले परिमित निर्देशित ग्राफ को अनियंत्रित करके प्राप्त किया जा सकता है; प्रारंभिक शीर्ष से पहुंच योग्य ग्राफ़ में एक (निर्देशित) चक्र एक अनंत वृक्ष देता है। नियमित पेड़ों की इस व्याख्या और एन्कोडिंग के साथ, प्रत्येक सच्चा S2S वाक्य प्राथमिक फ़ंक्शन अंकगणित में पहले से ही सिद्ध हो सकता है। यह गैर-नियमित पेड़ हैं जिन्हें निर्धारण के लिए गैर-विधेयात्मक समझ की आवश्यकता हो सकती है (नीचे)। गणना योग्य संतुष्टि संबंध के साथ S1S (और संभवतः S2S) (मानक प्रथम क्रम भाग के साथ और बिना दोनों) के गैर-नियमित (यानी गैर-नियमित भाषाओं वाले) मॉडल हैं। हालाँकि, स्ट्रिंग के पुनरावर्ती समुच्चय का समुच्चय समझ और निर्धारण की विफलता के कारण S2S का मॉडल नहीं बनाता है।
+S2S के न्यूनतम प्रतिरूप  में बाइनरी स्ट्रिंग्स पर सभी नियमित भाषाएँ सम्मलित होती हैं। यह मानक प्रतिरूप  का एक प्रारंभिक उपप्रतिरूप होता  है, इसलिए यदि ट्री एक S2S पैरामीटर-मुक्त निश्चित समुच्चय गैर-रिक्त होता है, तो इसमें एक नियमित ट्री सम्मलित होता है। एक नियमित भाषा को एक नियमित {0,1}-लेबल पूर्ण अनंत बाइनरी ट्री (स्ट्रिंग्स पर विधेय के साथ पहचाना गया) के रूप में भी माना जा सकता है। एक लेबल वाला ट्री  नियमित होता है यदि इसे प्रारंभिक शीर्ष के साथ शीर्ष-लेबल वाले परिमित निर्देशित ग्राफ को अनियंत्रित करके प्राप्त किया जा सकता है; प्रारंभिक शीर्ष से पहुंच योग्य ग्राफ़ में एक (निर्देशित) चक्र एक अनंत ट्री देता है। नियमित ट्री की इस व्याख्या और एन्कोडिंग के साथ, प्रत्येक सत्य  S2S सूत्र प्राथमिक फलन  अंकगणित में पहले से ही सिद्ध हो सकता है। यह गैर-नियमित ट्री होता  हैं जिन्हें निर्धारण के लिए गैर-विधेयात्मक समझ की आवश्यकता हो सकती है। गणना योग्य संबंध के साथ S1S (और संभवतः S2S) (मानक प्रथम क्रम भाग के साथ और बिना दोनों) के गैर-नियमित (अर्थात् गैर-नियमित भाषाओं वाले) प्रतिरूप होते हैं। यघपि , स्ट्रिंग के पुनरावर्ती समुच्चय का समुच्चय के ज्ञान और निर्धारण की विफलता के कारण S2S का प्रतिरूप नहीं बनाता है।
 == S2S की निर्णायकता ==
-निर्णायकता का प्रमाण यह दर्शाकर है कि प्रत्येक सूत्र एक गैर-नियतात्मक वृक्ष ऑटोमेटन द्वारा स्वीकृति के बराबर है ([[ वृक्ष स्वचालन | वृक्ष स्वचालन]] और अनंत-वृक्ष ऑटोमेटन देखें)। एक अनंत वृक्ष ऑटोमेटन जड़ से शुरू होता है और पेड़ की ओर बढ़ता है, और यदि प्रत्येक वृक्ष शाखा स्वीकार करती है तो इसे स्वीकार करती है। एक गैर-नियतात्मक ट्री ऑटोमेटन स्वीकार करता है कि क्या खिलाड़ी 1 के पास जीतने की रणनीति है, जहां खिलाड़ी 1 नए राज्यों की एक अनुमत (वर्तमान स्थिति और इनपुट के लिए) जोड़ी चुनता है (पी)<sub>0</sub>,पी<sub>1</sub>), जबकि खिलाड़ी 2 पी में संक्रमण के साथ शाखा चुनता है<sub>0</sub> यदि 0 चुना गया है और पी<sub>1</sub> अन्यथा। एक सह-नॉनडेटर्मिनिस्टिक ऑटोमेटन के लिए, सभी विकल्प खिलाड़ी 2 के अनुसार होते हैं, जबकि नियतात्मक के लिए, (पी)<sub>0</sub>,पी<sub>1</sub>) राज्य और इनपुट द्वारा तय किया गया है; और एक गेम ऑटोमेटन के लिए, दो खिलाड़ी शाखा और राज्य को समुच्चय करने के लिए एक सीमित गेम खेलते हैं। किसी शाखा पर स्वीकृति शाखा पर अनंत बार देखी जाने वाली स्थितियों पर आधारित होती है; समता ऑटोमेटा यहाँ पर्याप्त रूप से सामान्य हैं।
+निर्णायकता का प्रमाण यह प्रदर्शित करता है कि प्रत्येक सूत्र एक गैर-नियतात्मक ट्री ऑटोमेटन द्वारा स्वीकृति के बराबर होता है ([[ वृक्ष स्वचालन | ट्री स्वचालन]] और अनंत-ट्री  ऑटोमेटन देखें)। एक अनंत ट्री  ऑटोमेटन जड़ से प्रारम्भ  होता है और ट्री  की ओर बढ़ता है, और यदि प्रत्येक ट्री  शाखा स्वीकार करती है तो इसे स्वीकार करती है। एक गैर-नियतात्मक ट्री ऑटोमेटन स्वीकार करता है कि क्या खिलाड़ी 1 के पास जीतने की रणनीति है, जहां खिलाड़ी 1 नए राज्यों (पी 0, पी 1) की एक अनुमत (वर्तमान स्थिति और इनपुट के लिए) जोड़ी चुनता है, जबकि खिलाड़ी 2 शाखा चुनता है, यदि पी 0 में संक्रमण होता है 0 चुना गया है और p1 अन्यथा। सह-नॉनडेटर्मिनिस्टिक ऑटोमेटन के लिए, सभी विकल्प प्लेयर 2 द्वारा तय किए जाते हैं, जबकि नियतात्मक के लिए, (p0,p1) राज्य और इनपुट द्वारा तय किया जाता है; और एक गेम ऑटोमेटन के लिए, दो खिलाड़ी शाखा और राज्य को सेट करने के लिए एक सीमित गेम खेलते हैं। किसी शाखा पर स्वीकृति शाखा पर अनंत बार देखी जाने वाली स्थितियों पर आधारित होती है; समता ऑटोमेटा यहाँ पर्याप्त रूप से सामान्य हैं।
-सूत्रों को ऑटोमेटा में परिवर्तित करने के लिए, आधार मामला आसान है, और गैर-नियतत्ववाद अस्तित्वगत परिमाणकों के तहत समापन देता है, इसलिए हमें केवल पूरकता के तहत समापन की आवश्यकता है। समता खेलों की स्थितिगत निर्धारण का उपयोग करते हुए (जहां हमें पूर्वव्यापी समझ की आवश्यकता होती है), खिलाड़ी 1 जीतने वाली रणनीति की गैर-मौजूदगी एक खिलाड़ी 2 जीतने वाली रणनीति एस देती है, एक सह-नॉनडेटर्मिनिस्टिक ट्री ऑटोमेटन इसकी सुदृढ़ता की पुष्टि करता है। फिर ऑटोमेटन को नियतिवादी बनाया जा सकता है (जहां हमें राज्यों की संख्या में तेजी से वृद्धि मिलती है), और इस प्रकार एस का अस्तित्व एक गैर-नियतात्मक ऑटोमेटन द्वारा स्वीकृति से मेल खाता है।
+सूत्रों को ऑटोमेटा में परिवर्तित करने के लिए, आधार मामला आसान है, और गैर-नियतत्ववाद अस्तित्वगत परिमाणकों के अनुसार  समापन देता है, इसलिए हमें मात्र  पूरकता के अनुसार  समापन की आवश्यकता है। समता खेलों की स्थितिगत निर्धारण का उपयोग करते हुए (जहां हमें पूर्वव्यापी समझ की आवश्यकता होती है), खिलाड़ी 1 जीतने वाली रणनीति की गैर-मौजूदगी एक खिलाड़ी 2 जीतने वाली रणनीति S देती है, एक सह-नॉनडेटर्मिनिस्टिक ट्री ऑटोमेटन इसकी सुदृढ़ता की पुष्टि करता है। फिर ऑटोमेटन को नियतिवादी बनाया जा सकता है (जहां हमें राज्यों की संख्या में तेजी से वृद्धि मिलती है), और इस प्रकार S का अस्तित्व एक गैर-नियतात्मक ऑटोमेटन द्वारा स्वीकृति से मेल खाता है।
-निश्चयात्मकता: [[ZFC]] में, बोरेल खेल निश्चयात्मकता हैं, और Π के बूलियन संयोजनों के लिए निर्धारण प्रमाण हैं<sup>0</sup><sub>2</sub> सूत्र (मनमाने वास्तविक मापदंडों के साथ) यहां एक रणनीति भी देते हैं जो केवल वर्तमान स्थिति और पेड़ की स्थिति पर निर्भर करती है। इसका प्रमाण प्राथमिकताओं की संख्या पर प्रेरण द्वारा है। मान लें कि k प्राथमिकताएँ हैं, सर्वोच्च प्राथमिकता k है, और k में खिलाड़ी 2 के लिए सही समता है। प्रत्येक स्थिति (वृक्ष स्थिति + स्थिति) के लिए कम से कम क्रमसूचक α (यदि कोई हो) निर्दिष्ट करें ताकि खिलाड़ी 1 की जीत हो सभी दर्ज की गई (एक या अधिक चरणों के बाद) प्राथमिकता k स्थितियों (यदि कोई हो) के साथ रणनीति जिसमें लेबल <α हो। यदि प्रारंभिक स्थिति को लेबल किया गया है तो खिलाड़ी 1 जीत सकता है: हर बार प्राथमिकता k स्थिति तक पहुंचने पर, क्रमसूचक कम हो जाता है, और इसके अलावा घटने के बीच, खिलाड़ी 1 k-1 प्राथमिकताओं के लिए एक रणनीति का उपयोग कर सकता है। यदि स्थिति लेबल रहित है तो खिलाड़ी 2 जीत सकता है: k-1 प्राथमिकताओं के निर्धारण के अनुसार, खिलाड़ी 2 के पास एक रणनीति होती है जो जीतती है या एक गैर-लेबल प्राथमिकता k स्थिति में प्रवेश करती है, जिस स्थिति में खिलाड़ी 2 फिर से उस रणनीति का उपयोग कर सकता है। रणनीति को स्थितिगत बनाने के लिए (k पर प्रेरण द्वारा), सहायक खेल खेलते समय, यदि दो चुनी गई स्थितीय रणनीतियाँ एक ही स्थिति में ले जाती हैं, तो निम्न α के साथ रणनीति जारी रखें, या उसी α के लिए (या खिलाड़ी 2 के लिए) कम प्रारंभिक स्थिति (ताकि हम एक रणनीति को कई बार सीमित रूप से बदल सकें)।
+निश्चयात्मकता: [[ZFC]] में, बोरेल खेल निश्चयात्मकता हैं, और Π के बूलियन संयोजनों के लिए निर्धारण प्रमाण हैं<sup>0</sup><sub>2</sub> सूत्र (मनमाने वास्तविक मापदंडों के साथ) यहां एक रणनीति भी देते हैं जो मात्र  वर्तमान स्थिति और ट्री  की स्थिति पर निर्भर करती है। इसका प्रमाण प्राथमिकताओं की संख्या पर प्रेरण द्वारा है। मान लें कि k प्राथमिकताएँ हैं, सर्वोच्च प्राथमिकता k है, और k में खिलाड़ी 2 के लिए सही समता है। प्रत्येक स्थिति (ट्री  स्थिति + स्थिति) के लिए कम से कम क्रमसूचक α (यदि कोई हो) निर्दिष्ट करें ताकि खिलाड़ी 1 की जीत हो सभी दर्ज की गई (एक या अधिक चरणों के बाद) प्राथमिकता k स्थितियों (यदि कोई हो) के साथ रणनीति जिसमें लेबल <α हो। यदि प्रारंभिक स्थिति को लेबल किया गया है तो खिलाड़ी 1 जीत सकता है: हर बार प्राथमिकता k स्थिति तक पहुंचने पर, क्रमसूचक कम हो जाता है, और इसके अतिरिक्त घटने के मध्य, खिलाड़ी 1 k-1 प्राथमिकताओं के लिए एक रणनीति का उपयोग कर सकता है। यदि स्थिति लेबल रहित है तो खिलाड़ी 2 जीत सकता है: k-1 प्राथमिकताओं के निर्धारण के अनुसार, खिलाड़ी 2 के पास एक रणनीति होती है जो जीतती है या एक गैर-लेबल प्राथमिकता k स्थिति में प्रवेश करती है, जिस स्थिति में खिलाड़ी 2 फिर से उस रणनीति का उपयोग कर सकता है। रणनीति को स्थितिगत बनाने के लिए (k पर प्रेरण द्वारा), सहायक खेल खेलते समय, यदि दो चुनी गई स्थितीय रणनीतियाँ एक ही स्थिति में ले जाती हैं, तो निम्न α के साथ रणनीति जारी रखें, या उसी α के लिए (या खिलाड़ी 2 के लिए) कम प्रारंभिक स्थिति (ताकि हम एक रणनीति को कई बार सीमित रूप से बदल सकें)।
-ऑटोमेटा निर्धारण: सह-नॉनडेटर्मिनिस्टिक ट्री ऑटोमेटा के निर्धारण के लिए, ω-ऑटोमेटा पर विचार करना, शाखा की पसंद को इनपुट के रूप में मानना, ऑटोमेटन का निर्धारण करना और नियतात्मक ट्री ऑटोमेटन के लिए इसका उपयोग करना पर्याप्त है। ध्यान दें कि यह गैर-नियतात्मक ट्री ऑटोमेटा के लिए काम नहीं करता है क्योंकि बाईं ओर जाने का निर्धारण (यानी s→s0) दाहिनी शाखा की सामग्री पर निर्भर हो सकता है; गैर-नियतिवाद के विपरीत, नियतिवादी वृक्ष ऑटोमेटा सटीक रूप से गैर-रिक्त समुच्चयों को भी स्वीकार नहीं कर सकता है। एक गैर-नियतात्मक ω-ऑटोमेटन एम को निर्धारित करने के लिए (सह-नॉनडेटर्मिनिस्टिक के लिए, पूरक लें, यह ध्यान में रखते हुए कि नियतात्मक समता ऑटोमेटा पूरक के तहत बंद हैं), हम प्रत्येक नोड के साथ एम के संभावित राज्यों का एक समुच्चय संग्रहीत करने और नोड निर्माण के लिए एक सफरा पेड़ का उपयोग कर सकते हैं। और उच्च प्राथमिकता वाले राज्यों तक पहुंचने के आधार पर विलोपन। विवरण के लिए देखें <ref>{{Cite conference |last=Piterman |first=Nir |title=नॉनडेटर्मिनिस्टिक बुची और स्ट्रीट ऑटोमेटा से लेकर नियतात्मक पैरिटी ऑटोमेटा तक|conference=21st Annual IEEE Symposium on Logic in Computer Science (LICS'06) |date=2006 |pages=255–264 |doi=10.1109/LICS.2006.28 |arxiv=0705.2205}}</ref> या।<ref>{{Cite conference |last1=Löding |first1=Christof |last2=Pirogov |first2=Anton |title=Determinization of Büchi Automata: Unifying the Approaches of Safra and Muller-Schupp |conference=ICALP 2019 |arxiv=1902.02139}}</ref>
+ऑटोमेटा निर्धारण: सह-नॉनडेटर्मिनिस्टिक ट्री ऑटोमेटा के निर्धारण के लिए, ω-ऑटोमेटा पर विचार करना, शाखा की विकल्प को इनपुट के रूप में मानना, ऑटोमेटन का निर्धारण करना और नियतात्मक ट्री ऑटोमेटन के लिए इसका उपयोग करना पर्याप्त है। ध्यान दें कि यह गैर-नियतात्मक ट्री ऑटोमेटा के लिए काम नहीं करता है क्योंकि बाईं ओर जाने का निर्धारण (अर्थात् s→s0) दाहिनी शाखा की सामग्री पर निर्भर हो सकता है; गैर-नियतिवाद के विपरीत, नियतिवादी ट्री  ऑटोमेटा स्पष्ट  रूप से गैर-रिक्त समुच्चयों को भी स्वीकार नहीं कर सकता है। एक गैर-नियतात्मक ω-ऑटोमेटन एम को निर्धारित करने के लिए (सह-नॉनडेटर्मिनिस्टिक के लिए, पूरक लें, यह ध्यान में रखते हुए कि नियतात्मक समता ऑटोमेटा पूरक के अनुसार  बंद हैं), हम प्रत्येक नोड के साथ एम के संभावित राज्यों का एक समुच्चय संग्रहीत करने और नोड निर्माण के लिए एक सफरा ट्री  का उपयोग कर सकते हैं। और उच्च प्राथमिकता वाले राज्यों तक पहुंचने के आधार पर विलोपन। विवरण के लिए देखें <ref>{{Cite conference |last=Piterman |first=Nir |title=नॉनडेटर्मिनिस्टिक बुची और स्ट्रीट ऑटोमेटा से लेकर नियतात्मक पैरिटी ऑटोमेटा तक|conference=21st Annual IEEE Symposium on Logic in Computer Science (LICS'06) |date=2006 |pages=255–264 |doi=10.1109/LICS.2006.28 |arxiv=0705.2205}}</ref> या।<ref>{{Cite conference |last1=Löding |first1=Christof |last2=Pirogov |first2=Anton |title=Determinization of Büchi Automata: Unifying the Approaches of Safra and Muller-Schupp |conference=ICALP 2019 |arxiv=1902.02139}}</ref>
-स्वीकृति की निर्णायकता: खाली पेड़ के एक गैर-नियतात्मक समता ऑटोमेटन द्वारा स्वीकृति एक परिमित ग्राफ जी पर एक समता खेल से मेल खाती है। उपरोक्त स्थितीय (जिसे स्मृतिहीन भी कहा जाता है) निर्धारण का उपयोग करते हुए, इसे एक परिमित खेल द्वारा अनुकरण किया जा सकता है जो तब समाप्त होता है जब हम एक तक पहुंचते हैं लूप, लूप में सर्वोच्च प्राथमिकता वाले राज्य के आधार पर जीतने की स्थिति के साथ। एक चतुर अनुकूलन एक अर्धबहुपद समय एल्गोरिथ्म देता है,<ref>{{Cite conference |title = अर्धबहुपद समय में समता खेल तय करना|last1=Calude |first1=Cristian |last2=Jain |first2=Sanjay |last3=Khoussainov |first3=Bakhadyr  |last4=Li |first4= Wei |last5=Stephan |first5=Frank |conference=STOC 2017 |url=https://researchspace.auckland.ac.nz/bitstream/handle/2292/31757/500Cris.pdf}}</ref> जो बहुपद समय है जब प्राथमिकताओं की संख्या काफी कम होती है (जो आमतौर पर व्यवहार में होती है)।
+स्वीकृति की निर्णायकता: खाली ट्री  के एक गैर-नियतात्मक समता ऑटोमेटन द्वारा स्वीकृति एक परिमित ग्राफ जी पर एक समता खेल से मेल खाती है। उपरोक्त स्थितीय (जिसे स्मृतिहीन भी कहा जाता है) निर्धारण का उपयोग करते हुए, इसे एक परिमित खेल द्वारा अनुकरण किया जा सकता है जो तब समाप्त होता है जब हम एक तक पहुंचते हैं लूप, लूप में सर्वोच्च प्राथमिकता वाले राज्य के आधार पर जीतने की स्थिति के साथ। एक चतुर अनुकूलन एक अर्धबहुपद समय एल्गोरिथ्म देता है,<ref>{{Cite conference |title = अर्धबहुपद समय में समता खेल तय करना|last1=Calude |first1=Cristian |last2=Jain |first2=Sanjay |last3=Khoussainov |first3=Bakhadyr  |last4=Li |first4= Wei |last5=Stephan |first5=Frank |conference=STOC 2017 |url=https://researchspace.auckland.ac.nz/bitstream/handle/2292/31757/500Cris.pdf}}</ref> जो बहुपद समय है जब प्राथमिकताओं की संख्या काफी कम होती है (जो आमतौर पर व्यवहार में होती है)।
-पेड़ों का सिद्धांत: पेड़ों पर एमएसओ तर्क की निर्णायकता के लिए (यानी ग्राफ़ जो पेड़ हैं), यहां तक कि पहले क्रम की वस्तुओं के लिए परिमितता और मॉड्यूलर गिनती क्वांटिफायर के साथ, हम गणनीय पेड़ों को पूर्ण बाइनरी पेड़ में एम्बेड कर सकते हैं और एस 2 एस की निर्णायकता का उपयोग कर सकते हैं। उदाहरण के लिए, एक नोड s के लिए, हम उसके बच्चों को s1, s01, s001 इत्यादि द्वारा दर्शा सकते हैं। अनगिनत पेड़ों के लिए, हम शेलह-स्टुप प्रमेय (नीचे) का उपयोग कर सकते हैं। हम कार्डिनलिटी ω वाले समुच्चय प्रथम क्रम ऑब्जेक्ट के लिए एक विधेय भी जोड़ सकते हैं<sub>1</sub>, और कार्डिनैलिटी के लिए विधेय ω<sub>2</sub>, और इसी तरह अनंत नियमित कार्डिनल्स के लिए। बंधे हुए पेड़ की चौड़ाई के ग्राफ़ को पेड़ों का उपयोग करके व्याख्या की जा सकती है, और किनारों पर विधेय के बिना यह बंधे हुए क्लिक चौड़ाई के ग्राफ़ पर भी लागू होता है।
+ट्री ों का सिद्धांत: ट्री ों पर एमSओ युक्ति  की निर्णायकता के लिए (अर्थात् ग्राफ़ जो ट्री  हैं), यहां तक कि पहले क्रम की वस्तुओं के लिए परिमितता और मॉड्यूलर गिनती परिमाणक के साथ, हम गणनीय ट्री ों को पूर्ण बाइनरी ट्री  में एम्बेड कर सकते हैं और S 2 S की निर्णायकता का उपयोग कर सकते हैं। उदाहरण के लिए, एक नोड s के लिए, हम उसके बच्चों को s1, s01, s001 इत्यादि द्वारा दर्शा सकते हैं। अनगिनत ट्री ों के लिए, हम शेलह-स्टुप प्रमेय (नीचे) का उपयोग कर सकते हैं। हम कार्डिनलिT ω वाले समुच्चय प्रथम क्रम ऑब्जेक्ट के लिए एक विधेय भी जोड़ सकते हैं<sub>1</sub>, और कार्डिनैलिT के लिए विधेय ω<sub>2</sub>, और इसी तरह अनंत नियमित कार्डिनल्स के लिए। बंधे हुए ट्री  की चौड़ाई के ग्राफ़ को ट्री ों का उपयोग करके व्याख्या की जा सकती है, और किनारों पर विधेय के बिना यह बंधे हुए क्लिक चौड़ाई के ग्राफ़ पर भी लागू होता है।
 == S2S को अन्य निर्णायक सिद्धांतों के साथ जोड़ना ==
-अद्वैत सिद्धांतों के वृक्ष विस्तार: शेलह-स्टूप प्रमेय द्वारा,<ref>{{Cite journal |last=Shelah |first=Saharon |title=व्यवस्था का मोनैडिक सिद्धांत|journal=Annals of Mathematics |volume=102 |issue=3 |date=Nov 1975 |pages=379–419 |doi=10.2307/1971037 |jstor=1971037 |url=https://shelah.logic.at/files/213042/42.pdf}}</ref><ref>{{Cite web |url=https://www.mccme.ru/shen/muchnik-memorial/materials/publications/tree_str.pdf |title=The generalization of Shelah–Stup theorem |access-date=November 14, 2022}}</ref> यदि एक मोनैडिक रिलेशनल मॉडल एम निर्णायक है, तो उसका वृक्ष समकक्ष भी ऐसा ही है। उदाहरण के लिए, (औपचारिकरण का मॉड्यूलो विकल्प) S2S, {0,1} का वृक्ष समकक्ष है। ट्री समकक्ष में, पहले क्रम की वस्तुएं विस्तार द्वारा क्रमित एम के तत्वों के परिमित अनुक्रम हैं, और एक एम-संबंध पी<sub>''i''</sub> पी पर मैप किया गया है<sub>''i''</sub>(सीईओ<sub>1</sub>,...,सीईओ<sub>k</sub>) ⇔ पी<sub>''i''</sub>(डी<sub>1</sub>,...,डी<sub>k</sub>) पी के साथ<sub>''i''</sub>' अन्यथा गलत (डी<sub>''j''</sub>∈M, और v, M के तत्वों का एक (संभवतः खाली) अनुक्रम है)। प्रमाण S2S निर्णायकता प्रमाण के समान है। प्रत्येक चरण में, एक (नॉनडेटर्मिनिस्टिक) ऑटोमेटन को इनपुट के रूप में एम ऑब्जेक्ट्स (संभवतः दूसरे क्रम) का एक टुपल मिलता है, और एक एम फॉर्मूला निर्धारित करता है कि किस राज्य संक्रमण की अनुमति है। खिलाड़ी 1 (जैसा कि ऊपर है) एक मैपिंग चाइल्ड⇒स्टेट चुनता है जिसे सूत्र (वर्तमान स्थिति को देखते हुए) द्वारा अनुमति दी जाती है, और खिलाड़ी 2 जारी रखने के लिए चाइल्ड (नोड का) चुनता है। एक गैर-नियतात्मक ऑटोमेटन द्वारा अस्वीकृति देखने के लिए, प्रत्येक (नोड, राज्य) के लिए (बच्चे, राज्य) जोड़े का एक समुच्चय चुनें, जैसे कि हर विकल्प के लिए, कम से कम एक जोड़े को हिट किया जाए, और इस तरह कि सभी परिणामी पथ आगे बढ़ें अस्वीकृति के लिए.
+अद्वैत सिद्धांतों के ट्री  विस्तार: शेलह-स्टूप प्रमेय द्वारा,<ref>{{Cite journal |last=Shelah |first=Saharon |title=व्यवस्था का मोनैडिक सिद्धांत|journal=Annals of Mathematics |volume=102 |issue=3 |date=Nov 1975 |pages=379–419 |doi=10.2307/1971037 |jstor=1971037 |url=https://shelah.logic.at/files/213042/42.pdf}}</ref><ref>{{Cite web |url=https://www.mccme.ru/shen/muchnik-memorial/materials/publications/tree_str.pdf |title=The generalization of Shelah–Stup theorem |access-date=November 14, 2022}}</ref> यदि एक मोनैडिक रिलेशनल प्रतिरूप  एम निर्णायक है, तो उसका ट्री  समकक्ष भी ऐसा ही है। उदाहरण के लिए, (औपचारिकरण का मॉड्यूलो विकल्प) S2S, {0,1} का ट्री  समकक्ष है। ट्री समकक्ष में, पहले क्रम की वस्तुएं विस्तार द्वारा क्रमित एम के तत्वों के परिमित अनुक्रम हैं, और एक एम-संबंध पी<sub>''i''</sub> पी पर मैप किया गया है<sub>''i''</sub>(सीईओ<sub>1</sub>,...,सीईओ<sub>k</sub>) ⇔ पी<sub>''i''</sub>(डी<sub>1</sub>,...,डी<sub>k</sub>) पी के साथ<sub>''i''</sub>' अन्यथा गलत (डी<sub>''j''</sub>∈M, और v, M के तत्वों का एक (संभवतः खाली) अनुक्रम है)। प्रमाण S2S निर्णायकता प्रमाण के समान है। प्रत्येक चरण में, एक (नॉनडेटर्मिनिस्टिक) ऑटोमेटन को इनपुट के रूप में एम ऑब्जेक्ट्स (संभवतः दूसरे क्रम) का एक टुपल मिलता है, और एक एम फॉर्मूला निर्धारित करता है कि किस राज्य संक्रमण की अनुमति है। खिलाड़ी 1 (जैसा कि ऊपर है) एक मैपिंग चाइल्ड⇒स्टेट चुनता है जिसे सूत्र (वर्तमान स्थिति को देखते हुए) द्वारा अनुमति दी जाती है, और खिलाड़ी 2 जारी रखने के लिए चाइल्ड (नोड का) चुनता है। एक गैर-नियतात्मक ऑटोमेटन द्वारा अस्वीकृति देखने के लिए, प्रत्येक (नोड, राज्य) के लिए (बच्चे, राज्य) जोड़े का एक समुच्चय चुनें, जैसे कि हर विकल्प के लिए, कम से कम एक जोड़े को हिट किया जाए, और इस तरह कि सभी परिणामी पथ आगे बढ़ें अस्वीकृति के लिए.
-एक मोनैडिक सिद्धांत को प्रथम क्रम सिद्धांत के साथ जोड़ना: फ़ेफ़रमैन-वॉथ प्रमेय निम्नानुसार विस्तारित/लागू होता है। यदि एम एक एमएसओ मॉडल है और एन एक प्रथम क्रम मॉडल है, तो एम एक (थ्योरी (एम), थ्योरी (एन)) [[ओरेकल मशीन]] के सापेक्ष निर्णायक रहता है, भले ही एम को सभी कार्यों एम → एन के साथ संवर्धित किया गया हो जहां एम की पहचान की जाती है इसकी पहली वस्तुएं, और प्रत्येक s∈M के लिए हम N की एक असंयुक्त प्रतिलिपि का उपयोग करते हैं, भाषा को तदनुसार संशोधित किया जाता है। उदाहरण के लिए, यदि N है (<math>\mathbb{R}</math>,0,+,⋅), हम बता सकते हैं ∀(function f) ∀s ∃r∈N<sub>''s''</sub> एफ(एस)+<sub>''N''<sub>''s''</sub></sub>आर = 0 उप>एन<sub>''s''</sub></उप>. यदि M S2S है (या अधिक सामान्यतः, कुछ मोनैडिक मॉडल का वृक्ष समकक्ष), तो ऑटोमेटा अब N-सूत्रों का उपयोग कर सकता है, और इस प्रकार f:M→N को परिवर्तित कर सकता है<sup>k</sup>M समुच्चय के टुपल में। असम्बद्धता आवश्यक है क्योंकि अन्यथा समानता वाले प्रत्येक अनंत N के लिए, विस्तारित S2S या केवल WS1S अनिर्णीत है। इसके अलावा, (संभवतः अपूर्ण) सिद्धांत टी के लिए, सिद्धांत टी<sup>टी के एम-उत्पादों का एम (थ्योरी (एम), टी) ओरेकल के सापेक्ष निर्णय योग्य है, जहां टी का एक मॉडल<sup>M</sup> एक मनमाना असंयुक्त मॉडल N का उपयोग करता है<sub>''s''</sub> प्रत्येक s∈M के लिए T का (जैसा कि ऊपर बताया गया है, M एक MSO मॉडल है; थ्योरी(N<sub>''s''</sub>) एस पर निर्भर हो सकता है)। इसका प्रमाण सूत्र जटिलता पर प्रेरण द्वारा है। चलो वी<sub>''s''</sub> निःशुल्क एन की सूची बनें<sub>''s''</sub> यदि फ़ंक्शन f मुफ़्त है, तो f(s) सहित चर। प्रेरण द्वारा, कोई यह दर्शाता है कि v<sub>''s''</sub> इसका उपयोग केवल |v के साथ एन-सूत्रों के एक सीमित समुच्चय के माध्यम से किया जाता है<sub>''s''</sub>| मुक्त चर. इस प्रकार, हम जो संभव है उसका उत्तर देने के लिए एन (या टी) का उपयोग करके सभी संभावित परिणामों की मात्रा निर्धारित कर सकते हैं, और एक सूची संभावनाओं (या बाधाओं) को देखते हुए, एम में एक संबंधित वाक्य तैयार कर सकते हैं।
+एक मोनैडिक सिद्धांत को प्रथम क्रम सिद्धांत के साथ जोड़ना: फ़ेफ़रमैन-वॉथ प्रमेय निम्नानुसार विस्तारित/लागू होता है। यदि एम एक एमSओ प्रतिरूप  है और एन एक प्रथम क्रम प्रतिरूप  है, तो एम एक (थ्योरी (एम), थ्योरी (एन)) [[ओरेकल मशीन]] के सापेक्ष निर्णायक रहता है, तथापि   एम को सभी कार्यों एम → एन के साथ संवर्धित किया गया हो जहां एम की पहचान की जाती है इसकी पहली वस्तुएं, और प्रत्येक s∈M के लिए हम N की एक असंयुक्त प्रतिलिपि का उपयोग करते हैं, भाषा को तदनुसार संशोधित किया जाता है। उदाहरण के लिए, यदि N है (<math>\mathbb{R}</math>,0,+,⋅), हम बता सकते हैं ∀(function f) ∀s ∃r∈N<sub>''s''</sub> एफ(S)+<sub>''N''<sub>''s''</sub></sub>आर = 0 उप>एन<sub>''s''</sub></उप>. यदि M S2S है (या अधिक सामान्यतः, कुछ मोनैडिक प्रतिरूप  का ट्री  समकक्ष), तो ऑटोमेटा अब N-सूत्रों का उपयोग कर सकता है, और इस प्रकार f:M→N को परिवर्तित कर सकता है<sup>k</sup>M समुच्चय के टुपल में। असम्बद्धता आवश्यक है क्योंकि अन्यथा समानता वाले प्रत्येक अनंत N के लिए, विस्तारित S2S या मात्र  WS1S अनिर्णीत है। इसके अतिरिक्त, (संभवतः अपूर्ण) सिद्धांत T के लिए, सिद्धांत T<sup>T के एम-उत्पादों का एम (थ्योरी (एम), T) ओरेकल के सापेक्ष निर्णय योग्य है, जहां T का एक प्रतिरूप <sup>M</sup> एक मनमाना असंयुक्त प्रतिरूप  N का उपयोग करता है<sub>''s''</sub> प्रत्येक s∈M के लिए T का (जैसा कि ऊपर बताया गया है, M एक एमSओ प्रतिरूप  है; थ्योरी(N<sub>''s''</sub>) S पर निर्भर हो सकता है)। इसका प्रमाण सूत्र जटिलता पर प्रेरण द्वारा है। चलो वी<sub>''s''</sub> निःशुल्क एन की सूची बनें<sub>''s''</sub> यदि फलन  f मुफ़्त है, तो f(s) सहित चर। प्रेरण द्वारा, कोई यह दर्शाता है कि v<sub>''s''</sub> इसका उपयोग मात्र  |v के साथ एन-सूत्रों के एक सीमित समुच्चय के माध्यम से किया जाता है<sub>''s''</sub>| मुक्त चर. इस प्रकार, हम जो संभव है उसका उत्तर देने के लिए एन (या T) का उपयोग करके सभी संभावित परिणामों की मात्रा निर्धारित कर सकते हैं, और एक सूची संभावनाओं (या बाधाओं) को देखते हुए, एम में एक संबंधित सूत्र तैयार कर सकते हैं।
-S2S के एक्सटेंशन में कोडिंग: स्ट्रिंग्स पर प्रत्येक निर्णायक विधेय को एन्कोडेड विधेय के साथ S2S (यहां तक कि उपरोक्त एक्सटेंशन के साथ) की निर्णायकता के लिए एन्कोड किया जा सकता है (रैखिक समय एन्कोडिंग और डिकोडिंग के साथ)। प्रमाण: एक गैर-नियतात्मक अनंत वृक्ष ऑटोमेटन को देखते हुए, हम परिमित बाइनरी लेबल वाले पेड़ों के समुच्चय को विभाजित कर सकते हैं (जिन पर ऑटोमेटन संचालित हो सकता है) को कई वर्गों में विभाजित किया जा सकता है, जैसे कि यदि एक पूर्ण अनंत बाइनरी ट्री समान श्रेणी के पेड़ों से बना हो सकता है, स्वीकृति केवल वर्ग और प्रारंभिक स्थिति पर निर्भर करती है (अर्थात ऑटोमेटन पेड़ में प्रवेश करता है)। ([[ पम्पिंग लेम्मा | पम्पिंग लेम्मा]] के साथ एक मोटे समानता पर ध्यान दें।) उदाहरण के लिए (एक समता ऑटोमेटन के लिए), पेड़ों को एक ही वर्ग में असाइन करें यदि उनके पास एक ही विधेय है जो दिए गए प्रारंभिक_स्टेट और (स्टेट, उच्चतम_प्राथमिकता_पहुंचे हुए) जोड़े का क्यू देता है तो खिलाड़ी 1 ( यानी गैर-नियतिवाद) एक साथ सभी शाखाओं को Q के तत्वों के अनुरूप होने के लिए मजबूर कर सकता है। अब, प्रत्येक k के लिए, पेड़ों का एक सीमित समुच्चय चुनें (कोडिंग के लिए उपयुक्त) जो कि ऑटोमेटा 1-k के लिए एक ही वर्ग से संबंधित है, वर्ग की पसंद के अनुरूप के पार किसी विधेय को एनकोड करने के लिए, कुछ बिट्स को k=1 का उपयोग करके एनकोड करें, फिर अधिक बिट्स को k=2 का उपयोग करके एनकोड करें, इत्यादि।
+S2S के एक्सटेंशन में कोडिंग: स्ट्रिंग्स पर प्रत्येक निर्णायक विधेय को एन्कोडेड विधेय के साथ S2S (यहां तक कि उपरोक्त एक्सटेंशन के साथ) की निर्णायकता के लिए एन्कोड किया जा सकता है (रैखिक समय एन्कोडिंग और डिकोडिंग के साथ)। प्रमाण: एक गैर-नियतात्मक अनंत ट्री  ऑटोमेटन को देखते हुए, हम परिमित बाइनरी लेबल वाले ट्री ों के समुच्चय को विभाजित कर सकते हैं (जिन पर ऑटोमेटन संचालित हो सकता है) को कई वर्गों में विभाजित किया जा सकता है, जैसे कि यदि एक पूर्ण अनंत बाइनरी ट्री समान श्रेणी के ट्री ों से बना हो सकता है, स्वीकृति मात्र  वर्ग और प्रारंभिक स्थिति पर निर्भर करती है (अर्थात ऑटोमेटन ट्री  में प्रवेश करता है)। ([[ पम्पिंग लेम्मा | पम्पिंग लेम्मा]] के साथ एक मोटे समानता पर ध्यान दें।) उदाहरण के लिए (एक समता ऑटोमेटन के लिए), ट्री ों को एक ही वर्ग में असाइन करें यदि उनके पास एक ही विधेय है जो दिए गए प्रारंभिक_स्टेट और (स्टेट, उच्चतम_प्राथमिकता_पहुंचे हुए) जोड़े का क्यू देता है तो खिलाड़ी 1 ( अर्थात् गैर-नियतिवाद) एक साथ सभी शाखाओं को Q के तत्वों के अनुरूप होने के लिए मजबूर कर सकता है। अब, प्रत्येक k के लिए, ट्री ों का एक सीमित समुच्चय चुनें (कोडिंग के लिए उपयुक्त) जो कि ऑटोमेटा 1-k के लिए एक ही वर्ग से संबंधित है, वर्ग की विकल्प के अनुरूप के पार किसी विधेय को एनकोड करने के लिए, कुछ बिट्स को k=1 का उपयोग करके एनकोड करें, फिर अधिक बिट्स को k=2 का उपयोग करके एनकोड करें, इत्यादि।
 == संदर्भ ==

Anonymous

Search

S2S (गणित): Difference between revisions

Namespaces

More

Page actions

Revision as of 02:23, 6 July 2023

Contents

मूल गुण

निर्णय जटिलता

अक्षीयकरण

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

सूत्र जटिलता

S1S और S2S के प्रतिरूप

S2S की निर्णायकता

S2S को अन्य निर्णायक सिद्धांतों के साथ जोड़ना

संदर्भ

Navigation

Navigation

Wiki tools

Wiki tools

Anonymous

Search

S2S (गणित): Difference between revisions

Revision as of 02:23, 6 July 2023

मूल गुण

निर्णय जटिलता

अक्षीयकरण

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

सूत्र जटिलता

S1S और S2S के प्रतिरूप

S2S की निर्णायकता

S2S को अन्य निर्णायक सिद्धांतों के साथ जोड़ना

संदर्भ

Navigation

Wiki tools

Page tools

Other projects

Categories