S2S (गणित)

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

मूल गुण

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} एक पूर्ण अनंत बाइनरी ट्री बनाता है।
• सूत्र जटिलता के लिए, स्ट्रिंग्स पर उपसर्ग संबंध को सामान्यतः पहले क्रम के रूप में माना जाता है। इसकेअतिरिक्त, सभी सूत्र Δ¹₂ के समतुल्य नहीं होंगे।
• S2S में अभिव्यक्त गुणों के लिए (सभी बाइनरी स्ट्रिंग्स के समुच्चय को एक ट्री के रूप में देखते हुए), प्रत्येक नोड के लिए, मात्र O(1) बिट्स को बाएं सबट्री और दाएं सबट्री और बाकी के मध्य संचारित किया जा सकता है (संचार जटिलता देखें)।
• एक निश्चित k के लिए, स्ट्रिंग से k तक एक फलन (अर्थात् k के नीचे की प्राकृतिक संख्या) को एक समुच्चय द्वारा एनकोड किया जा सकता है। इसके अतिरिक्त, s,t ⇒ s01t′ जहां T′ t के प्रत्येक वर्ण को दोगुना कर देता है, और s ⇒ {s01t′: t∈{0,1}^*} S2S निश्चित होता है। इसके विपरीत, संचार जटिलता युक्ति के अनुसार, S1S (नीचे) में समुच्चय की एक जोड़ी को एक समुच्चय द्वारा एनकोड करने योग्य नहीं होता है।

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

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

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

अक्षीयकरण

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

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

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

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

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

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

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

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

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

सूत्र जटिलता

बाइनरी स्ट्रिंग्स का एक समुच्चय 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₀ } में सिद्ध किया जा सकता है। आधार सिद्धांत पर, स्कीमा (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 के लिए अद्वितीय MSO प्रतिरूप होता है) के अतिरिक्त, S1S और S2S के लिए अन्य प्रतिरूप भी होते हैं, जो कार्यक्षेत्र के सभी सबसमुच्चय के अतिरिक्त कुछ का उपयोग करते हैं (हेनकिन अर्थ विज्ञान देखें)।

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

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

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

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

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

स्वीकृति की निर्णायकता: रिक्त ट्री के एक गैर-नियतात्मक समता ऑटोमेटन द्वारा स्वीकृति एक परिमित ग्राफ G पर एक समता खेल से सामान्य होती है। उपरोक्त स्थितीय (जिसे स्मृतिहीन भी कहा जाता है) निर्धारण का उपयोग करते हुए, इसे एक परिमित खेल द्वारा अनुकरण किया जा सकता है जो तब समाप्त होता है जब तक हम लूप में सर्वोच्च प्राथमिकता वाले स्थिति के आधार पर जीतने की स्थिति के साथ एक लूप तक पहुंचते हैं। एक सर्वोत्तम अनुकूलन एक अर्धबहुपद समय एल्गोरिथ्म देता है, जो बहुपद समय होता है जब प्राथमिकताओं की संख्या अत्यधिक कम होती है (जो अधिकांशतः व्यवहार में होती है)।

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

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

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

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

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

संदर्भ

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.